PiTensorProduct.lift.tprod
theorem PiTensorProduct.lift.tprod :
∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
[inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
{φ : MultilinearMap R s E} (f : (i : ι) → s i), (PiTensorProduct.lift φ) ((PiTensorProduct.tprod R) f) = φ f
The theorem `PiTensorProduct.lift.tprod` states that for any index set `ι`, any commutative semiring `R`, any family of types `s : ι → Type` each equipped with an additive commutative monoid structure and an `R`-module structure, and any type `E` equipped with an additive commutative monoid structure and an `R`-module structure, for any multilinear map `φ : MultilinearMap R s E` and any function `f : (i : ι) → s i`, the function `PiTensorProduct.lift φ` applied to the canonical multilinear map `PiTensorProduct.tprod R` of `f`, is equal to `φ` applied to `f`.
In other words, lifting a multilinear map `φ` to the space of tensor products and then applying it to a tensor product of a function `f`, is the same as directly applying `φ` to `f`. This property is crucial in showing the universal property of the tensor product.
More concisely: For any commutative semiring R, any family s : ι → Type of types with additive commutative monoid and R-module structures, any R-module E with additive commutative monoid structure, any multilinear map φ : R^(s) -> E, and any function f : ι -> s, the maps PiTensorProduct.lift φ (PiTensorProduct.tprod R) and φ applied to f are equal.
|
PiTensorProduct.ext
theorem PiTensorProduct.ext :
∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
[inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
{φ₁ φ₂ : (PiTensorProduct R fun i => s i) →ₗ[R] E},
φ₁.compMultilinearMap (PiTensorProduct.tprod R) = φ₂.compMultilinearMap (PiTensorProduct.tprod R) → φ₁ = φ₂
The theorem `PiTensorProduct.ext` states that for a given type `ι`, a commutative semiring `R`, a function `s : ι → Type u_7` wherein each `s i` is an additive commutative monoid and a module over `R`, and another module `E` over `R`, if there are two linear mappings `φ₁` and `φ₂` from the Pi Tensor Product of `s i` over `R` to `E` such that the composition of these mappings with the canonical multilinear map from `s` to the Pi Tensor Product equals, then `φ₁` and `φ₂` must be the same. In other words, if two linear maps agree on the output of the canonical multilinear map, they are the same.
More concisely: Given a commutative semiring R, a type ι, and for each i in ι, a commutative additive monoid s(i) that is an R-module, if two linear maps from the Pi tensor product of the s(i) over R to an R-module E agree on the canonical multilinear map, then they are equal.
|
PiTensorProduct.hasSMul'.proof_5
theorem PiTensorProduct.hasSMul'.proof_5 :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {R₁ : Type u_4} {s : ι → Type u_3}
[inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
[inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] (r : R₁) [inst_6 : DecidableEq ι] (z : R)
(f : (i : ι) → s i) (i : ι) (r' : R),
PiTensorProduct.tprodCoeff R (r • z) (Function.update f i (r' • f i)) =
PiTensorProduct.tprodCoeff R (r • (r' * z)) f
This theorem states that in the context of a commutative semiring `R`, an indexed collection of additively commutative monoids `s i` that are also `R`-modules, and a distributive multiply action of `R₁` on `R` where `R₁` is a monoid and the scalar multiplication is commutative, given an element `r` of `R₁`, a decidable equality on the indexing set `ι`, an element `z` of `R`, a function `f` from `ι` to `s i`, an index `i` in `ι`, and a scalar `r'` in `R`, the tensor product coefficient of the scalar multiple `r` times `z` and the function `f` updated at index `i` to be `r'` times `f i` equals the tensor product coefficient of `r` times the product of `r'` and `z` and the original function `f`. This essentially establishes a particular equality of tensor product coefficients under certain scalar multiplications and updates to the function `f`.
More concisely: Given a commutative semiring `R`, an indexed collection of additively commutative `R`-modules `s i`, a distributive multiply action of a commutative monoid `R₁` on `R`, and a function `f` from `ι` to `s i`, the tensor product coefficient of `r` (an element of `R₁`) times `z` (an element of `R`) and the updated function `f` at index `i` with scalar `r'`, equals the tensor product coefficient of `r` times the product of `r'` and `z` and the original function `f`.
|
PiTensorProduct.reindex_symm
theorem PiTensorProduct.reindex_symm :
∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {M : Type u_8} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (e : ι ≃ ι₂),
(PiTensorProduct.reindex R (fun x => M) e).symm = PiTensorProduct.reindex R (fun x => M) e.symm
This theorem, named `PiTensorProduct.reindex_symm`, states that for any types `ι` and `ι₂`, a commutative semiring `R`, and a module `M` over `R`, if we have a bijection `e` between `ι` and `ι₂`, then the inverse of the `reindex` function applied to `e` in the context of the tensor product of `M` over all elements of `ι` (denoted by `PiTensorProduct.reindex`) is equal to the `reindex` function applied to the inverse of `e`. This essentially asserts the compatibility of the `reindex` function with the operation of taking inverses of bijections.
More concisely: For any commutative semiring R, type ι and ι₂, and module M over R, if there is a bijection e between ι and ι₂, then `PiTensorProduct.reindex (e. inverse) (M ⊗ₗ (Pi M ι)) = (PiTensorProduct.reindex e)_ (M ⊗ₗ (Pi M ι₂))`.
|
PiTensorProduct.hasSMul'.proof_4
theorem PiTensorProduct.hasSMul'.proof_4 :
∀ {ι : Type u_2} {R : Type u_1} [inst : CommSemiring R] {R₁ : Type u_4} {s : ι → Type u_3}
[inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
[inst_4 : DistribMulAction R₁ R] (r : R₁) (r' r'' : R) (f : (i : ι) → s i),
PiTensorProduct.tprodCoeff R (r • r') f + PiTensorProduct.tprodCoeff R (r • r'') f =
PiTensorProduct.tprodCoeff R (r • (r' + r'')) f
This theorem states that for all types `ι`, `R`, and `R₁`, under the conditions that `R` is a commutative semiring, each `s i` (where `s` is a function from `ι` to some type) is a module over `R`, and `R₁` is a monoid that is also a distributive multiplicative action on `R`, the scalar multiplication of `r` (from `R₁`) with `r'` (from `R`) and `r''` (also from `R`) followed by tensor producting with a function `f` from `ι` to `s i` satisfies the property of distribution over addition. In other words, if we tensor product a scalar multiple of a sum, we get the same result as if we had added the tensor products of the scalar multiples of the summands. Formulated mathematically, we have the equality:
`r * (r' + r'') * f = r * r' * f + r * r'' * f`,
where `*` represents tensor producting.
More concisely: Given commutative semiring `R`, module `s` over `R` indexed by type `ι`, monoid `R₁` acting distributively and multiplicatively on `R`, the scalar multiplication distributes over tensor product addition, i.e., `r * (r' + r'') * f = r * r' * f + r * r'' * f` for all `r, r', r'' from `R` and `f` from `ι` to `s ι`.
|
PiTensorProduct.induction_on'
theorem PiTensorProduct.induction_on' :
∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
[inst_2 : (i : ι) → Module R (s i)] {motive : (PiTensorProduct R fun i => s i) → Prop}
(z : PiTensorProduct R fun i => s i),
(∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)) →
(∀ (x y : PiTensorProduct R fun i => s i), motive x → motive y → motive (x + y)) → motive z
The theorem `PiTensorProduct.induction_on'` is an induction principle for the tensor product of a family of modules over a commutative semiring. It states that for any type `ι`, a commutative semiring `R`, a function `s` that maps each element of `ι` to a type, and a `motive` which is a property of elements of the tensor product of the 's `i`s over `R`, if the `motive` holds for each tensor product of the coefficients `r` and a function `f` from `ι` to `s i`, and if the `motive` is preserved under addition (i.e., if it holds for `x` and `y` then it also holds for `x + y`), then the `motive` holds for all elements `z` of the tensor product.
More concisely: Given a commutative semiring `R`, a type `ι`, and a family `{M_i : Type}_i.{0 < i < ℰ}` of `R`-modules indexed by `ι`, if for all `i` and `r : R`, `f : ι → M_i`, and `x, y : ∏ i, M_i`, the property `motive (r, f, x, y)` holds and is preserved under addition, then `motive (r, f, z)` holds for all `z : ∏ i, M_i`.
|
PiTensorProduct.smul_tprodCoeff'
theorem PiTensorProduct.smul_tprodCoeff' :
∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7}
[inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
[inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] (r : R₁) (z : R) (f : (i : ι) → s i),
r • PiTensorProduct.tprodCoeff R z f = PiTensorProduct.tprodCoeff R (r • z) f
This theorem states that for any types `ι`, `R`, `R₁`, and a function `s` mapping `ι` to another type, along with certain conditions on `R`, `R₁`, and `s` (such as `R` being a commutative semiring, each `s i` being an additive commutative monoid and a module over `R`, and `R₁` being a monoid that distributes over the multiplication action on `R`), the scalar multiplication of `r` from `R₁` and the tensor product coefficient of `R`, `z` from `R` and function `f` from `ι` to `s i`, is equal to the tensor product coefficient of `R`, the scalar multiplication of `r` and `z`, and `f`. In mathematical terms, it asserts that `r • (z ⊗ₜ f) = (r • z) ⊗ₜ f` where `•` denotes scalar multiplication and `⊗ₜ` represents the tensor product.
More concisely: For any commutative semiring `R`, monoid `R₁`, type `ι`, and function `s : ι → Type`, if `s i` is an additive commutative monoid and a module over `R` for each `i`, and `R₁` distributes over the multiplication action on `R`, then for all `r in R₁` and `z in R` and `f : ι → s i`, we have `r • (z ⊗ₜ f) = (r • z) ⊗ₜ f`, where `•` denotes scalar multiplication and `⊗ₜ` represents the tensor product.
|
PiTensorProduct.smul_add
theorem PiTensorProduct.smul_add :
∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {R₁ : Type u_5} {s : ι → Type u_7}
[inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
[inst_4 : DistribMulAction R₁ R] [inst_5 : SMulCommClass R₁ R R] (r : R₁) (x y : PiTensorProduct R fun i => s i),
r • (x + y) = r • x + r • y
The theorem `PiTensorProduct.smul_add` states that for any type `ι`, a commutative semiring `R`, a monoid `R₁`, a type family `s : ι → Type` such that each `s i` is an additive commutative monoid and a module over `R`, an action of `R₁` on `R` that is distributive over multiplication, a scalar multiplication that is commutative between `R₁` and `R`, and for any `r` in `R₁` and `x` and `y` in the Pi tensor product of the `s i`'s over `R`, the scalar multiplication of `r` with the sum of `x` and `y` equals the sum of the scalar multiplication of `r` with `x` and `r` with `y`. This is equivalent to the property `r • (x + y) = r • x + r • y` in the language of scalar multiplication and addition, where `•` denotes scalar multiplication and `+` denotes addition.
More concisely: For any commutative semiring `R`, monoid `R₁`, type family `s : ι → Type` of additive commutative monoids and `R`-modules, and distributive action of `R₁` on `R` and commutative scalar multiplication on `R₁ × (∏ i, s i)`, the scalar multiplication of an element `r` in `R₁` with the sum of two elements `x` and `y` in the Pi tensor product equals the sum of the scalar multiplications of `r` with `x` and `r` with `y`.
|
PiTensorProduct.hasSMul'.proof_3
theorem PiTensorProduct.hasSMul'.proof_3 :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {R₁ : Type u_4} {s : ι → Type u_3}
[inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
[inst_4 : DistribMulAction R₁ R] (r : R₁) [inst_5 : DecidableEq ι] (r' : R) (f : (i : ι) → s i) (i : ι)
(m₁ m₂ : s i),
PiTensorProduct.tprodCoeff R (r • r') (Function.update f i m₁) +
PiTensorProduct.tprodCoeff R (r • r') (Function.update f i m₂) =
PiTensorProduct.tprodCoeff R (r • r') (Function.update f i (m₁ + m₂))
This theorem, `PiTensorProduct.hasSMul'.proof_3`, establishes a property of tensor products in the context of commutative semirings and modules.
For any index type `ι`, commutative semiring `R`, type `R₁` forming a monoid, a distributive multiplication action of `R₁` on `R`, a function `s` mapping indices `i` from `ι` to additive commutative monoids that are also `R`-modules, a scalar `r` from `R₁`, a decidable equality on `ι`, a scalar `r'` from `R`, a function `f` from `ι` to `s i`, an index `i` from `ι`, and two elements `m₁` and `m₂` from `s i`:
The theorem states that the sum of the tensor products of the scalar `r • r'` and the updated functions `f` at index `i` with `m₁` and `m₂` respectively, equals the tensor product of the scalar `r • r'` and the updated function `f` at index `i` with the sum of `m₁` and `m₂`.
More concisely: For any commutative semiring `R`, index type `ι`, distributive action of `R` on additive commutative `R`-modules indexed by `ι`, scalar `r` from `R₁`, decidable equality on `ι`, and functions `s : ι -> AddMonoid R-Module`, `f : ι -> s i`, the tensor product of `r • r'` and `f i` with the sum of elements `m₁` and `m₂` from `s i` is equal to the sum of the tensor products of `r • r'` and `f i` with `m₁` and `m₂` respectively.
|
PiTensorProduct.hasSMul'.proof_1
theorem PiTensorProduct.hasSMul'.proof_1 :
∀ {ι : Type u_3} {R : Type u_2} [inst : CommSemiring R] {R₁ : Type u_4} {s : ι → Type u_1}
[inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
[inst_4 : DistribMulAction R₁ R] (r : R₁) (r' : R) (f : (i : ι) → s i) (i : ι),
f i = 0 → (fun f => PiTensorProduct.tprodCoeff R (r • f.1) f.2) (r', f) = 0
This theorem is stating that for any index type `ι`, any type `R` with a commutative semiring structure, any type `R₁` that is a monoid with multiplication distributing over addition on `R`, any function `s` from `ι` to a type with addition commutative monoid and module structure over `R`, given an element `r` of `R₁`, an element `r'` of `R`, a function `f` from `ι` to the type `s i` and an index `i`, if `f i` equals zero, then the tensor product of `r • f.1` and `f.2` with respect to `R` under the function `PiTensorProduct.tprodCoeff` equals zero.
More concisely: For any commutative semiring `R`, monoid `R₁` with `R`-module action on `s : ι → M` where `M` is an `R`-module with commutative additive monoid structure, and `r : R₁` and `r' : R`, if `f : ι → M` satisfies `f i = 0` for some index `i`, then `r • f i ⊗ f i (using `PiTensorProduct.tprodCoeff) = 0`.
|
PiTensorProduct.hasSMul'.proof_2
theorem PiTensorProduct.hasSMul'.proof_2 :
∀ {ι : Type u_2} {R : Type u_1} [inst : CommSemiring R] {R₁ : Type u_4} {s : ι → Type u_3}
[inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] [inst_3 : Monoid R₁]
[inst_4 : DistribMulAction R₁ R] (r : R₁) (f : (i : ι) → s i), PiTensorProduct.tprodCoeff R (r • 0) f = 0
This theorem states that for any index set `ι`, any commutative semiring `R`, any type `R₁` that forms a monoid, any scalar `r` from `R₁`, and any function `f` mapping from `ι` to a type `s i` (where each `s i` is an `R`-module and an add-commutative monoid), the tensor product of the zero scalar (scaled by `r`) and `f` is zero. This theorem essentially captures the property in tensor product that scaling the zero element results in the zero element.
More concisely: For any commutative semiring R, monoid M with scalar r, and function f from an index set ι to the add-commutative R-modules s i, the tensor product of r⊤ (the scalar multiplication of r in M) and f is the zero function.
|
PiTensorProduct.liftAux_tprod
theorem PiTensorProduct.liftAux_tprod :
∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
[inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
(φ : MultilinearMap R s E) (f : (i : ι) → s i), (PiTensorProduct.liftAux φ) ((PiTensorProduct.tprod R) f) = φ f
The theorem `PiTensorProduct.liftAux_tprod` states that for any type `ι`, any commutative semiring `R`, any type-valued function `s` from `ι`, and any type `E` (where the types `s i` and `E` are both additive commutative monoids and `R`-modules), given a multilinear map `φ` from `s` to `E` and a function `f` from `ι` to `s i`, the result of applying the auxiliary lift function `PiTensorProduct.liftAux` on the tensor product `PiTensorProduct.tprod R f` equals the result of applying the multilinear map `φ` on `f`. In other words, the auxiliary lift function `PiTensorProduct.liftAux` preserves the structure of the tensor product when applied to `PiTensorProduct.tprod R f`.
More concisely: Given a commutative semiring R, a type ι, an additive commutative monoid and R-module E, a multilinear map φ from ι to E, and a function f from ι to the type s with s i an additive commutative monoid and R-module, the auxiliary lift function PiTensorProduct.liftAux preserves the structure of the tensor product, i.e., PiTensorProduct.liftAux (PiTensorProduct.tprod R f) = φ (f).
|