Linear algebra properties of FreeAlgebra R X

This file provides a FreeMonoid X basis on the FreeAlgebra R X, and uses it to show the dimension of the algebra is the cardinality of List X

noncomputable def FreeAlgebra.basisFreeMonoid (R : Type u) (X : Type v) [CommSemiring R] : Basis (FreeMonoid X) R (FreeAlgebra R X)

The FreeMonoid X basis on the FreeAlgebra R X, mapping [x₁, x₂, ..., xₙ] to the "monomial" 1 • x₁ * x₂ * ⋯ * xₙ

Equations

• FreeAlgebra.basisFreeMonoid R X = Basis.map Finsupp.basisSingleOne (AlgEquiv.toLinearEquiv (AlgEquiv.symm FreeAlgebra.equivMonoidAlgebraFreeMonoid))

instance FreeAlgebra.instFreeFreeAlgebraToSemiringInstAddCommMonoidToModuleInstSemiringFreeAlgebraInstAlgebraId (R : Type u) (X : Type v) [CommSemiring R] : Module.Free R (FreeAlgebra R X)

Equations

• ⋯ = ⋯

theorem FreeAlgebra.rank_eq (R : Type u) (X : Type v) [CommRing R] [Nontrivial R] : Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))