mathlib documentation

linear_algebra.free_algebra

Linear algebra properties of free_algebra R X #

This file provides a free_monoid X basis on the free_algebra R X, and uses it to show the dimension of the algebra is the cardinality of list X

source
def free_algebra.basis_free_monoid (R : Type u_1) (X : Type u_2) [comm_ring R] :
basis (free_monoid X) R (free_algebra R X)

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

Equations
source
@[simp]
theorem free_algebra.basis_free_monoid_repr_symm_apply (R : Type u_1) (X : Type u_2) [comm_ring R] (ᾰ : free_monoid X →₀ R) :
⇑((free_algebra.basis_free_monoid R X).repr.symm) ᾰ = ⇑(free_algebra.equiv_monoid_algebra_free_monoid.to_linear_equiv.to_equiv.symm) (⇑((linear_equiv.refl R (free_monoid X →₀ R)).to_equiv.symm) ᾰ)
source
@[simp]
theorem free_algebra.basis_free_monoid_repr_apply (R : Type u_1) (X : Type u_2) [comm_ring R] (ᾰ : free_algebra R X) :
⇑((free_algebra.basis_free_monoid R X).repr) ᾰ = ⇑free_algebra.equiv_monoid_algebra_free_monoid ᾰ
source
theorem free_algebra.dim_eq {K : Type u_1} {X : Type (max u_1 u_2)} [field K] :
module.rank K (free_algebra K X) = # (list X)