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

Equations

• TensorAlgebra.equivFreeAlgebra b = AlgEquiv.ofAlgHom ((TensorAlgebra.lift R) (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ ↑b.repr)) ((FreeAlgebra.lift R) (⇑(TensorAlgebra.ι R) ∘ ⇑b)) ⋯ ⋯

@[simp]

theorem TensorAlgebra.equivFreeAlgebra_ι_apply {κ : Type uκ} {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R M) (i : κ) : (equivFreeAlgebra b) ((ι 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 : Module.Basis κ R M) (i : κ) : (equivFreeAlgebra b).symm (FreeAlgebra.ι R i) = (ι R) (b i)

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

Equations

• b.tensorAlgebra = (FreeAlgebra.basisFreeMonoid R κ).map ↑(TensorAlgebra.equivFreeAlgebra b).symm

@[simp]

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

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.

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

The TensorAlgebra of a free module over a commutative semiring with no zero-divisors has no zero-divisors.

instance TensorAlgebra.instIsDomain {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [Module.Free R M] : IsDomain (TensorAlgebra R M)

The TensorAlgebra of a free module over an integral domain is a domain.

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)