Documentation

Mathlib.LinearAlgebra.TensorProduct.Basis

Bases and dimensionality of tensor products of modules #

This file defines various bases on the tensor product of modules, and shows that the tensor product of free modules is again free.

def Basis.tensorProduct {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) :
Basis (ι × κ) S (TensorProduct R M N)

If b : ι → M and c : κ → N are bases then so is fun i ↦ b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Basis.tensorProduct_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (i : ι) (j : κ) :
(b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j
theorem Basis.tensorProduct_apply' {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) :
(b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2
@[simp]
theorem Basis.tensorProduct_repr_tmul_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) :
((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j (b.repr m) i
noncomputable def Basis.baseChange {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) :
Basis ι S (TensorProduct R S M)

The lift of an R-basis of M to an S-basis of the base change S ⊗[R] M.

Equations
@[simp]
theorem Basis.baseChange_repr_tmul {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (x : S) (y : M) (i : ι) :
((baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i x
@[simp]
theorem Basis.baseChange_apply {R : Type u_1} {M : Type u_3} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Type u_7) [Semiring S] [Algebra R S] (b : Basis ι R M) (i : ι) :
(baseChange S b) i = 1 ⊗ₜ[R] b i
def TensorProduct.equivFinsuppOfBasisRight {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) :

If {𝒞ᵢ} is a basis for the module N, then every elements of x ∈ M ⊗ N can be uniquely written as ∑ᵢ mᵢ ⊗ 𝒞ᵢ for some mᵢ ∈ M.

Equations
@[simp]
theorem TensorProduct.equivFinsuppOfBasisRight_apply_tmul {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (m : M) (n : N) :
(equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun (x : R) => x m) (𝒞.repr n)
theorem TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (m : M) (n : N) (i : κ) :
((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) i = (𝒞.repr n) i m
theorem TensorProduct.equivFinsuppOfBasisRight_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) :
(equivFinsuppOfBasisRight 𝒞).symm = (Finsupp.lsum R) fun (i : κ) => (mk R M N).flip (𝒞 i)
@[simp]
theorem TensorProduct.equivFinsuppOfBasisRight_symm_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq κ] (𝒞 : Basis κ R N) (b : κ →₀ M) :
(equivFinsuppOfBasisRight 𝒞).symm b = b.sum fun (i : κ) (m : M) => m ⊗ₜ[R] 𝒞 i
theorem TensorProduct.sum_tmul_basis_right_injective {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (𝒞 : Basis κ R N) :
Function.Injective ((Finsupp.lsum R) fun (i : κ) => (mk R M N).flip (𝒞 i))
theorem TensorProduct.sum_tmul_basis_right_eq_zero {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (𝒞 : Basis κ R N) (b : κ →₀ M) (h : (b.sum fun (i : κ) (m : M) => m ⊗ₜ[R] 𝒞 i) = 0) :
b = 0
def TensorProduct.equivFinsuppOfBasisLeft {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] ( : Basis ι R M) :

If {ℬᵢ} is a basis for the module M, then every elements of x ∈ M ⊗ N can be uniquely written as ∑ᵢ ℬᵢ ⊗ nᵢ for some nᵢ ∈ N.

Equations
@[simp]
theorem TensorProduct.equivFinsuppOfBasisLeft_apply_tmul {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] ( : Basis ι R M) (m : M) (n : N) :
(equivFinsuppOfBasisLeft ) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun (x : R) => x n) (.repr m)
theorem TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] ( : Basis ι R M) (m : M) (n : N) (i : ι) :
((equivFinsuppOfBasisLeft ) (m ⊗ₜ[R] n)) i = (.repr m) i n
theorem TensorProduct.equivFinsuppOfBasisLeft_symm {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] ( : Basis ι R M) :
(equivFinsuppOfBasisLeft ).symm = (Finsupp.lsum R) fun (i : ι) => (mk R M N) ( i)
@[simp]
theorem TensorProduct.equivFinsuppOfBasisLeft_symm_apply {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq ι] ( : Basis ι R M) (b : ι →₀ N) :
(equivFinsuppOfBasisLeft ).symm b = b.sum fun (i : ι) (n : N) => i ⊗ₜ[R] n
theorem TensorProduct.eq_repr_basis_right {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (𝒞 : Basis κ R N) (x : TensorProduct R M N) :
∃ (b : κ →₀ M), (b.sum fun (i : κ) (m : M) => m ⊗ₜ[R] 𝒞 i) = x

Elements in M ⊗ N can be represented by sum of elements in M tensor elements of basis of N.

theorem TensorProduct.eq_repr_basis_left {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] ( : Basis ι R M) (x : TensorProduct R M N) :
∃ (c : ι →₀ N), (c.sum fun (i : ι) (n : N) => i ⊗ₜ[R] n) = x

Elements in M ⊗ N can be represented by sum of elements of basis of M tensor elements of N.

theorem TensorProduct.sum_tmul_basis_left_injective {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] ( : Basis ι R M) :
Function.Injective ((Finsupp.lsum R) fun (i : ι) => (mk R M N) ( i))
theorem TensorProduct.sum_tmul_basis_left_eq_zero {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] ( : Basis ι R M) (b : ι →₀ N) (h : (b.sum fun (i : ι) (n : N) => i ⊗ₜ[R] n) = 0) :
b = 0
instance Module.Free.tensor {R : Type u_1} {M : Type u_3} {N : Type u_4} {S : Type u_7} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Free S M] [AddCommMonoid N] [Module R N] [Free R N] :