The Grossman–Larson bialgebra

The Grossman–Larson algebra is a cocommutative bialgebra. Its comultiplication splits a forest into two subforests in all ways, as in the symmetric algebra on the trees, and its counit takes the coefficient of the empty forest. The one-tree forests are primitive, and the symmetry-weighted pairing transposes the product of the Connes–Kreimer algebra to this comultiplication.

Main definitions

• GrossmanLarson.instBialgebra: the bialgebra structure.

Main results

• GrossmanLarson.comul_of: Δ(F) = ∑_{A + B = F} A ⊗ B.
• GrossmanLarson.isPrimitiveElem_ι: the pre-Lie algebra of trees lies in the primitive elements.
• GrossmanLarson.toConv_pairing_mul: ⟨z w, ·⟩ = ⟨z, ·⟩ * ⟨w, ·⟩ in the convolution algebra of linear functionals on the Grossman–Larson bialgebra.

Implementation notes

The coalgebra is the primitive coproduct of Coproduct/Primitive.lean, moved along the linear identification with the Connes–Kreimer module. Its compatibility with the product is Oudom and Guin's Lemma 3.11, here read off UnorderedTree.productMultiset_bind_antidiagonal.

TODO

The Grossman–Larson bialgebra is graded and connected, so it has an antipode.

References

• [GL89]
• [OG08]
• [Hof03]

The coalgebra

@[instance_reducible]

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

Equations

• GrossmanLarson.instCoalgebra = LinearEquiv.coalgebra R GrossmanLarson.linearEquiv

theorem GrossmanLarson.comul_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : GrossmanLarson R α) : CoalgebraStruct.comul x = (TensorProduct.map ↑linearEquiv.symm ↑linearEquiv.symm) (ConnesKreimer.comulPrim x.toConnesKreimer)

@[simp]

theorem GrossmanLarson.counit_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : GrossmanLarson R α) : CoalgebraStruct.counit x = ConnesKreimer.counit x.toConnesKreimer

theorem GrossmanLarson.comul_of {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : UnorderedTree.Forest (UnorderedTree α)) : CoalgebraStruct.comul (of F) = (Multiset.map (fun (p : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => of p.1 ⊗ₜ[R] of p.2) (Multiset.antidiagonal F)).sum

The comultiplication sums A ⊗ B over the splittings F = A + B, counted with multiplicity.

instance GrossmanLarson.instIsCocomm {R : Type u_1} [CommSemiring R] {α : Type u_2} : Coalgebra.IsCocomm R (GrossmanLarson R α)

The bialgebra

theorem GrossmanLarson.comul_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : GrossmanLarson R α) : CoalgebraStruct.comul (x * y) = CoalgebraStruct.comul x * CoalgebraStruct.comul y

@[instance_reducible]

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

Equations

• GrossmanLarson.instBialgebra = Bialgebra.mk' R (GrossmanLarson R α) ⋯ ⋯ ⋯ ⋯

Primitive elements

theorem GrossmanLarson.isPrimitiveElem_of_singleton {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : UnorderedTree α) : Bialgebra.IsPrimitiveElem R (of {T})

A one-tree forest is primitive.

theorem GrossmanLarson.isPrimitiveElem_ι {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ChapotonLivernet R α) : Bialgebra.IsPrimitiveElem R (ι x)

The pre-Lie algebra of trees lies in the primitive elements.

The pairing

theorem GrossmanLarson.toConv_pairing_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (z w : ConnesKreimer R (UnorderedTree α)) : WithConv.toConv (pairing (z * w) ∘ₗ ↑linearEquiv) = WithConv.toConv (pairing z ∘ₗ ↑linearEquiv) * WithConv.toConv (pairing w ∘ₗ ↑linearEquiv)

The pairing transposes the product of the Connes–Kreimer algebra to the comultiplication of the Grossman–Larson bialgebra: pairing with z * w is the convolution product of pairing with z and pairing with w.