The pruning coproduct Δ^ρ

The admissible-cut, root-component pruning coproduct on unordered rooted trees ([MCB25] Definition 1.2.6 and Lemma 1.2.11 — per their Remark 1.2.9, the Connes-Kreimer Hopf-algebra coproduct of [Foi]), with the Hochschild 1-cocycle property of grafting and the counit laws. Δ^ρ deletes cut subtrees outright, unlike the trace variant Δ^c (Coproduct/Trace.lean), which leaves marker leaves.

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 ([Foi]; [GR20]).
• ConnesKreimer.instBialgebraRho — the Δ^ρ Bialgebra ([MCB25] Lemma 1.2.11), over any CommSemiring.

Implementation notes

B+ only well-defines on unordered children (Multiset (Nonplanar α) → Nonplanar α); on planar trees it would need a canonical ordering — hence the cocycle and everything downstream live at the Nonplanar level. The clean-coassoc route through the cocycle does not generalize to Δ^c (B+ is not a 1-cocycle for the trace variant, which instead uses the direct double-cut bijection).

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.

Status

[UPSTREAM] candidate.

Nonplanar 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} : RoseTree.Nonplanar α → TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))

The nonplanar tree-level Δ^ρ: comulTreeNG at cuts := cutSummandsN.

Equations

• ConnesKreimer.comulTreeN = ConnesKreimer.comulTreeNG ConnesKreimer.cutSummandsN

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

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 : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : comulForestN (F + G) = comulForestN F * comulForestN G

@[simp]

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

Recursive formula: comulForestN (T ::ₘ F) = comulTreeN T * comulForestN F.

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

The Δ^ρ coproduct on ConnesKreimer R (Nonplanar α) as an algebra hom: comulAlgHomNG at cuts := cutSummandsN.

Equations

• ConnesKreimer.comulAlgHomN = ConnesKreimer.comulAlgHomNG ConnesKreimer.cutSummandsN

@[simp]

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

@[simp]

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

Hochschild 1-cocycle for B+_a

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

Δ^ρ ∘ 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 (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)

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

Equations

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

@[simp]

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

@[simp]

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

comulForestN as a sum over forest cuts

Together with cutSummandsN_node (Combinatorics/RootedTree/Cut.lean), the expansion comulForestN_eq_sum drives the cocycle: cuts of a node decompose along the per-tree decisions of cutForestSummandsN, and comulForestN expands as the matching multiset sum.

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

The forest coproduct comulForestN F expands as a multiset sum of of' cf ⊗ of' rem over (cf, rem) ∈ cutForestSummandsN F: the generic comulForestNG_eq_sum at cuts := cutSummandsN, transported along cutForestSummandsN_eq_forestCutsG.

The cocycle theorem (basis-level)

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

The tree-level coproduct on a leaf: comulTreeN (leaf a) = ofTree (leaf a) ⊗ 1 + 1 ⊗ ofTree (leaf a).

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

The Hochschild 1-cocycle property of B+_a, on basis elements: for every forest F, the coproduct of the grafted tree Nonplanar.node a F decomposes as the explicit primitive term plus the right-channel B+ application of comulForestN F. Proven via the substrate cutSummandsN_node (cuts of a node decompose along cutForestSummandsN F) and comulForestN_eq_sum (forest coproduct expands as the matching multiset sum); the LinearMap.lTensor distributes over the sum via map_multiset_sum, and the per-summand check reduces to LinearMap.lTensor_tmul + bPlusLin_of'.

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

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

Counit laws

(ε ⊗ id) ∘ Δ^ρ = lid⁻¹ and (id ⊗ ε) ∘ Δ^ρ = rid⁻¹: reduce to of' F via ConnesKreimer.algHom_ext, then close the tree case by strong induction on depth through the cocycle comulTreeN_node_cocycle.

Coassociativity (comulRhoN_coassoc, Foissy's subalgebra argument) and the Bialgebra instance follow below.

Counit ⊗ id commutation with lTensor (bPlusLin a)

The factor-wise commutation (counit ⊗ id) ∘ (id ⊗ B+_a) = (id ⊗ B+_a) ∘ (counit ⊗ id) (where the right id is on different domains: H on the left, R on the right). Pure TensorProduct.induction_on calculation; both sides reduce to counit x ⊗ B+_a y on simple tensors. Used in the tree-level counit law.

Tree-level counit law (depth induction)

(counit ⊗ id)(Δ T) = 1 ⊗ T for every nonplanar tree T. Strong induction on T.depth: present T as Nonplanar.node a F via a planar rep, then the cocycle comulTreeN_node_cocycle, the commutation counit_rTensor_lTensor_bPlus_apply, and the forest law on the strictly shallower children close the goal.

Counit laws (algebra-hom level)

Reduce to of' F via ConnesKreimer.algHom_ext; the forest laws comulForestN_counit_rTensor and comulForestN_counit_lTensor close from the tree-level laws.

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

theorem ConnesKreimer.counit_lTensor_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (RoseTree.Nonplanar α))) counit).comp comulAlgHomN = ↑(Algebra.TensorProduct.rid R R (ConnesKreimer R (RoseTree.Nonplanar α))).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 depth 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 (RoseTree.Nonplanar α) →ₐ[R] TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α)))

The "compute coassociativity left-hand side" algebra hom: x ↦ assoc((Δ ⊗ id)(Δ x)).

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 (RoseTree.Nonplanar α) →ₐ[R] TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α)))

The "compute coassociativity right-hand side" algebra hom: x ↦ (id ⊗ Δ)(Δ x).

Equations

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

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

The Foissy coassociativity subalgebra: elements where the two sides of coassociativity agree. By Foissy's clean argument (coassocSubalg_eq_top), this 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 (RoseTree.Nonplanar α)) : x ∈ coassocSubalg ↔ coassocLHS x = coassocRHS x

Linear extension of the cocycle

The cocycle comulAlgHomN_bPlusLin_cocycle is stated for of' F. Since both sides are R-linear in x : H, it extends to arbitrary x via ConnesKreimer.lhom_ext (all linear maps out of H = R[Forest] are determined by their action on basis vectors of' F = ConnesKreimer.single F 1).

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

The cocycle, extended to arbitrary x : H via 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.induction_on), 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 (RoseTree.Nonplanar α)) (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 : RoseTree.Nonplanar α) : ofTree T ∈ coassocSubalg

Every Nonplanar tree's ofTree lies in coassocSubalg. By strong induction on tree depth: leaves are B+_a 1 (closed under B+_a from 1); nodes are B+_a (of' F) where of' F is a product of ofTree of smaller-depth trees.

coassocSubalg = ⊤

Since H is generated as an algebra by {ofTree T | T : Nonplanar α} and each generator is in coassocSubalg, the subalgebra is the whole thing.

theorem ConnesKreimer.coassocSubalg_eq_top {R : Type u_1} [CommSemiring R] {α : Type u_2} : coassocSubalg = ⊤

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 (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α)))).comp ((Algebra.TensorProduct.map comulAlgHomN (AlgHom.id R (ConnesKreimer R (RoseTree.Nonplanar α)))).comp comulAlgHomN) = (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (RoseTree.Nonplanar α))) comulAlgHomN).comp comulAlgHomN

theorem ConnesKreimer.comulRhoN_coassoc {R : Type u_1} [CommSemiring R] {α : Type u_2} : ↑(TensorProduct.assoc R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))) ∘ₗ LinearMap.rTensor (ConnesKreimer R (RoseTree.Nonplanar α)) comulAlgHomN.toLinearMap ∘ₗ comulAlgHomN.toLinearMap = LinearMap.lTensor (ConnesKreimer R (RoseTree.Nonplanar α)) 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 (RoseTree.Nonplanar α))

The Δ^ρ Bialgebra on ConnesKreimer R (Nonplanar α) ([MCB25] Lemma 1.2.11), over any CommSemiring.

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 (RoseTree.Nonplanar α)) : 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 (RoseTree.Nonplanar α)) : 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).