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 = Finsupp.basisSingleOne.map FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toLinearEquiv
Instances For
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) ≤ Cardinal.mk ↑s ⊔ Cardinal.aleph0