Dual-primitive functionals on the Connes-Kreimer bialgebra

[MCB25]

Substrate for [MCB25]'s Lemma 1.7.3 (book pp. 78-79): the insertion Lie algebra is the Lie algebra of primitive elements in the dual Hopf algebra of the Hopf algebra of workspaces. This file proves the dual-primitives side on the Connes-Kreimer bialgebra with the Δ^ρ (deletion-remainder) coproduct, specializing the general Bialgebra.dualPrimitives theory of Core/RingTheory/Bialgebra/Primitive.

The paper's dual-basis functional δ_T is lcoeff R {T}; the cut count countSingleCutsRho lives with cutSummandsN in Coproduct/Pruning.

Main results

• ConnesKreimer.lcoeff_singleton_isDualPrimitive: each single-tree delta δ_T is a dual primitive.
• ConnesKreimer.lie_lcoeff_singleton_apply_ofTree: the explicit count form ⁅δ_{T₁}, δ_{T₂}⁆ (ofTree T) = countSingleCutsRho T T₁ T₂ − countSingleCutsRho T T₂ T₁, the Δ^ρ analog of the book's c^T_{T₁,T₂} − c^T_{T₂,T₁}. The Δ^c (trace-leaf) version follows via the strip machinery in Coproduct/Deletion.lean.

Not yet stated: the Lie algebra isomorphism with the insertion Lie algebra on trees; this file proves the dual-primitives side only.

Single-tree deltas are dual primitives

theorem ConnesKreimer.lcoeff_singleton_isDualPrimitive {R : Type u_1} [CommRing R] {α : Type u_2} (T : RoseTree.Nonplanar α) [DecidableEq α] [CharZero R] [NoZeroDivisors R] : Bialgebra.IsDualPrimitive R (lcoeff R {T})

The single-tree delta δ_T = lcoeff R {T} is a dual primitive: the bialgebraic content of [MCB25]'s observation (book p. 79) that primitives in the dual are exactly the single-tree deltas.

theorem ConnesKreimer.toConv_lcoeff_singleton_mem_dualPrimitives {R : Type u_1} [CommRing R] {α : Type u_2} (T : RoseTree.Nonplanar α) [DecidableEq α] [CharZero R] [NoZeroDivisors R] : WithConv.toConv (lcoeff R {T}) ∈ Bialgebra.dualPrimitives R (ConnesKreimer R (RoseTree.Nonplanar α))

[MCB25] Lemma 1.7.3, membership form: single-tree deltas lie in the Lie subalgebra of dual primitives (so their brackets do too, by LieSubalgebra.lie_mem).

The explicit count formula

theorem ConnesKreimer.convMul_lcoeff_singleton_apply_ofTree {R : Type u_1} [CommRing R] {α : Type u_2} (T T₁ T₂ : RoseTree.Nonplanar α) [DecidableEq α] [CharZero R] [NoZeroDivisors R] : (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 evaluated on a single-tree basis vector counts the Δ^ρ cut summands of T extracting {T₁} and leaving T₂.

theorem ConnesKreimer.lie_lcoeff_singleton_apply_ofTree {R : Type u_1} [CommRing R] {α : Type u_2} (T T₁ T₂ : RoseTree.Nonplanar α) [DecidableEq α] [CharZero R] [NoZeroDivisors R] : ⁅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 delta functionals, evaluated at a tree T, is the antisymmetrized count of single Δ^ρ cuts of T with cut forest {T₁} and remainder T₂. This is Lemma 1.7.3 of [MCB25] in Δ^ρ form; the book's c^T_{T₁,T₂} − c^T_{T₂,T₁} is stated for the trace-leaf coproduct Δ^c, which agrees under the trace-erasure projection (eraseTracesAlgHom).