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))
Instances For
instance
FreeAlgebra.instFreeFreeAlgebraToSemiringInstAddCommMonoidToModuleInstSemiringFreeAlgebraInstAlgebraId
(R : Type u)
(X : Type v)
[CommSemiring R]
:
Module.Free R (FreeAlgebra R X)
Equations
- (_ : Module.Free R (FreeAlgebra R X)) = (_ : 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))