A basis for TensorAlgebra R M

Main definitions

• TensorAlgebra.equivMonoidAlgebra b : TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ: the isomorphism given by a basis b : Basis κ R M.
• Basis.tensorAlgebra b : Basis (FreeMonoid κ) R (TensorAlgebra R M): the basis on the tensor algebra given by a basis b : Basis κ R M.

Main results

• TensorAlgebra.instFreeModule: the tensor algebra over M is free when M is
• TensorAlgebra.rank_eq

noncomputable def TensorAlgebra.equivFreeAlgebra {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ

A basis provides an algebra isomorphism with the free algebra, replacing each basis vector with its index.

@[simp]

theorem TensorAlgebra.equivFreeAlgebra_ι_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (i : κ) : ↑(TensorAlgebra.equivFreeAlgebra b) (↑(TensorAlgebra.ι R) (↑b i)) = FreeAlgebra.ι R i

@[simp]

theorem TensorAlgebra.equivFreeAlgebra_symm_ι {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (i : κ) : ↑(AlgEquiv.symm (TensorAlgebra.equivFreeAlgebra b)) (FreeAlgebra.ι R i) = ↑(TensorAlgebra.ι R) (↑b i)

@[simp]

theorem Basis.tensorAlgebra_repr_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : ∀ (a : TensorAlgebra R M), ↑(Basis.tensorAlgebra b).repr a = ↑(FreeAlgebra.basisFreeMonoid R κ).repr (↑(TensorAlgebra.equivFreeAlgebra b) a)

noncomputable def Basis.tensorAlgebra {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) : Basis (FreeMonoid κ) R (TensorAlgebra R M)

A basis on M can be lifted to a basis on TensorAlgebra R M

instance TensorAlgebra.instModuleFree {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] : Module.Free R (TensorAlgebra R M)

TensorAlgebra R M is free when M is.

theorem TensorAlgebra.rank_eq {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial R] [Module.Free R M] : Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)