Dual-primitive functionals on the Connes–Kreimer bialgebra

A linear functional on the Connes–Kreimer bialgebra is a dual primitive exactly when it vanishes on every forest that is not a single tree. The delta functionals δ_T = lcoeff R {T} of the trees are dual primitives, and the commutator of two of them counts single cuts. The symmetry-weighted pairing sends the primitive elements of the Grossman–Larson bialgebra to dual primitives, and it maps the pre-Lie algebra of rooted trees to the Lie algebra of dual primitives. Chapoton and Livernet observe this identification with the Lie algebra that Connes and Kreimer find dual to their Hopf algebra.

Main definitions

• GrossmanLarson.pairingLie: the pairing as a map of Lie algebras from the pre-Lie algebra of rooted trees to Bialgebra.dualPrimitives.

Main results

• ConnesKreimer.isDualPrimitive_iff: the dual primitives are the functionals supported on single trees.
• ConnesKreimer.lie_lcoeff_singleton_apply_ofTree, ConnesKreimer.lie_lcoeff_singleton_apply_of': the commutator ⁅δ_{T₁}, δ_{T₂}⁆ takes a tree T to the number of single cuts of T with crown T₁ and trunk T₂ minus the number with crown T₂ and trunk T₁, and vanishes on every other forest.
• ConnesKreimer.autCard_mul_autCard_mul_countSingleCutsRho: Hoffman's relation between the single cuts of T with crown T₁ and trunk T₂ and the graftings of T₁ onto T₂ that give T, each weighted by numbers of symmetries.
• GrossmanLarson.isDualPrimitive_pairing, GrossmanLarson.pairingLie_injective: pairing with a primitive element is a dual primitive, and in characteristic zero the pre-Lie algebra of trees embeds in the dual primitives.

Implementation notes

The product δ_{T₁} ⋆ δ_{T₂} is not a combination of the δ_T: on the forest {T₁, T₂} it takes the value 1, or 2 when the trees are equal (ConnesKreimer.convMul_lcoeff_singleton_apply_mul). Only the commutator is a dual primitive.

The grafting product puts the host first and the pruning coproduct puts the crown first, so the pairing reverses products. GrossmanLarson.pairingLie is therefore defined on the opposite pre-Lie algebra (ChapotonLivernet R α)ᵐᵒᵖ, whose product grafts the first factor onto the second, as Connes and Kreimer's does.

References

• [CK98]
• [CL01]
• [Hof03]

theorem ConnesKreimer.isDualPrimitive_iff {R : Type u_1} {α : Type u_2} [CommSemiring R] {f : ConnesKreimer R (UnorderedTree α) →ₗ[R] R} : Bialgebra.IsDualPrimitive R f ↔ ∀ (F : UnorderedTree.Forest (UnorderedTree α)), Multiset.card F ≠ 1 → f (of' F) = 0

A linear functional on the Connes–Kreimer bialgebra is a dual primitive exactly when it vanishes on every forest that is not a single tree.

theorem ConnesKreimer.isDualPrimitive_lcoeff_singleton {R : Type u_1} {α : Type u_2} [CommSemiring R] (T : UnorderedTree α) : Bialgebra.IsDualPrimitive R (lcoeff R {T})

The delta functional of a single tree is a dual primitive.

theorem ConnesKreimer.isDualPrimitive_lcoeff_iff {R : Type u_1} {α : Type u_2} [CommSemiring R] {F : UnorderedTree.Forest (UnorderedTree α)} [Nontrivial R] : Bialgebra.IsDualPrimitive R (lcoeff R F) ↔ Multiset.card F = 1

Among the delta functionals of forests, the dual primitives are those of the single trees.

theorem ConnesKreimer.convMul_lcoeff_singleton_apply_ofTree {R : Type u_1} {α : Type u_2} [CommSemiring R] [DecidableEq α] (T T₁ T₂ : UnorderedTree α) : (WithConv.toConv (lcoeff R {T₁}) * WithConv.toConv (lcoeff R {T₂})).ofConv (ofTree T) = ↑(countSingleCutsRho T T₁ T₂)

The convolution product of two single-tree deltas takes a tree T to the number of single cuts of T with crown T₁ and trunk T₂.

theorem ConnesKreimer.convMul_lcoeff_singleton_apply_mul {R : Type u_1} {α : Type u_2} [CommSemiring R] [DecidableEq α] (T₁ T₂ : UnorderedTree α) : (WithConv.toConv (lcoeff R {T₁}) * WithConv.toConv (lcoeff R {T₂})).ofConv (ofTree T₁ * ofTree T₂) = if T₁ = T₂ then 2 else 1

The convolution product of two single-tree deltas takes the forest of the two trees to 1, or to 2 when the trees are equal, so the product of two dual primitives need not be one.

theorem ConnesKreimer.lie_lcoeff_singleton_apply_of' {R : Type u_1} {α : Type u_2} [CommRing R] (T₁ T₂ : UnorderedTree α) {F : UnorderedTree.Forest (UnorderedTree α)} (hF : Multiset.card F ≠ 1) : ⁅WithConv.toConv (lcoeff R {T₁}), WithConv.toConv (lcoeff R {T₂})⁆.ofConv (of' F) = 0

The commutator of two single-tree deltas vanishes on every forest that is not a single tree.

theorem ConnesKreimer.lie_lcoeff_singleton_apply_ofTree {R : Type u_1} {α : Type u_2} [CommRing R] (T T₁ T₂ : UnorderedTree α) [DecidableEq α] : ⁅WithConv.toConv (lcoeff R {T₁}), WithConv.toConv (lcoeff R {T₂})⁆.ofConv (ofTree T) = ↑(countSingleCutsRho T T₁ T₂) - ↑(countSingleCutsRho T T₂ T₁)

The commutator of two single-tree deltas takes a tree T to the number of single cuts of T with crown T₁ and trunk T₂ minus the number with crown T₂ and trunk T₁.

The pairing with the pre-Lie algebra of trees

theorem GrossmanLarson.isDualPrimitive_pairing {R : Type u_1} {α : Type u_2} [DecidableEq α] [CommSemiring R] {x : GrossmanLarson R α} (hx : Bialgebra.IsPrimitiveElem R x) : Bialgebra.IsDualPrimitive R (pairing x.toConnesKreimer)

Pairing with a primitive element of the Grossman–Larson bialgebra is a dual primitive of the Connes–Kreimer bialgebra.

theorem GrossmanLarson.isPrimitiveElem_of_iff {R : Type u_1} {α : Type u_2} [DecidableEq α] [CommSemiring R] [CharZero R] {F : UnorderedTree.Forest (UnorderedTree α)} : Bialgebra.IsPrimitiveElem R (of F) ↔ Multiset.card F = 1

Among the basis forests of the Grossman–Larson bialgebra, the primitive ones are the single trees.

theorem ConnesKreimer.autCard_mul_autCard_mul_countSingleCutsRho {α : Type u_2} [DecidableEq α] (T T₁ T₂ : UnorderedTree α) : T₁.autCard * T₂.autCard * countSingleCutsRho T T₁ T₂ = Multiset.count T (T₂.insertSum T₁) * T.autCard

Hoffman's relation. The single cuts of T with crown T₁ and trunk T₂, counted with the symmetries of T₁ and T₂, are as many as the vertices of T₂ at which grafting T₁ gives T, counted with the symmetries of T.

noncomputable def GrossmanLarson.pairingLie {R : Type u_1} {α : Type u_2} [DecidableEq α] [CommRing R] : (ChapotonLivernet R α)ᵐᵒᵖ →ₗ⁅R⁆ ↥(Bialgebra.dualPrimitives R (ConnesKreimer R (UnorderedTree α)))

The pairing as a map of Lie algebras from the left pre-Lie algebra of rooted trees, in which the first factor is grafted onto the second, to the dual primitives of the Connes–Kreimer bialgebra. It sends a tree T to |Aut T| • δ_T.

Equations

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

@[simp]

theorem GrossmanLarson.coe_pairingLie {R : Type u_1} {α : Type u_2} [DecidableEq α] [CommRing R] (x : (ChapotonLivernet R α)ᵐᵒᵖ) : ↑(pairingLie x) = WithConv.toConv (pairing (ι (MulOpposite.unop x)).toConnesKreimer)

theorem GrossmanLarson.coe_pairingLie_op_of {R : Type u_1} {α : Type u_2} [DecidableEq α] [CommRing R] (T : UnorderedTree α) : ↑(pairingLie (MulOpposite.op (ChapotonLivernet.of T))) = ↑T.autCard • WithConv.toConv (ConnesKreimer.lcoeff R {T})

theorem GrossmanLarson.pairingLie_injective {R : Type u_1} {α : Type u_2} [DecidableEq α] [CommRing R] [CharZero R] [NoZeroDivisors R] : Function.Injective ⇑pairingLie

Over a ring of characteristic zero without zero divisors, the pre-Lie algebra of rooted trees embeds in the dual primitives.