GL/CK duality for the pruning coproduct

The Grossman-Larson product and the pruning coproduct Δ^ρ are adjoint under the symmetry-weighted pairing ([Foi02]; the grafting calculus of [OG08]).

Main results

• ConnesKreimer.pairing_gl_eq_pairing_coproduct_Rho — the duality ⟨x ⋆ y, z⟩ = pairing₂ (y ⊗ x) (Δ^ρ z).
• ConnesKreimer.pairing_product_assoc — Foissy coassociativity of Δ^ρ pushed back through the duality: the two GL triple products pair equally against everything (associativity up to separation, closed in GrossmanLarson/Monoid.lean).
• The IsAdmissibleCuts cutSummandsN model instance for the WithCuts carrier (coassociativity and counit laws from Coproduct/Pruning.lean).

Implementation notes

The tensor slots of the duality are crossed: the GL product x ⋆ y grafts y's trees into the host x (so x carries the root structure), while Δ^ρ puts the pruned crown in the first tensor slot and the root trunk in the second. Hence y pairs against crowns and x against trunks. The uncrossed orientation pairing₂ (x ⊗ y) (Δ^ρ z) is false (e.g. x = {•_p}, y = {•_q}, z the 2-chain p–q: LHS 1, RHS 0).

The duality is proved by strong induction on the total weight of a basis forest z = of' C, with the single-tree step driven by the B⁺/B⁻ adjoint of BMinus.lean and the Hochschild cocycle, and the multi-tree step by the pairing product rule over antidiagonal-indexed splits.

Adjoint through the second tensor slot

Tensor-square of the pairing product rule

The duality theorem

theorem ConnesKreimer.pairing_gl_eq_pairing_coproduct_Rho {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (x y z : ConnesKreimer R (RoseTree.Nonplanar α)) : (GrossmanLarson.pairing ((GrossmanLarson.product x) y)) z = (GrossmanLarson.pairing₂ (y ⊗ₜ[R] x)) (comulAlgHomN z)

The GL/CK duality for Δ^ρ ([Foi02]): the GL ⋆ product and the pruning coproduct Δ^ρ are adjoint under the symmetry-weighted pairing, with crossed tensor slots (see module docstring):

⟨x ⋆ y, z⟩ = pairing₂ (y ⊗ x) (Δ^ρ z)

(y against pruned crowns, x against root trunks).

Associativity of the GL product, pairing form

Foissy coassociativity of Δ^ρ (Coproduct/Pruning.lean) transports back through the duality: pairing the two GL triple products against an arbitrary element yields the two sides of coassociativity. Separation over a characteristic-zero domain and the descent to any CommSemiring live in GrossmanLarson/Monoid.lean.

theorem ConnesKreimer.pairing_product_assoc {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (x y z w : ConnesKreimer R (RoseTree.Nonplanar α)) : (GrossmanLarson.pairing ((GrossmanLarson.product x) ((GrossmanLarson.product y) z))) w = (GrossmanLarson.pairing ((GrossmanLarson.product ((GrossmanLarson.product x) y)) z)) w

Associativity of the GL product, pairing form: the two triple products pair equally against everything — Δ^ρ coassociativity (comulRhoN_coassoc) pushed through the duality twice on each side.

theorem ConnesKreimer.comulAlgHomN_eq_G {R : Type u_3} [CommSemiring R] {α : Type u_4} : comulAlgHomN = comulAlgHomNG cutSummandsN

Δ^ρ is the generic coproduct at cuts := cutSummandsN — definitional.

instance ConnesKreimer.instIsAdmissibleCutsCutSummandsNOfDecidableEq {α : Type u_3} [DecidableEq α] : IsAdmissibleCuts cutSummandsN

Δ^ρ is admissible: Foissy coassociativity and the counit laws (Coproduct/Pruning.lean), transported through the rfl bridge comulAlgHomN_eq_G.