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] : Module.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 = Finsupp.basisSingleOne.map ((↑FreeAlgebra.equivMonoidAlgebraFreeMonoid).trans (MonoidAlgebra.coeffLinearEquiv R)).symm

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

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))

theorem Algebra.rank_adjoin_le {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (s : Set S) : Module.rank R ↥(adjoin R s) ≤ max (Cardinal.mk ↑s) Cardinal.aleph0