The Grossman–Larson algebra

This file proves that the Grossman–Larson product is associative, makes GrossmanLarson R α an R-algebra, and maps the pre-Lie algebra of trees into it as a Lie algebra.

Main results

• UnorderedTree.productMultiset_assoc: the product is associative on basis forests.
• GrossmanLarson.product_assoc: (x ⋆ y) ⋆ z = x ⋆ (y ⋆ z).
• GrossmanLarson.instSemiring, GrossmanLarson.instAlgebra, GrossmanLarson.instRing.
• GrossmanLarson.ιLie: the one-tree forests as a map of Lie algebras from the commutator of the grafting product to the commutator of the Grossman–Larson product. It extends to the map UniversalEnvelopingAlgebra.lift R ιLie from the enveloping algebra.

Implementation notes

Associativity is proved over ℤ by duality: the product is the transpose of the pruning coproduct under the symmetry-weighted pairing (Coproduct/PruningDuality.lean), which is coassociative, and over ℤ the pairing separates points. The structure constants are natural numbers, so the ℤ case is an identity of multisets of forests, which gives associativity over every commutative semiring.

TODO

• UniversalEnvelopingAlgebra.lift R ιLie is an isomorphism: Oudom and Guin's identification of their product with the enveloping algebra. Injectivity needs the Poincaré–Birkhoff–Witt theorem.

References

• [GL89]
• [OG08]
• [Foi21]

theorem UnorderedTree.productMultiset_assoc {α : Type u_1} (F G H : Multiset (UnorderedTree α)) : ((productMultiset F G).bind fun (x : Multiset (UnorderedTree α)) => productMultiset x H) = (productMultiset G H).bind fun (x : Multiset (UnorderedTree α)) => productMultiset F x

The Grossman–Larson product is associative on basis forests, multiplicities included.

theorem GrossmanLarson.product_assoc {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y z : ConnesKreimer R (UnorderedTree α)) : (product ((product x) y)) z = (product x) ((product y) z)

The Grossman–Larson product is associative.

@[instance_reducible]

noncomputable instance GrossmanLarson.instSemiring {R : Type u_1} [CommSemiring R] {α : Type u_2} : Semiring (GrossmanLarson R α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance GrossmanLarson.instAlgebra {R : Type u_1} [CommSemiring R] {α : Type u_2} : Algebra R (GrossmanLarson R α)

Equations

• GrossmanLarson.instAlgebra = Algebra.ofModule ⋯ ⋯

@[instance_reducible]

noncomputable instance GrossmanLarson.instNeg {α : Type u_2} {R : Type u_3} [CommRing R] : Neg (GrossmanLarson R α)

Equations

• GrossmanLarson.instNeg = { neg := fun (x : GrossmanLarson R α) => { toConnesKreimer := -x.toConnesKreimer } }

@[instance_reducible]

noncomputable instance GrossmanLarson.instSub {α : Type u_2} {R : Type u_3} [CommRing R] : Sub (GrossmanLarson R α)

Equations

• GrossmanLarson.instSub = { sub := fun (x y : GrossmanLarson R α) => { toConnesKreimer := x.toConnesKreimer - y.toConnesKreimer } }

@[simp]

theorem GrossmanLarson.toConnesKreimer_neg {α : Type u_2} {R : Type u_3} [CommRing R] (x : GrossmanLarson R α) : (-x).toConnesKreimer = -x.toConnesKreimer

@[simp]

theorem GrossmanLarson.toConnesKreimer_sub {α : Type u_2} {R : Type u_3} [CommRing R] (x y : GrossmanLarson R α) : (x - y).toConnesKreimer = x.toConnesKreimer - y.toConnesKreimer

@[instance_reducible]

noncomputable instance GrossmanLarson.instAddCommGroup {α : Type u_2} {R : Type u_3} [CommRing R] : AddCommGroup (GrossmanLarson R α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance GrossmanLarson.instRing {α : Type u_2} {R : Type u_3} [CommRing R] : Ring (GrossmanLarson R α)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GrossmanLarson.ιLie {α : Type u_2} {R : Type u_3} [CommRing R] : ChapotonLivernet R α →ₗ⁅R⁆ GrossmanLarson R α

The one-tree forests as a map of Lie algebras: the commutator of two trees in the Grossman–Larson algebra is the commutator of their grafting products.

Equations

• GrossmanLarson.ιLie = { toLinearMap := GrossmanLarson.ι, map_lie' := ⋯ }

@[simp]

theorem GrossmanLarson.ιLie_apply {α : Type u_2} {R : Type u_3} [CommRing R] (x : ChapotonLivernet R α) : ιLie x = ι x