mathlib documentation

linear_algebra.free_algebra

Linear algebra properties of free_algebra R X #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
noncomputable def free_algebra.basis_free_monoid (R : Type u) (X : Type v) [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) (X : Type v) [comm_ring R] (ᾰ : free_monoid X →₀ R) :
⇑((free_algebra.basis_free_monoid R X).repr.symm) ᾰ = ⇑(free_algebra.equiv_monoid_algebra_free_monoid.symm) ᾰ
source
@[simp]
theorem free_algebra.basis_free_monoid_repr_apply (R : Type u) (X : Type v) [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.rank_eq {K : Type u} {X : Type (max u v)} [field K] :
module.rank K (free_algebra K X) = cardinal.mk (list X)