Duality of the Grossman–Larson product and the pruning coproduct

Under the symmetry-weighted pairing, the Grossman–Larson product is the transpose of the pruning coproduct Δ^ρ: ⟨x ⋆ y, z⟩ = ⟨y ⊗ x, Δ^ρ z⟩. So the pairing turns the Grossman–Larson product into the convolution product of linear functionals on the Connes–Kreimer bialgebra, in the opposite order. Hoffman states the duality in this form, as a map of the Grossman–Larson algebra to the graded dual.

Main results

• ConnesKreimer.pairing_gl_eq_pairing_coproduct_Rho: the duality ⟨x ⋆ y, z⟩ = pairing₂ (y ⊗ x) (Δ^ρ z).
• ConnesKreimer.toConv_pairing_product: ⟨x ⋆ y, ·⟩ = ⟨y, ·⟩ * ⟨x, ·⟩ in the convolution algebra of linear functionals.
• ConnesKreimer.pairing_product_assoc: the two triple products pair equally against everything, since the convolution product is associative.

Implementation notes

The tensor slots of the duality are crossed. The product x ⋆ y grafts the trees of y onto the host x, while Δ^ρ puts the pruned crown in the first tensor slot and the trunk in the second, so y pairs against crowns and x against trunks. The uncrossed statement is false: for the one-vertex trees x = •_p and y = •_q and the chain z with root p and leaf q, the left side is 1 and pairing₂ (x ⊗ y) (Δ^ρ z) is 0.

The duality is proved by strong induction on the total weight of a basis forest z = of' C. The one-tree step uses the adjunction of B⁺ and B⁻ (BMinus.lean) and the Hochschild cocycle property; the step for several trees uses the product rule of the pairing.

References

• [Foi02]
• [OG08]
• [Hof03]

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 (UnorderedTree α)) : (GrossmanLarson.pairing ((GrossmanLarson.product x) y)) z = (GrossmanLarson.pairing₂ (y ⊗ₜ[R] x)) (comulAlgHomN z)

The Grossman–Larson product is the transpose of the pruning coproduct under the symmetry-weighted pairing, ⟨x ⋆ y, z⟩ = pairing₂ (y ⊗ x) (Δ^ρ z). The tensor slots are crossed: the grafted factor y pairs against the pruned crowns and the host x against the trunks.

The pairing as a map to the convolution algebra

theorem ConnesKreimer.toConv_pairing_product {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (x y : ConnesKreimer R (UnorderedTree α)) : WithConv.toConv (GrossmanLarson.pairing ((GrossmanLarson.product x) y)) = WithConv.toConv (GrossmanLarson.pairing y) * WithConv.toConv (GrossmanLarson.pairing x)

The pairing turns the Grossman–Larson product into the convolution product of linear functionals, in the opposite order.

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

The two triple Grossman–Larson products pair equally against everything, since the convolution product is associative.

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

Δ^ρ is the generic admissible-cut coproduct at the pruning cuts.

instance ConnesKreimer.instIsAdmissibleCutsCutSummandsN {α : Type u_3} : IsAdmissibleCuts cutSummandsN

The pruning cuts are admissible, by the coassociativity and counit laws of Δ^ρ.