Results on bases of tensor products

In the file we construct a basis for the base change of a module to an algebra, and deduce that Module.Free is stable under base change.

Main declarations

• Algebra.TensorProduct.basis: given a basis of a module M over a commutative semiring R, and an R-algebra A, this provides a basis for A ⊗[R] M over A.
• Algebra.TensorProduct.instFree: if M is free, then so is A ⊗[R] M.

noncomputable def Algebra.TensorProduct.basisAux {R : Type u_1} (A : Type u_2) {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) : TensorProduct R A M ≃ₗ[R] ι →₀ A

Given an R-algebra A and an R-basis of M, this is an R-linear isomorphism A ⊗[R] M ≃ (ι →₀ A) (which is in fact A-linear).

Equations

• One or more equations did not get rendered due to their size.

theorem Algebra.TensorProduct.basisAux_tmul {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (m : M) : (basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

theorem Algebra.TensorProduct.basisAux_map_smul {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (x : TensorProduct R A M) : (basisAux A b) (a • x) = a • (basisAux A b) x

noncomputable def Algebra.TensorProduct.basis {R : Type u_1} (A : Type u_2) {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) : Module.Basis ι A (TensorProduct R A M)

Given an R-algebra A, this is the A-basis of A ⊗[R] M induced by an R-basis of M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.TensorProduct.basis_repr_tmul {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (m : M) : (basis A b).repr (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

theorem Algebra.TensorProduct.basis_repr_symm_apply {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (i : ι) : (basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)

@[simp]

theorem Algebra.TensorProduct.basis_apply {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (i : ι) : (basis A b) i = 1 ⊗ₜ[R] b i

theorem Algebra.TensorProduct.basis_repr_symm_apply' {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M) (a : A) (i : ι) : a • (basis A b) i = a ⊗ₜ[R] b i

theorem Module.Basis.baseChange_linearMap {R : Type u_1} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] {ι' : Type u_3} {N : Type u_4} [Fintype ι'] [DecidableEq ι'] [AddCommMonoid N] [Module R N] (A : Type u_5) [CommSemiring A] [Algebra R A] (b : Basis ι R M) (b' : Basis ι' R N) (ij : ι × ι') : LinearMap.baseChange A ((b'.linearMap b) ij) = ((Algebra.TensorProduct.basis A b').linearMap (Algebra.TensorProduct.basis A b)) ij

theorem Module.Basis.baseChange_end {R : Type u_1} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (A : Type u_5) [CommSemiring A] [Algebra R A] [DecidableEq ι] (b : Basis ι R M) (ij : ι × ι) : LinearMap.baseChange A (b.end ij) = (Algebra.TensorProduct.basis A b).end ij

instance Algebra.TensorProduct.instFree (R : Type u_3) (A : Type u_4) (M : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [CommSemiring A] [Algebra R A] : Module.Free A (TensorProduct R A M)

@[simp]

theorem LinearMap.toMatrix_baseChange {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} {ι₂ : Type u_5} (A : Type u_6) [Fintype ι] [Finite ι₂] [DecidableEq ι] [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (b₁ : Module.Basis ι R M₁) (b₂ : Module.Basis ι₂ R M₂) : (toMatrix (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂)) (baseChange A f) = ((toMatrix b₁ b₂) f).map ⇑(algebraMap R A)