Δ^ρ (admissible-cut, root-component pruning) coproduct on RoseTree α

[MCB25] [foissy-introduction-hopf-algebras-trees]

The admissible-cut, root-component pruning variant of the Connes-Kreimer coproduct on ordered (planar) n-ary rooted trees RoseTree α. For a tree T:

Δ^ρ(T) = T ⊗ 1 + Σ_{c : Cut T} of'(cutForest c) ⊗ ofTree(remainderDeletion c)

where the empty cut contributes 1 ⊗ T (since cutForest empty = ∅).

Naming. Linglib's "Δ^ρ" corresponds to MCB Definition 1.2.6's Δ^ρ (book p. 31) — the admissible-cut coproduct whose right channel is the root component ρ_C(T) after pruning the cut subtrees from the parent's children list. The result lives in at-most-n-ary trees (Lemma 1.2.11, book p. 38). Per MCB Remark 1.2.9 (book p. 34), this Δ^ρ coproduct corresponds to the Foissy Connes-Kreimer Hopf algebra of (not-necessarily-binary) rooted trees, where the right channel can contain rooted trees that are not binary.

NOT MCB's Δ^d (Definition 1.2.5, p. 31), which is "deletion + rebinarization" — Δ^d additionally contracts edges to recover binarity. Δ^d is the closest to PF Externalization and would be derived from this Δ^ρ (or built independently) when a consumer needs it. See sibling Coproduct/Deletion.lean (FUTURE) for that.

For the trace variant Δ^c (T/^c F_v, parent arity preserved via trace leaves; MCB Definition 1.2.4, book p. 30), see sibling Coproduct/Trace.lean. MCB Δ^c on binary nonplanar = restriction of the Connes-Kreimer Hopf algebra of Feynman graphs (a different, related Hopf algebra; Remark 1.2.9, p. 34). Used at the C-I (semantic) interface for FormCopy.

Relation to the generic cut enumeration

The bespoke cutSummandsP/cutListSummandsP/augActionP block below is the deletion (Δ^ρ) sibling of the extraction-policy-parameterized cutSummandsG in Coproduct/Defs.lean. It is NOT re-expressed as cutSummandsG (fun _ => some []) because the downstream coassoc proof (Coproduct/PruningNonplanar.lean) is written against the Option remainder encoding used here — deletion is Option.none, a surviving child is Option.some r — whereas cutSummandsG carries List remainders (deletion [], survival [r]). Folding onto cutSummandsG would change the public return type of augActionP (Option → List) and the shapes of augActionP_eq/cutListSummandsP_cons, all of which PruningNonplanar.lean consumes; so the two enumerations coexist. (Δ^c in Trace.lean does derive from cutSummandsG, since it was written against the List encoding.)

Foissy clean coassoc

Δ^ρ satisfies the Hochschild 1-cocycle condition with B+ (graft as new root):

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

The B+ operator only well-defines on Multiset (Nonplanar α) → Nonplanar α (unordered children of a new root). On RoseTree α with Multiset forests, B+ would need a canonical ordering. Hence the sorry-free coassoc proof for Δ^ρ lives in Coproduct/PruningNonplanar.lean on RootedTree.Nonplanar α. (Note: this Foissy clean coassoc strategy does NOT generalize to Δ^c — B+ is not a Hochschild 1-cocycle for the trace variant. Δ^c coassoc uses Grossman-Larson duality instead; see the GL substrate when it lands.)

Status

[UPSTREAM] candidate. cutSummands recursive definition; full Bialgebra structure (descent + coassoc + counit + Hopf antipode) lives in Coproduct/PruningNonplanar.lean and HopfAlgebraNonplanar.lean.

cutSummandsP — multiset of (cut forest, deletion remainder) pairs

Recursive enumeration of cut summands. For a leaf, the only cut is the empty cut. For a node, sum over all per-child decisions: each child can either be extracted whole (contributes to cut forest, drops from remainder) OR recurse with a smaller cut (contributes whatever its cut extracts, leaves its deletion-remainder in the remainder list).

@[irreducible]

def RootedTree.ConnesKreimer.cutSummandsP {α : Type u_2} : RoseTree α → Multiset (Forest (RoseTree α) × RoseTree α)

Multiset of (cut forest, deletion remainder) pairs for a tree. Each summand corresponds to one admissible cut on T under the deletion semantics.

Equations

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

@[irreducible]

def RootedTree.ConnesKreimer.cutListSummandsP {α : Type u_2} : List (RoseTree α) → Multiset (Forest (RoseTree α) × List (RoseTree α))

Auxiliary: cut summands for a list of children. The remainder is a list (children of the parent that survived the cut).

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.ConnesKreimer.cutListSummandsP [] = {(0, [])}

@[irreducible]

def RootedTree.ConnesKreimer.augActionP {α : Type u_2} : RoseTree α → Multiset (Forest (RoseTree α) × Option (RoseTree α))

Auxiliary: per-child action — either extract whole (none remainder) or recurse with a cut (some remainder).

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.cutSummandsP_node {α : Type u_2} (a : α) (cs : List (RoseTree α)) : cutSummandsP (RoseTree.node a cs) = Multiset.map (fun (p : Forest (RoseTree α) × List (RoseTree α)) => (p.1, RoseTree.node a p.2)) (cutListSummandsP cs)

Recursive formula on a node: cutSummandsP unfolds via cutListSummandsP.

@[simp]

theorem RootedTree.ConnesKreimer.cutListSummandsP_nil {α : Type u_2} : cutListSummandsP [] = {(0, [])}

Recursive formula for cutListSummandsP on empty list.

@[simp]

theorem RootedTree.ConnesKreimer.cutListSummandsP_cons {α : Type u_2} (t : RoseTree α) (ts : List (RoseTree α)) : cutListSummandsP (t :: ts) = Multiset.map (fun (p : (Forest (RoseTree α) × Option (RoseTree α)) × Forest (RoseTree α) × List (RoseTree α)) => match p.1.2 with | none => (p.1.1 + p.2.1, p.2.2) | some r => (p.1.1 + p.2.1, r :: p.2.2)) (augActionP t ×ˢ cutListSummandsP ts)

Recursive formula for cutListSummandsP on a cons list.

@[simp]

theorem RootedTree.ConnesKreimer.augActionP_eq {α : Type u_2} (t : RoseTree α) : augActionP t = ({t}, none) ::ₘ Multiset.map (fun (p : Forest (RoseTree α) × RoseTree α) => (p.1, some p.2)) (cutSummandsP t)

Recursive formula for augActionP.

comulTreeP — tree-level Δ^ρ

Sum the cut summands as tensors, plus the explicit T ⊗ 1 term.

noncomputable def RootedTree.ConnesKreimer.comulTreeP {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : RoseTree α) : TensorProduct R (ConnesKreimer R (RoseTree α)) (ConnesKreimer R (RoseTree α))

The tree-level Δ^ρ coproduct: explicit T ⊗ 1 term plus the sum of cut-summand tensors.

Equations

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

comulForestP — forest-level Δ^ρ

Multiplicative extension over the disjoint-union product on forests: Δ(F + G) = Δ(F) · Δ(G).

noncomputable def RootedTree.ConnesKreimer.comulForestP {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (RoseTree α)) : TensorProduct R (ConnesKreimer R (RoseTree α)) (ConnesKreimer R (RoseTree α))

The forest-level Δ^ρ: multiplicative product of tree-level coproducts over the components of the forest.

Equations

• RootedTree.ConnesKreimer.comulForestP F = (Multiset.map RootedTree.ConnesKreimer.comulTreeP F).prod

@[simp]

theorem RootedTree.ConnesKreimer.comulForestP_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : comulForestP 0 = 1

@[simp]

theorem RootedTree.ConnesKreimer.comulForestP_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : Forest (RoseTree α)) : comulForestP (F + G) = comulForestP F * comulForestP G

comulMonoidHom and comulAlgHom

Package the multiplicative extension as a MonoidHom, then lift to the full AlgHom via ConnesKreimer.lift.

noncomputable def RootedTree.ConnesKreimer.comulMonoidHomP {R : Type u_1} [CommSemiring R] {α : Type u_2} : Multiplicative (Forest (RoseTree α)) →* TensorProduct R (ConnesKreimer R (RoseTree α)) (ConnesKreimer R (RoseTree α))

comulForestP as a monoid hom from Multiplicative (Forest (RoseTree α)).

Equations

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

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

The Δ^ρ coproduct on ConnesKreimer R (RoseTree α) as an algebra hom.

Equations

• RootedTree.ConnesKreimer.comulAlgHomP = RootedTree.ConnesKreimer.lift RootedTree.ConnesKreimer.comulMonoidHomP

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomP_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (RoseTree α)) : comulAlgHomP (of' F) = comulForestP F

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomP_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : RoseTree α) : comulAlgHomP (ofTree T) = comulTreeP T