GL/CK duality for Δ^ρ and coassociativity of the pruning coproduct

[Foi02] [OG08] [MCB25]

The duality theorem pairing_gl_eq_pairing_coproduct_Rho:

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

pairing the Grossman-Larson product against the pruning coproduct through the symmetry-weighted pairing, and its consequence: Δ^ρ coassociativity (comulRhoN_coassoc) and the Bialgebra R (ConnesKreimer R (Nonplanar α)) instance (instBialgebraRho), both transported from GrossmanLarson.mul_assoc.

Orientation

The tensor slots are crossed: linglib's GL product x ⋆ y grafts y's trees into the host x (so x carries the root structure, cf. bMinusLin_gl_mul placing B⁻ on x), while Δ^ρ puts the pruned crown in the first tensor slot and the root trunk in the second (comulTreeN). Hence y pairs against crowns and x against trunks. An earlier sorry-fenced statement of this theorem used the uncrossed orientation pairing₂ (x ⊗ y) (Δ^ρ z), which is false (e.g. x = {•_p}, y = {•_q}, z the 2-chain p–q: LHS 1, RHS 0). Both orientations were checked against the exhaustive planar simulation battery in scratch/validate_duality.lean (V1): the crossed form holds on all weight-matched triples of forests of weight ≤ 3 and on targeted weight-4 duplicate-tree traps; the uncrossed form fails on 72 of them.

This file lives downstream of BMinus.lean (whose B⁻ calculus drives the single-tree induction step), so the duality theorem and its consumers were moved here from Coproduct/PruningNonplanar.lean.

Proof architecture (weight induction on z)

Reduce to basis forests z = of' C by linearity; strong induction on total weight of C:

• C = 0: both sides are counits — counit_gl_mul.
• C = {T}, T = B⁺_a W: ⟨x ⋆ y, B⁺_a W⟩ unfolds via pairing_apply_bPlus_gl_mul (B⁺/B⁻ adjoint + the OG cocycle bMinusLin_gl_mul); pairing₂ (y ⊗ x) (Δ^ρ B⁺_a W) unfolds via the Hochschild cocycle comulTreeN_node_cocycle + the adjoint moved through the second tensor slot. The two recurrences match summand-wise; the T ⊗ 1 term is the adjoint identity itself.
• C = T ::ₘ C' (C' ≠ 0): split of' C = ofTree T * of' C'; apply pairing_product_of'_mul_of' (LHS) and the tensor-square of pairing_of'_mul (RHS, via Δ^ρ multiplicativity); the two antidiagonal-indexed sums match termwise under the induction hypothesis at ofTree T and of' C'.

Adjoint through the second tensor slot

Pairing against the unit

Tensor-square of the pairing product rule

CK-typed linearity of the GL product in its first slot

GrossmanLarson.product is a LinearMap at the GrossmanLarson carrier; these restate first-slot linearity with all terms ascribed at ConnesKreimer (definitionally equal carriers, syntactically different instances), so they can be used as rewrite rules in CK-typed goals.

The duality theorem

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

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).

Coassoc LinearMaps + chain lemmas via the duality

theorem RootedTree.ConnesKreimer.pairing₃_coassocLHSLinRho {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y z' z : ConnesKreimer R (Nonplanar α)) : (pairing₃ (x ⊗ₜ[R] (y ⊗ₜ[R] z'))) (RootedTree.ConnesKreimer.coassocLHSLinRho✝ z) = (GrossmanLarson.pairing ((GrossmanLarson.product z') ((GrossmanLarson.product y) x))) z

LHS chain via the duality (twice): pairing the LHS coassoc expression against a pure triple tensor reduces to pairing the GL product z' ⋆ (y ⋆ x) against z.

theorem RootedTree.ConnesKreimer.pairing₃_coassocRHSLinRho {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y z' z : ConnesKreimer R (Nonplanar α)) : (pairing₃ (x ⊗ₜ[R] (y ⊗ₜ[R] z'))) (RootedTree.ConnesKreimer.coassocRHSLinRho✝ z) = (GrossmanLarson.pairing ((GrossmanLarson.product ((GrossmanLarson.product z') y)) x)) z

RHS chain via the duality (twice): pairing the RHS coassoc expression against a pure triple tensor reduces to pairing the GL product (z' ⋆ y) ⋆ x against z.

Coassociativity of Δ^ρ via GL/CK duality (LinearMap form)

Specialized to [CommRing R] (rather than [CommSemiring R]) since the proof uses subtraction (via sub_eq_zero in pairing₃_unique), which requires R to be a Ring (so CK R T has AddCommGroup).

theorem RootedTree.ConnesKreimer.comulRhoN_coassoc {R' : Type u_3} [CommRing R'] {α' : Type u_4} [CharZero R'] [NoZeroDivisors R'] : ↑(TensorProduct.assoc R' (ConnesKreimer R' (Nonplanar α')) (ConnesKreimer R' (Nonplanar α')) (ConnesKreimer R' (Nonplanar α'))) ∘ₗ LinearMap.rTensor (ConnesKreimer R' (Nonplanar α')) comulAlgHomN.toLinearMap ∘ₗ comulAlgHomN.toLinearMap = LinearMap.lTensor (ConnesKreimer R' (Nonplanar α')) comulAlgHomN.toLinearMap ∘ₗ comulAlgHomN.toLinearMap

Coassociativity of comulAlgHomN (LinearMap form), via GL/CK duality. Parallel to TraceNonplanar.comulCN_coassoc for Δ^c.

Derived via the chain:

1. ext z: reduce to pointwise LHS z = RHS z.
2. pairing₃_unique: reduce to ∀ t, pairing₃ t (LHS z) = pairing₃ t (RHS z).
3. TensorProduct.induction_on thrice: reduce t to pure triple tensors x ⊗ (y ⊗ z').
4. pairing₃_coassocLHSLinRho / pairing₃_coassocRHSLinRho: reduce both sides to GL products against z (two duality applications each).
5. GrossmanLarson.mul_assoc z' y x closes.

theorem RootedTree.ConnesKreimer.comulAlgHomN_coassoc_algHom {R' : Type u_3} [CommRing R'] {α' : Type u_4} [CharZero R'] [NoZeroDivisors R'] : (↑(Algebra.TensorProduct.assoc R' R' R' (ConnesKreimer R' (Nonplanar α')) (ConnesKreimer R' (Nonplanar α')) (ConnesKreimer R' (Nonplanar α')))).comp ((Algebra.TensorProduct.map comulAlgHomN (AlgHom.id R' (ConnesKreimer R' (Nonplanar α')))).comp comulAlgHomN) = (Algebra.TensorProduct.map (AlgHom.id R' (ConnesKreimer R' (Nonplanar α'))) comulAlgHomN).comp comulAlgHomN

AlgHom-form coassociativity of comulAlgHomN. Follows from comulRhoN_coassoc (LinearMap form) by AlgHom extensionality, the same one-liner pattern as TraceNonplanar.comulCAlgHomN_coassoc_algHom.

Bialgebra instance

Built via Bialgebra.ofAlgHom from comulAlgHomN_coassoc_algHom (GL/CK duality) and the two counit AlgHom laws. The duality-based coassoc proof forces [CommRing R] [CharZero R] [NoZeroDivisors R]; the counit laws hold over [CommSemiring R] and are automatically satisfied.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instBialgebraRho {R' : Type u_3} [CommRing R'] [CharZero R'] [NoZeroDivisors R'] {α' : Type u_4} : Bialgebra R' (ConnesKreimer R' (Nonplanar α'))

Equations

• RootedTree.ConnesKreimer.instBialgebraRho = Bialgebra.ofAlgHom RootedTree.ConnesKreimer.comulAlgHomN RootedTree.ConnesKreimer.counit ⋯ ⋯ ⋯