TensorProduct.rid_tmul
theorem TensorProduct.rid_tmul :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
(r : R), (TensorProduct.rid R M) (m ⊗ₜ[R] r) = r • m
This theorem states that for any commutative semiring `R` and an `R`-module `M`, given any element `m` of `M` and any element `r` of `R`, applying the `TensorProduct.rid R M` operation to the tensor product of `m` and `r`, i.e., `(m ⊗ₜ[R] r)`, is equivalent to scaling `m` by `r`, denoted by `r • m`. In other words, the `TensorProduct.rid R M` operation behaves as a right identity for the tensor product of modules, up to linear equivalence.
More concisely: For any commutative semiring `R` and `R`-module `M`, the tensor product `(m ⊗ₜ[R] r)` of an element `m` of `M` and an element `r` of `R` is linear equivalent to the scalar multiplication `r • m` of `m` by `r`.
|
TensorProduct.tmul_smul
theorem TensorProduct.tmul_smul :
∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_2} [inst_1 : Monoid R'] {M : Type u_4} {N : Type u_5}
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : DistribMulAction R' M] [inst_7 : SMulCommClass R R' M] [inst_8 : DistribMulAction R' N]
[inst_9 : TensorProduct.CompatibleSMul R R' M N] (r : R') (x : M) (y : N), x ⊗ₜ[R] (r • y) = r • x ⊗ₜ[R] y
This theorem, named `TensorProduct.tmul_smul`, states that for any given commutative semiring `R`, monoid `R'`, additive commutative monoids `M` and `N`, such that `M` and `N` are modules over `R`, `M` and `N` are distributive over multiplication action by `R'`, and the scalar multiplication is compatible with the tensor product, the following equality holds: for any element `r` from `R'`, and elements `x` from `M` and `y` from `N`, the tensor product of `x` and the scalar multiplication of `r` and `y` is equal to the scalar multiplication of `r` and the tensor product of `x` and `y`. In mathematical notation, this is saying that for all `r`, `x`, and `y`, \(x \otimes (r \cdot y) = r \cdot (x \otimes y)\).
More concisely: For any commutative semiring `R`, monoid `R'`, additive commutative monoids `M` and `N` being `R`-modules, and assuming distributivity and compatibility of scalar multiplication with the tensor product, the equality `x ⊗ (r * y) = r ⊗ (x ⊗ y)` holds for all `r` in `R'` and elements `x` from `M` and `y` from `N`.
|
TensorProduct.tmul_add
theorem TensorProduct.tmul_add :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n₁ n₂ : N),
m ⊗ₜ[R] (n₁ + n₂) = m ⊗ₜ[R] n₁ + m ⊗ₜ[R] n₂
This theorem states that for any commutative semiring `R`, any module `M` over `R`, any module `N` over `R`, and any elements `m` in `M` and `n₁`, `n₂` in `N`, the tensor product of `m` with the sum of `n₁` and `n₂` is equal to the sum of the tensor product of `m` with `n₁` and the tensor product of `m` with `n₂`. This is a statement of the distributive property in the context of tensor products.
More concisely: For any commutative semiring R, modules M and N, and elements m in M and n₁, n₂ in N, the tensor product m ⊗ (n₁ + n₂) is equal to the sum of the tensor products m ⊗ n₁ and m ⊗ n₂.
|
TensorProduct.induction_on
theorem TensorProduct.induction_on :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {motive : TensorProduct R M N → Prop}
(z : TensorProduct R M N),
motive 0 →
(∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)) →
(∀ (x y : TensorProduct R M N), motive x → motive y → motive (x + y)) → motive z
This theorem is an induction principle for the tensor product of two modules. In plain English, given two modules `M` and `N` over a commutative semi-ring `R`, it provides a way to prove a property `motive` for any element `z` of the tensor product of `M` and `N`. The principle states that if the property holds for the zero tensor, and if it holds for simple tensors of the form `x ⊗ₜ[R] y` (where `x` is in `M` and `y` is in `N`), and if the property is preserved under addition of tensors (i.e., if it holds for `x` and `y`, it also holds for `x + y`), then it holds for all tensors `z`. This method of proof is often useful when the property `motive` is defined in terms of the structure of the tensor product.
More concisely: If `M` and `N` are modules over a commutative semi-ring `R`, and `motive` is a property preserved under addition, if `motive` holds for the zero tensor and all simple tensors `x ⊗ₜ[R] y`, then `motive` holds for all tensors in `M ⊗ₜ[R] N`.
|
TensorProduct.ext_fourfold'
theorem TensorProduct.ext_fourfold' :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8}
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
[inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R P] [inst_9 : Module R Q]
[inst_10 : Module R S] {φ ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₗ[R] S},
(∀ (w : M) (x : N) (y : P) (z : Q), φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)) → φ = ψ
The theorem `TensorProduct.ext_fourfold'` states that for a given commutative semiring `R` and modules `M`, `N`, `P`, `Q`, and `S` over `R`, if two linear maps `φ` and `ψ` from the tensor product of `M`, `N`, `P`, and `Q` to `S` agree on all elements of the form `(m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)`, where `m` is an element of `M`, `n` is an element of `N`, `p` is an element of `P`, and `q` is an element of `Q`, then `φ` and `ψ` are equal. In other words, the equality of two such linear maps can be checked on tensor products of pairs of elements from `M`, `N`, `P`, and `Q`.
More concisely: Given commutative semirings R and modules M, N, P, Q, and S over R, if linear maps φ and ψ from M ⊗ N ⊗ P ⊗ Q to S agree on all elements of the form (m ⊗ n) ⊗ (p ⊗ q) for m ∈ M, n ∈ N, p ∈ P, and q ∈ Q, then φ = ψ.
|
TensorProduct.span_tmul_eq_top
theorem TensorProduct.span_tmul_eq_top :
∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_4) (N : Type u_5) [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} = ⊤
The theorem `TensorProduct.span_tmul_eq_top` states that for any commutative semiring `R` and any two types `M` and `N` that are both additively commutative monoids and also `R`-modules, the span of the set of all tensor products `m ⊗ₜ[R] n` (where `m` is from `M` and `n` is from `N`) is equal to the top submodule. In other words, every element in the tensor product space can be expressed as a linear combination of simple tensor products.
More concisely: For any commutative semiring `R`, and additively commutative monoids `M` and `N` that are also `R`-modules, the span of all simple tensor products `m ⊗ₜ[R] n` (where `m` is from `M` and `n` is from `N`) equals the top submodule of the tensor product space `M ⊗ₜ[R] N`.
|
TensorProduct.zero_tmul
theorem TensorProduct.zero_tmul :
∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_4) {N : Type u_5} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (n : N), 0 ⊗ₜ[R] n = 0
The theorem `TensorProduct.zero_tmul` states that for any commutative semiring `R` and types `M` and `N` which both form `R`-modules, the tensor product of zero from `M` and any element `n` from `N` is zero. In mathematical terms, given a commutative semiring `R` and `R`-modules `M` and `N`, for any `n` in `N`, `0 ⊗ₜ[R] n = 0`. This theorem establishes one of the important properties of tensor products in the context of module theory.
More concisely: For any commutative semiring `R` and `R`-modules `M` and `N`, the tensor product of the zero element in `M` and any element in `N` is the zero element in the tensor product `M ⊗ₜ[R] N`.
|
TensorProduct.ext_threefold
theorem TensorProduct.ext_threefold :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7}
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
[inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
{g h : TensorProduct R (TensorProduct R M N) P →ₗ[R] Q},
(∀ (x : M) (y : N) (z : P), g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)) → g = h
This theorem, `TensorProduct.ext_threefold`, states that for any commutative semiring `R` and any modules `M`, `N`, `P`, and `Q` over `R`, if we have two linear maps `g` and `h` from the tensor product of `M`, `N`, and `P` to `Q`, then if these two maps agree on all triples of elements `(x, y, z)` where `x` is from `M`, `y` is from `N`, and `z` is from `P`, i.e., `g ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = h ((x ⊗ₜ[R] y) ⊗ₜ[R] z)` for all `x`, `y`, `z`, then `g` and `h` are the same map, i.e., `g = h`. This is an extension property of tensor products in the context of module theory, ensuring the uniqueness of maps out of the tensor product given their values on generators.
More concisely: Given a commutative semiring R and modules M, N, P, and Q over R, if two linear maps g and h from M ⊗ N ⊗ P to Q agree on all triples of elements, then g = h.
|
TensorProduct.tmul_zero
theorem TensorProduct.tmul_zero :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} (N : Type u_5) [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M), m ⊗ₜ[R] 0 = 0
This theorem states that for any commutative semiring `R`, any type `M` that forms an `R`-module with respect to an additive commutative monoid structure, and any type `N` that also forms an `R`-module with respect to another additive commutative monoid structure, the tensor product of any element `m` of `M` and the zero element of `N` is the zero element of the tensor product space. Symbolically, this can be represented as `m ⊗ₜ[R] 0 = 0`.
More concisely: For any commutative semiring R, and for any R-module M and R-module N with additive structures, the tensor product of any element in M with the zero element in N is the zero element in the tensor product of M and N.
|
TensorProduct.map_id
theorem TensorProduct.map_id :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
TensorProduct.map LinearMap.id LinearMap.id = LinearMap.id
This theorem, `TensorProduct.map_id`, states that for any commutative semiring `R` and any two types `M` and `N` that form additively commutative monoids and are modules over `R`, the tensor product of the identity linear map with itself is equal to the identity linear map. This is a property about the identity in the context of tensor products and linear maps, similar to the idea that multiplying any number by 1 leaves it unchanged.
More concisely: For any commutative semiring `R`, and modules `M` and `N` over `R` that form additively commutative monoids, the identity linear map from `M` to itself, tensored with itself, is equal to the identity linear map from `M` to `M` and from `N` to itself, tensored with itself, in the tensor product `M ⊗ N` over `R`.
|
TensorProduct.smul_tmul'
theorem TensorProduct.smul_tmul' :
∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_2} [inst_1 : Monoid R'] {M : Type u_4} {N : Type u_5}
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : DistribMulAction R' M] [inst_7 : SMulCommClass R R' M] (r : R') (m : M) (n : N),
r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
This theorem states that for any commutative semiring `R`, monoid `R'`, and modules `M` and `N` over `R`, if `M` also has a distributive multiplication action by `R'` and `R'` and `R` commute under scalar multiplication on `M`, then for any elements `r` in `R'`, `m` in `M`, and `n` in `N`, the scalar multiplication of `r` and tensor product of `m` and `n` is equal to the tensor product of the scalar multiplication of `r` and `m` and `n`. In mathematical notation, this can be expressed as $r \cdot (m \otimes n) = (r \cdot m) \otimes n$.
More concisely: For any commutative semiring `R`, monoid `R'`, and modules `M` and `N` over `R` with distributive `R'`-actions on `M`, if `R'` and `R` commute under scalar multiplication on `M`, then for all `r` in `R'`, `m` in `M`, and `n` in `N`, $r \cdot (m \otimes n) = (r \cdot m) \otimes n$.
|
TensorProduct.map_comp_comm_eq
theorem TensorProduct.map_comp_comm_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7}
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
[inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (f : M →ₗ[R] P)
(g : N →ₗ[R] Q),
TensorProduct.map f g ∘ₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R Q P) ∘ₗ TensorProduct.map g f
This theorem states that for any given commutative semiring `R` and modules `M`, `N`, `P`, and `Q` over `R`, if we have linear maps `f: M → P` and `g: N → Q`, then the operation of applying the tensor product map `f ⊗ g` to the tensor product `M ⊗ N`, when identified with `N ⊗ M`, is the same as applying the tensor product map `g ⊗ f` to the tensor product `N ⊗ M`, when identified with `M ⊗ N`. In other words, under the mentioned identifications, the operation of tensoring commutes with the operation of applying linear maps, hence the name `map_comp_comm_eq`. This is a statement about the commutativity of tensor product of modules up to linear equivalence.
More concisely: For any commutative semirings `R`, and modules `M`, `N`, `P`, and `Q` over `R`, the application of linear maps `f: M → P` and `g: N → Q` to the tensor product `M ⊗ N` identified with `N ⊗ M`, commutes up to linear equivalence, i.e., `(f ⊗ g) (M ⊗ N) = (g ⊗ f) (N ⊗ M)`.
|
TensorProduct.lift.tmul
theorem TensorProduct.lift.tmul :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : Module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N), (TensorProduct.lift f) (x ⊗ₜ[R] y) = (f x) y
This theorem states that for any commutative semiring 'R', types 'M', 'N', and 'P' each with a commutative monoid addition and a 'R'-module structure, and a bilinear map 'f' from 'M' to 'N' into 'P', the 'lift' of 'f' applied to the tensor product of elements 'x' from 'M' and 'y' from 'N' is equal to the evaluation of 'f' at 'x' and 'y'. In other words, lifting a bilinear map to the tensor product space and applying it to a tensor is the same as applying the original map to the components of the tensor.
More concisely: For any commutative semiring 'R', and bilinear map 'f' from a commutative monoid 'M' with 'R'-module structure to commutative monoids 'N' and 'P' with 'R'-module structures, the lifting of 'f' to the tensor product 'M ⊗ N' satisfies 'f (x ⊗ y) = f x ⊗ y' for all 'x' in 'M' and 'y' in 'N'.
|
TensorProduct.ext
theorem TensorProduct.ext :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : Module R P] {g h : TensorProduct R M N →ₗ[R] P},
(TensorProduct.mk R M N).compr₂ g = (TensorProduct.mk R M N).compr₂ h → g = h
The theorem `TensorProduct.ext` states that for any commutative semiring `R`, and any modules `M`, `N`, `P` over `R`, if two linear maps `g` and `h` from the tensor product of `M` and `N` over `R` to `P` are such that the composition of each map with the canonical bilinear map from `M` and `N` to their tensor product is the same, then the two linear maps `g` and `h` are equal. In more compact terms, if `LinearMap.compr₂ (TensorProduct.mk R M N) g = LinearMap.compr₂ (TensorProduct.mk R M N) h`, then `g = h`. This theorem provides a criterion for equality of linear maps in terms of their compositions with a specific bilinear map.
More concisely: If `g` and `h` are linear maps from the tensor product of modules `M` and `N` over a commutative semiring `R` to module `P`, and `LinearMap.compr₂ (TensorProduct.mk R M N) g = LinearMap.compr₂ (TensorProduct.mk R M N) h`, then `g = h`.
|
TensorProduct.add_tmul
theorem TensorProduct.add_tmul :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m₁ m₂ : M) (n : N),
(m₁ + m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n + m₂ ⊗ₜ[R] n
This theorem states that for any commutative semiring `R`, and any types `M` and `N` that are both commutative monoids and `R`-modules, the tensor product of the sum of two elements `m₁` and `m₂` from `M` and an element `n` from `N` is equal to the sum of the tensor product of `m₁` and `n` and the tensor product of `m₂` and `n`. In mathematical terms, this can be written as $(m₁ + m₂) \otimes n = m₁ \otimes n + m₂ \otimes n$. This theorem shows that the tensor product operation respects the addition operation from the module structure.
More concisely: For any commutative semiring `R`, and `R`-modules `M` and `N` as commutative monoids, $(m\_1 + m\_2) \otimes n = m\_1 \otimes n + m\_2 \otimes n$ holds for all `m_1, m_2 ∈ M` and `n ∈ N`.
|
TensorProduct.map_map_comp_assoc_eq
theorem TensorProduct.map_map_comp_assoc_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8}
{T : Type u_9} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P]
[inst_4 : AddCommMonoid Q] [inst_5 : AddCommMonoid S] [inst_6 : AddCommMonoid T] [inst_7 : Module R M]
[inst_8 : Module R N] [inst_9 : Module R P] [inst_10 : Module R Q] [inst_11 : Module R S] [inst_12 : Module R T]
(f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T),
TensorProduct.map f (TensorProduct.map g h) ∘ₗ ↑(TensorProduct.assoc R M N P) =
↑(TensorProduct.assoc R Q S T) ∘ₗ TensorProduct.map (TensorProduct.map f g) h
The theorem `TensorProduct.map_map_comp_assoc_eq` states that given the linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, along with the associative nature of tensor products, the composition of `f` and the tensor product of `g` and `h` is the same as the tensor product of `f` and `g`, and `h`, when we regard `(M ⊗ N) ⊗ P` as `M ⊗ (N ⊗ P)` and `(Q ⊗ S) ⊗ T` as `Q ⊗ (S ⊗ T)`. That is, `f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h`.
More concisely: The theorem asserts that the composition of a linear map with the tensor product of two other linear maps is equal to the tensor product of the first map with the second and third maps, when the tensor products are associated accordingly.
|
TensorProduct.smul_add
theorem TensorProduct.smul_add :
∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_2} [inst_1 : Monoid R'] {M : Type u_4} {N : Type u_5}
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : DistribMulAction R' M] [inst_7 : SMulCommClass R R' M] (r : R') (x y : TensorProduct R M N),
r • (x + y) = r • x + r • y
This theorem states that for any commutative semiring `R`, another type `R'` which is a monoid, and modules `M` and `N` over `R` (where `M` is also an `R'`-module and the scalar multiplication on `M` commutes with the ring multiplication of `R`), scalar multiplication distributes over the addition of tensor products. In mathematical notation, for any scalar `r` in `R'` and any two tensor products `x` and `y` in `M ⊗ N`, we have `r • (x + y) = r • x + r • y`.
More concisely: For any commutative semiring `R`, `R'-module `M` over `R`, and modules `N` over `R` with commuting scalar multiplication, the scalar multiplication on `M` distributes over the tensor product addition, that is, `r • (x ⊗ y) = r • x ⊗ y + r • x' ⊗ y'` for all `r` in `R'`, and `x, x'` in `M`, and `y, y'` in `N`.
|
TensorProduct.smul_zero
theorem TensorProduct.smul_zero :
∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_2} [inst_1 : Monoid R'] {M : Type u_4} {N : Type u_5}
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : DistribMulAction R' M] [inst_7 : SMulCommClass R R' M] (r : R'), r • 0 = 0
The theorem `TensorProduct.smul_zero` asserts that for any commutative semiring `R`, monoid `R'`, types `M` and `N` that form additive commutative monoids and `R`-modules, and type `M` is a `R'`-distributive mul-action where `R` and `R'` commute on `M`, scalar multiplication of any element `r` from `R'` and the zero element from `M` (denoted as `0`) always gives us the zero element. This is a generalization of the property in linear algebra where scalar multiplication of any scalar and the zero vector yields the zero vector.
More concisely: For any commutative semiring `R`, monoid `R'`, additive commutative monoids `M` and `N`, and `R`-modules `M` with `R'`-distributive and commuting actions, `r * 0 = 0` for all `r` in `R'`.
|
TensorProduct.lid_tmul
theorem TensorProduct.lid_tmul :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
(r : R), (TensorProduct.lid R M) (r ⊗ₜ[R] m) = r • m
The theorem `TensorProduct.lid_tmul` states that for any commutative semiring `R`, any module `M` over `R`, and any elements `m` in `M` and `r` in `R`, applying the left identity operation of the tensor product (`TensorProduct.lid R M`) to the tensor product of `r` and `m` (`r ⊗ₜ[R] m`) is equivalent to scalar multiplication of `m` by `r` (`r • m`). This essentially says that the scalar can be "pulled out" of the tensor product, reinforcing the idea that the base ring behaves like a left identity for the tensor product of modules, up to a linear equivalence.
More concisely: For any commutative semiring `R`, module `M` over `R`, and elements `m in M` and `r in R`, `r ⊗ₜ[R] m = TensorProduct.lid R M r ⊗ₜ[R] m` is equivalent to `r • m`.
|
TensorProduct.map_map_comp_assoc_symm_eq
theorem TensorProduct.map_map_comp_assoc_symm_eq :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_7} {S : Type u_8}
{T : Type u_9} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P]
[inst_4 : AddCommMonoid Q] [inst_5 : AddCommMonoid S] [inst_6 : AddCommMonoid T] [inst_7 : Module R M]
[inst_8 : Module R N] [inst_9 : Module R P] [inst_10 : Module R Q] [inst_11 : Module R S] [inst_12 : Module R T]
(f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T),
TensorProduct.map (TensorProduct.map f g) h ∘ₗ ↑(TensorProduct.assoc R M N P).symm =
↑(TensorProduct.assoc R Q S T).symm ∘ₗ TensorProduct.map f (TensorProduct.map g h)
This theorem is about the associativity of tensor product mappings in the context of linear algebra over a commutative semiring. Given three linear maps `f` mapping `M` to `Q`, `g` mapping `N` to `S`, and `h` mapping `P` to `T`, and provided that the tensor products `M ⊗ (N ⊗ P)` and `Q ⊗ (S ⊗ T)` are identified with `(M ⊗ N) ⊗ P` and `(Q ⊗ S) ⊗ T` respectively, this theorem states that the composition of tensor product mappings `(f ⊗ g) ⊗ h` and `f ⊗ (g ⊗ h)` are equal. This is a fundamental property of tensor products in linear algebra, underlining their associative nature.
More concisely: Given three linear maps `f: M -> Q`, `g: N -> S`, and `h: P -> T` over a commutative semiring, the compositions `(f ⊗ g) ⊗ h` and `f ⊗ (g ⊗ h)` of their tensor product mappings are equal.
|
TensorProduct.smul_tmul
theorem TensorProduct.smul_tmul :
∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_2} [inst_1 : Monoid R'] {M : Type u_4} {N : Type u_5}
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : DistribMulAction R' M] [inst_7 : DistribMulAction R' N] [inst_8 : TensorProduct.CompatibleSMul R R' M N]
(r : R') (m : M) (n : N), (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)
This theorem states that for any commutative semiring `R`, any monoid `R'`, and any two modules `M` and `N` over `R` that also have a distribution action of `R'`, the scalar multiplication `smul` can be moved from one side of the tensor product to the other. More specifically, for any element `r` from `R'`, `m` from `M` and `n` from `N`, the tensor product of the scalar multiplication of `r` and `m` with `n` is equal to the tensor product of `m` with the scalar multiplication of `r` and `n`, given that the scalar multiplication and tensor product are compatible.
More concisely: For any commutative semiring `R`, monoid `R'`, and modules `M` and `N` over `R` with a distribution action of `R'`, the scalar multiplication of `R'` commutes with the tensor product of `M` and `N`, i.e., `r * (m ⊤ n) = (r * m) ⊤ n` for all `r` in `R`, `m` in `M`, and `n` in `N`.
|
TensorProduct.ext'
theorem TensorProduct.ext' :
∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : Module R P] {g h : TensorProduct R M N →ₗ[R] P},
(∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) → g = h
The theorem `TensorProduct.ext'` states that for any commutative semiring `R` and any three modules `M`, `N`, and `P` over `R`, if two linear maps `g` and `h` from the tensor product of `M` and `N` to `P` have the same value for every pair of elements `x` from `M` and `y` from `N` in their tensor product, then these two maps `g` and `h` are the same. The tensor product here is denoted by `x ⊗ₜ[R] y`.
More concisely: If two linear maps from the tensor product of two R-modules agree on all pairs of their arguments, then they are equal.
|