The Connes–Kreimer algebra is a symmetric algebra

As an algebra, ConnesKreimer R T is the symmetric algebra on the free module with basis T, as MvPolynomial is (IsSymmetricAlgebra.mvPolynomial). The carrier stays a separate type: it carries the admissible-cut Bialgebra, while SymmetricAlgebra carries the one in which every generator is primitive.

Main results

• IsSymmetricAlgebra.connesKreimer: for a basis b of M indexed by T, the linear map sending b t to the tree t exhibits ConnesKreimer R T as the symmetric algebra on M.

References

• [CK98]

theorem IsSymmetricAlgebra.connesKreimer {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] (b : Module.Basis T R M) : IsSymmetricAlgebra ((b.constr R) ConnesKreimer.ofTree)

ConnesKreimer R T is the symmetric algebra on a module with basis T, each basis vector going to its tree.