The pruning coproduct Δ^ρ

The Connes–Kreimer coproduct on unordered rooted trees, summing over admissible cuts that prune the cut subtrees, with the Hochschild 1-cocycle property of grafting and the counit laws.

Main definitions

• ConnesKreimer.comulTreeN, ConnesKreimer.comulForestN, ConnesKreimer.comulAlgHomN: the Δ^ρ coproduct, as the generic admissible-cut coproduct (Coproduct/WithCuts.lean) at the enumeration cutSummandsN.
• ConnesKreimer.bPlusLin: grafting B+_a as a linear map.

Main results

• ConnesKreimer.comulAlgHomN_bPlusLin_cocycle: the Hochschild 1-cocycle law Δ^ρ ∘ B+_a = B+_a ⊗ 1 + (id ⊗ B+_a) ∘ Δ^ρ.
• ConnesKreimer.counit_rTensor_comulAlgHomN, ConnesKreimer.counit_lTensor_comulAlgHomN: the counit laws.
• ConnesKreimer.comulAlgHomN_coassoc_algHom, comulRhoN_coassoc: coassociativity, by Foissy's subalgebra argument.
• ConnesKreimer.instBialgebraRho: the Δ^ρ Bialgebra, over any CommSemiring.

Implementation notes

B+ only well-defines on unordered children (Multiset (UnorderedTree α) → UnorderedTree α); on planar trees it would need a canonical ordering — hence the cocycle and everything downstream live at the UnorderedTree level.

The GL/CK duality theorem lives downstream in Coproduct/PruningDuality.lean (its proof needs the B⁻ calculus of BMinus.lean, which imports this file); the full HopfAlgebra instance is in HopfAlgebra.lean.

[UPSTREAM] candidate.

References

• [CK98]
• [Foi]
• [GR20]

UnorderedTree tree- and forest-level Δ^ρ

Definitional instantiations of the generic admissible-cut coproduct (Coproduct/WithCuts.lean) at the Δ^ρ enumeration cutSummandsN.

noncomputable def ConnesKreimer.comulTreeN {R : Type u_1} [CommSemiring R] {α : Type u_2} : UnorderedTree α → TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The pruning coproduct Δ^ρ of a tree, which is comulTreeNG at the pruning cuts.

Equations

• ConnesKreimer.comulTreeN = ConnesKreimer.comulTreeNG ConnesKreimer.cutSummandsN

noncomputable def ConnesKreimer.comulForestN {R : Type u_1} [CommSemiring R] {α : Type u_2} : UnorderedTree.Forest (UnorderedTree α) → TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The nonplanar forest-level Δ^ρ (multiplicative extension).

Equations

• ConnesKreimer.comulForestN = ConnesKreimer.comulForestNG ConnesKreimer.cutSummandsN

@[simp]

theorem ConnesKreimer.comulForestN_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : comulForestN 0 = 1

@[simp]

theorem ConnesKreimer.comulForestN_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : UnorderedTree.Forest (UnorderedTree α)) : comulForestN (F + G) = comulForestN F * comulForestN G

@[simp]

theorem ConnesKreimer.comulForestN_cons {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : UnorderedTree α) (F : UnorderedTree.Forest (UnorderedTree α)) : comulForestN (T ::ₘ F) = comulTreeN T * comulForestN F

comulForestN is multiplicative, comulForestN (T ::ₘ F) = comulTreeN T * comulForestN F.

noncomputable def ConnesKreimer.comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (UnorderedTree α) →ₐ[R] TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The pruning coproduct Δ^ρ as an algebra homomorphism, which is comulAlgHomNG at the pruning cuts.

Equations

• ConnesKreimer.comulAlgHomN = ConnesKreimer.comulAlgHomNG ConnesKreimer.cutSummandsN

@[simp]

theorem ConnesKreimer.comulAlgHomN_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : UnorderedTree.Forest (UnorderedTree α)) : comulAlgHomN (of' F) = comulForestN F

@[simp]

theorem ConnesKreimer.comulAlgHomN_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : UnorderedTree α) : comulAlgHomN (ofTree T) = comulTreeN T

Hochschild 1-cocycle for B+_a

B+_a : Forest (UnorderedTree α) → UnorderedTree α is the smart constructor UnorderedTree.node a. Linearly extended to bPlusLin a : H →ₗ[R] H (sending basis element of' F to ofTree (UnorderedTree.node a F)), it satisfies the Hochschild 1-cocycle property:

Δ^ρ ∘ B+_a = (·) ⊗ 1 ∘ B+_a + (id ⊗ B+_a) ∘ Δ^ρ

i.e., for every x : H:

Δ^ρ (B+_a x) = (B+_a x) ⊗ 1 + (id ⊗ B+_a)(Δ^ρ x).

This is the algebraic input to Foissy's clean inductive proof of coassociativity (§A.7-δ): the subalgebra A := {x | (Δ ⊗ id)(Δ x) = (id ⊗ Δ)(Δ x)} is closed under B+_a, contains all leaves (which are B+_a 1), hence equals the whole algebra.

B+_a as a linear map

noncomputable def ConnesKreimer.bPlusLin {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : ConnesKreimer R (UnorderedTree α) →ₗ[R] ConnesKreimer R (UnorderedTree α)

The grafting map B+_a extends the smart constructor UnorderedTree.node a linearly to an R-linear endomorphism of ConnesKreimer R (UnorderedTree α), sending the basis element of' F to ofTree (UnorderedTree.node a F).

Equations

• ConnesKreimer.bPlusLin a = ConnesKreimer.linearLift fun (F : UnorderedTree.Forest (UnorderedTree α)) => ConnesKreimer.ofTree (UnorderedTree.node a F)

@[simp]

theorem ConnesKreimer.bPlusLin_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : UnorderedTree.Forest (UnorderedTree α)) : (bPlusLin a) (of' F) = ofTree (UnorderedTree.node a F)

@[simp]

theorem ConnesKreimer.bPlusLin_one {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : (bPlusLin a) 1 = ofTree (UnorderedTree.leaf a)

comulForestN as a sum over forest cuts

theorem ConnesKreimer.comulForestN_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : UnorderedTree.Forest (UnorderedTree α)) : comulForestN F = (Multiset.map (fun (pf : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => of' pf.1 ⊗ₜ[R] of' pf.2) (forestCutsG cutSummandsN F)).sum

The forest coproduct is the sum of of' cf ⊗ of' rem over the cuts (cf, rem) of the forest.

The cocycle theorem (basis-level)

theorem ConnesKreimer.comulTreeN_leaf {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : comulTreeN (UnorderedTree.leaf a) = ofTree (UnorderedTree.leaf a) ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ofTree (UnorderedTree.leaf a)

A leaf is primitive for the pruning coproduct.

theorem ConnesKreimer.comulTreeN_node_cocycle {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : UnorderedTree.Forest (UnorderedTree α)) : comulTreeN (UnorderedTree.node a F) = ofTree (UnorderedTree.node a F) ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (UnorderedTree α)) (bPlusLin a)) (comulForestN F)

The Hochschild 1-cocycle property of B+_a on basis elements. The coproduct of the grafted tree UnorderedTree.node a F is the primitive term plus B+_a applied on the right channel of comulForestN F.

theorem ConnesKreimer.comulAlgHomN_bPlusLin_cocycle {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : UnorderedTree.Forest (UnorderedTree α)) : comulAlgHomN ((bPlusLin a) (of' F)) = (bPlusLin a) (of' F) ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (UnorderedTree α)) (bPlusLin a)) (comulAlgHomN (of' F))

The cocycle, lifted to the algebra-hom level on tree basis elements.

Counit laws

(ε ⊗ id) ∘ Δ^ρ = lid⁻¹ and (id ⊗ ε) ∘ Δ^ρ = rid⁻¹, checked on trees through the cocycle comulTreeN_node_cocycle. The left law needs induction on the tree.

theorem ConnesKreimer.counit_rTensor_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : (Algebra.TensorProduct.map counit (AlgHom.id R (ConnesKreimer R (UnorderedTree α)))).comp comulAlgHomN = ↑(Algebra.TensorProduct.lid R (ConnesKreimer R (UnorderedTree α))).symm

theorem ConnesKreimer.counit_lTensor_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (UnorderedTree α))) counit).comp comulAlgHomN = ↑(Algebra.TensorProduct.rid R R (ConnesKreimer R (UnorderedTree α))).symm

Coassociativity: Foissy's subalgebra argument

Foissy's clean proof ([Foi]; for the connected-graded-bialgebra framing see [GR20]): the set A := {x | (id ⊗ Δ)(Δ x) = assoc ((Δ ⊗ id)(Δ x))} is a subalgebra, closed under B+_a by the Hochschild cocycle, and contains every ofTree T by height induction — hence A = ⊤. Works over any CommSemiring, with no pairing or nondegeneracy input.

noncomputable def ConnesKreimer.coassocLHS {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (UnorderedTree α) →ₐ[R] TensorProduct R (ConnesKreimer R (UnorderedTree α)) (TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)))

The left-hand side of coassociativity, x ↦ assoc ((Δ ⊗ id) (Δ x)), as an algebra homomorphism.

Equations

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

noncomputable def ConnesKreimer.coassocRHS {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (UnorderedTree α) →ₐ[R] TensorProduct R (ConnesKreimer R (UnorderedTree α)) (TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)))

The right-hand side of coassociativity, x ↦ (id ⊗ Δ) (Δ x), as an algebra homomorphism.

Equations

• ConnesKreimer.coassocRHS = (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (UnorderedTree α))) ConnesKreimer.comulAlgHomN).comp ConnesKreimer.comulAlgHomN

noncomputable def ConnesKreimer.coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} : Subalgebra R (ConnesKreimer R (UnorderedTree α))

The coassociativity subalgebra holds the elements on which the two sides of coassociativity agree. By Foissy's argument it contains every tree (ofTree_mem_coassocSubalg), hence is all of H.

Equations

• ConnesKreimer.coassocSubalg = ConnesKreimer.coassocLHS.equalizer ConnesKreimer.coassocRHS

theorem ConnesKreimer.mem_coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : x ∈ coassocSubalg ↔ coassocLHS x = coassocRHS x

Linear extension of the cocycle

Both sides of comulAlgHomN_bPlusLin_cocycle are linear, so it extends from forests to all of H by ConnesKreimer.lhom_ext'.

theorem ConnesKreimer.comulAlgHomN_bPlusLin_cocycle_general {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (x : ConnesKreimer R (UnorderedTree α)) : comulAlgHomN ((bPlusLin a) x) = (bPlusLin a) x ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (UnorderedTree α)) (bPlusLin a)) (comulAlgHomN x)

The cocycle law holds for arbitrary x : H, by linearity.

Closure of coassocSubalg under B+_a

The substantive Foissy bit. Uses the cocycle (twice) plus tensor-algebra calculations. Sketch (Sweedler-style, with Δ x = Σᵢ aᵢ ⊗ bᵢ):

• Δ(B+_a x) = (B+_a x) ⊗ 1 + Σᵢ aᵢ ⊗ B+_a bᵢ (cocycle).
• (Δ ⊗ id)(Δ(B+_a x)) = Δ(B+_a x) ⊗ 1 + Σᵢ Δ(aᵢ) ⊗ B+_a bᵢ. Re-apply cocycle to Δ(B+_a x) to expand the first summand.
• assoc((Δ ⊗ id)(Δ(B+_a x))) = (B+_a x) ⊗ (1 ⊗ 1) + Σᵢ aᵢ ⊗ (B+_a bᵢ ⊗ 1) + Σᵢ assoc(Δ(aᵢ) ⊗ B+_a bᵢ).
• (id ⊗ Δ)(Δ(B+_a x)) = (B+_a x) ⊗ (1 ⊗ 1) + Σᵢ aᵢ ⊗ (B+_a bᵢ ⊗ 1) + Σᵢ aᵢ ⊗ ((id ⊗ B+_a)(Δ bᵢ)).
• The "shared" first two summands match by inspection. The third summands match via (id ⊗ id ⊗ B+_a) applied to the hypothesis assoc((Δ ⊗ id)(Δ x)) = (id ⊗ Δ)(Δ x).

A clean Lean implementation would extract a LinearMap-level helper assoc_lTensor_bPlus_eq : assoc ∘ (Δ ⊗ id) ∘ (id ⊗ B+_a) = (id ⊗ id ⊗ B+_a) ∘ assoc ∘ (Δ ⊗ id) (provable by TensorProduct.inductionOn), then close by congrArg ((id ⊗ id ⊗ B+_a)) on hx.

Helper commutations for the bPlus closure proof

Three commutation/identity lemmas for the substantive Foissy bit:

• comulAlgHomN_lTensor_bPlus_commute: (Δ ⊗ id) ∘ (id ⊗ B+) = (id ⊗ id ⊗ B+) ∘ (Δ ⊗ id), i.e., the comul on the left factor commutes with B+ on the right factor.
• assoc_lTensor_bPlus_commute: assoc ∘ (id ⊗ id_R ⊗ B+ on (H⊗H)⊗H) = (id ⊗ id ⊗ B+ on H⊗(H⊗H)) ∘ assoc, i.e., the associator commutes with B+ acting on the rightmost factor.
• lTensor_id_Δ_bPlus_eq: (id ⊗ Δ) ∘ (id ⊗ B+) z = assoc((id ⊗ B+)(z) ⊗ 1) + (id ⊗ id ⊗ B+) ∘ (id ⊗ Δ)(z), by cocycle on the right factor of (id ⊗ B+)(z).

theorem ConnesKreimer.bPlus_mem_coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (x : ConnesKreimer R (UnorderedTree α)) (hx : x ∈ coassocSubalg) : (bPlusLin a) x ∈ coassocSubalg

Tree induction: every ofTree T is in coassocSubalg

theorem ConnesKreimer.ofTree_mem_coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : UnorderedTree α) : ofTree T ∈ coassocSubalg

Every tree generator lies in coassocSubalg, by strong induction on height. A leaf is B+_a 1, and a node is B+_a (of' F) with of' F a product of generators of smaller height.

Coassociativity at the algebra-hom level

Direct corollary: coassocLHS = coassocRHS as algebra homs. The Bialgebra.ofAlgHom constructor takes this in its unfolded form (without going through the coassocLHS/coassocRHS named bundles), so we expose both.

theorem ConnesKreimer.coassocLHS_eq_coassocRHS {R : Type u_1} [CommSemiring R] {α : Type u_2} : coassocLHS = coassocRHS

theorem ConnesKreimer.comulAlgHomN_coassoc_algHom {R : Type u_1} [CommSemiring R] {α : Type u_2} : (↑(Algebra.TensorProduct.assoc R R R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)))).comp ((Algebra.TensorProduct.map comulAlgHomN (AlgHom.id R (ConnesKreimer R (UnorderedTree α)))).comp comulAlgHomN) = (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (UnorderedTree α))) comulAlgHomN).comp comulAlgHomN

theorem ConnesKreimer.comulRhoN_coassoc {R : Type u_1} [CommSemiring R] {α : Type u_2} : ↑(TensorProduct.assoc R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))) ∘ₗ LinearMap.rTensor (ConnesKreimer R (UnorderedTree α)) comulAlgHomN.toLinearMap ∘ₗ comulAlgHomN.toLinearMap = LinearMap.lTensor (ConnesKreimer R (UnorderedTree α)) comulAlgHomN.toLinearMap ∘ₗ comulAlgHomN.toLinearMap

Coassociativity of Δ^ρ (LinearMap form).

@[instance_reducible]

noncomputable instance ConnesKreimer.instBialgebraRho {R : Type u_1} [CommSemiring R] {α : Type u_2} : Bialgebra R (ConnesKreimer R (UnorderedTree α))

The pruning coproduct makes ConnesKreimer R (UnorderedTree α) a bialgebra over any commutative semiring.

Equations

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

theorem ConnesKreimer.coalgebra_comul_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : CoalgebraStruct.comul x = comulAlgHomN x

The coproduct of instBialgebraRho is comulAlgHomN.

theorem ConnesKreimer.coalgebra_counit_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : CoalgebraStruct.counit x = counit x

The counit of instBialgebraRho is ConnesKreimer.counit.

GL/CK duality: downstream

The GL/CK duality theorem (pairing_gl_eq_pairing_coproduct_Rho) lives in Coproduct/PruningDuality.lean, downstream of BMinus.lean (whose B⁻ calculus drives its proof).