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 Module.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 Module.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 Module.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 Module.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 Module.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

• Module.Basis.baseChange S b = ((Module.Basis.singleton Unit S).tensorProduct b).reindex (Equiv.punitProd ι)

@[simp]

theorem Module.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 Module.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 κ] (𝒞 : Module.Basis κ R N) : TensorProduct R M N ≃ₗ[R] κ →₀ M

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

• TensorProduct.equivFinsuppOfBasisRight 𝒞 = (LinearEquiv.lTensor M 𝒞.repr).trans (TensorProduct.finsuppScalarRight R M κ)

@[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 κ] (𝒞 : Module.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 κ] (𝒞 : Module.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 κ] (𝒞 : Module.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 κ] (𝒞 : Module.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] (𝒞 : Module.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] (𝒞 : Module.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 ι] (ℬ : Module.Basis ι R M) : TensorProduct R M N ≃ₗ[R] ι →₀ N

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

• TensorProduct.equivFinsuppOfBasisLeft ℬ = (TensorProduct.comm R M N).trans (TensorProduct.equivFinsuppOfBasisRight ℬ)

@[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 ι] (ℬ : Module.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 ι] (ℬ : Module.Basis ι R M) (m : M) (n : N) (i : ι) : ((equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) i = (ℬ.repr m) i • n

theorem TensorProduct.equivFinsuppOfBasisRight_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 κ] (𝒞 : Module.Basis κ R N) (x : TensorProduct R M N) (i : κ) : ((equivFinsuppOfBasisRight 𝒞) x) i = (TensorProduct.rid R M) ((LinearMap.lTensor M (𝒞.coord i)) x)

Given a basis 𝒞 of N, x ∈ M ⊗ N can be written as ∑ᵢ mᵢ ⊗ 𝒞 i. The coefficient mᵢ equals the i-th coordinate functional applied to the right tensor factor.

theorem TensorProduct.equivFinsuppOfBasisLeft_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 ι] (ℬ : Module.Basis ι R M) (x : TensorProduct R M N) (i : ι) : ((equivFinsuppOfBasisLeft ℬ) x) i = (TensorProduct.lid R N) ((LinearMap.rTensor N (ℬ.coord i)) x)

Given a basis ℬ of M, x ∈ M ⊗ N can be written as ∑ᵢ ℬ i ⊗ nᵢ. The coefficient nᵢ equals the i-th coordinate functional applied to the left tensor factor.

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 ι] (ℬ : Module.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 ι] (ℬ : Module.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] (𝒞 : Module.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] (ℬ : Module.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] (ℬ : Module.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] (ℬ : Module.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} {S : Type u_2} {M : Type u_3} {N : Type u_4} [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] : Free S (TensorProduct R M N)