The coordinates of the standard basis of a monoid algebra

Mathlib defines the standard basis MonoidAlgebra.basis X k of k[X] by repr := MonoidAlgebra.coeffLinearEquiv _ but records no lemma for the resulting repr. This file is that missing bridge: the coordinates in the standard basis are the coefficients.

It is all that is needed for the generic basis API -- Module.Basis.coe_sumCoords, Module.Basis.sumCoords_self_apply, LinearMap.toMatrix_apply -- to compute in terms of MonoidAlgebra.coeff.

Main statements

• TauCeti.MonoidAlgebra.basis_repr: the coordinates of k[X] in the standard basis are the coefficients.
• TauCeti.MonoidAlgebra.coeff_basis_toDualEquiv_symm_apply: the coefficients under the standard-basis dual equivalence are evaluations on basis vectors.
• TauCeti.MonoidAlgebra.sumCoords_basis_surjective: the coefficient sum is surjective when the index type is nonempty.
• TauCeti.MonoidAlgebra.ker_sumCoords_basis_eq_span: its kernel is spanned by differences of basis vectors from a fixed one.

@[simp]

theorem TauCeti.MonoidAlgebra.basis_repr {k : Type u_1} [Semiring k] {X : Type u_2} (v : MonoidAlgebra k X) : (MonoidAlgebra.basis X k).repr v = v.coeff

The coordinates of k[X] in the standard basis are the coefficients.

@[simp]

theorem TauCeti.MonoidAlgebra.coeff_basis_toDualEquiv_symm_apply {k : Type u_1} [CommSemiring k] {X : Type u_2} [Finite X] (f : Module.Dual k (MonoidAlgebra k X)) (x : X) : ((MonoidAlgebra.basis X k).toDualEquiv.symm f).coeff x = f (MonoidAlgebra.single x 1)

The coefficients of the vector corresponding to a functional under the standard-basis identification k[X] ≃ Hom_k(k[X], k) are the values of the functional on the basis.

The sum of the coefficients

theorem TauCeti.MonoidAlgebra.sumCoords_basis_surjective {k : Type u_1} [Semiring k] {X : Type u_2} [Nonempty X] : Function.Surjective ⇑(MonoidAlgebra.basis X k).sumCoords

The sum of the coefficients is surjective when the index type is nonempty.

theorem TauCeti.MonoidAlgebra.ker_sumCoords_basis_eq_span (k : Type u_1) [Ring k] (X : Type u_2) (x₀ : X) : (MonoidAlgebra.basis X k).sumCoords.ker = Submodule.span k (Set.range fun (x : X) => MonoidAlgebra.single x 1 - MonoidAlgebra.single x₀ 1)

The kernel of the coefficient sum is spanned by the differences of the standard basis vectors from a fixed one.