Δ^d on ConnesKreimer R (Nonplanar (α ⊕ β)) via projection from Δ^c

[MCB25]

The deletion variant of the Connes-Kreimer admissible-cut coproduct, derived from Δ^c (Coproduct/TraceNonplanar.lean) by stripping trace-placeholder leaves from the right channel — MCB Lemma 1.3.10 (p. 44):

Δ^d = (id ⊗ Π_{d,c}) ∘ Δ^c = (id ⊗ Π_{d,p}) ∘ Δ^ρ

where Π_{c,p} deletes trace-placeholder leaves and Π_{d,p} is the binary-rebinarize step.

In our n-ary substrate

MCB works with binary trees throughout. Their Π_{d,p} (the "rebinarize" step) contracts degree-1 vertices to recover binary structure. In our Nonplanar α substrate trees can be arbitrary n-ary, so Π_{d,p} is the identity: no degree-1 smoothing needed, no rebinarization step.

Δ^d in our setting therefore reduces to just the trace-strip projection from Δ^c:

Δ^d := (Π_{d,c} ⊗ Π_{d,c}) ∘ Δ^c

This file constructs Π_{d,c} as an algebra hom stripTraceAlgHom : ConnesKreimer R (Nonplanar (α ⊕ β)) →ₐ[R] ConnesKreimer R (Nonplanar α) and defines comulDN as the composition above.

Relationship to Δ^ρ

The Sum.inl embedding embedInlAlgHom : ConnesKreimer R (Nonplanar α) →ₐ ConnesKreimer R (Nonplanar (α ⊕ β)) (induced by Sum.inl : α → α ⊕ β) lets us compare:

comulDN ∘ embedInlAlgHom = comulAlgHomN (the equivalence theorem)

i.e., starting from a trace-free tree, applying Δ^c then stripping gives the same result as Δ^ρ directly. This is the n-ary specialization of MCB's Δ^d = (id ⊗ Π_{d,p}) ∘ Δ^ρ (since Π_{d,p} is identity here).

Bialgebra structure

Δ^d does not have a separate Bialgebra structure in this file. By the equivalence theorem, consumers wanting a Bialgebra should compose through embedInlAlgHom and use the Δ^ρ structure (PruningDuality.instBialgebraRho). MCB's Lemma 1.2.12 (Δ^d weak coassoc with distance-≤-1 multiplicity discrepancy) is specific to the binary Π_{d,p} step which is identity in our setting; in our n-ary substrate Δ^d ≡ Δ^ρ (modulo the embedding) has strict coassoc.

Status

[UPSTREAM] candidate. Sorry-free as of MCB Phase F.1 R.9 closure: comulDN_embedInl_eq_comulAlgHomN is now proven via tree-level mutual structural induction on tree / children-list, factoring the wrapper bPlusLin a out of the per-summand tensors so the head and tail induction hypotheses apply cleanly. The left-channel half uses stripTraceAlgHom_comp_embedInlAlgHom (strip inverts the Sum.inl embedding); the right-channel trace-removal uses strip_cutSummandsCP_sum_eq + strip_cutListSummandsG_unwrap_sum_eq.

Tree-level trace-strip projection

Strip trace-placeholder subtrees (Sum.inr-rooted subtrees) from a RoseTree (α ⊕ β) tree, yielding Option (RoseTree α) — the result is none only if the root itself is a trace placeholder.

The strip recurses into children via filterMap: each child is stripped, and none results are dropped.

def RootedTree.ConnesKreimer.RoseTree.mapList {α : Type u_2} {β : Type u_3} (f : α → β) (cs : List (RoseTree α)) : List (RoseTree β)

The children-list functor action mapList f = List.map (RoseTree.map f), named so the node-expansion of RoseTree.map reads structurally below.

Equations

• RootedTree.ConnesKreimer.RoseTree.mapList f cs = List.map (RoseTree.map f) cs

theorem RootedTree.ConnesKreimer.RoseTree.map_node_mapList {α : Type u_2} {β : Type u_3} (f : α → β) (a : α) (cs : List (RoseTree α)) : RoseTree.map f (RoseTree.node a cs) = RoseTree.node (f a) (mapList f cs)

RoseTree.map on a node, expressed through RoseTree.mapList.

def RootedTree.ConnesKreimer.RoseTree.stripTrace {α : Type u_2} {β : Type u_3} : RoseTree (α ⊕ β) → Option (RoseTree α)

Strip trace-placeholder subtrees from a tree-level tree. Returns none if the root is a trace placeholder (Sum.inr-labeled).

Equations

• RootedTree.ConnesKreimer.RoseTree.stripTrace (RoseTree.node (Sum.inr val) children) = none
• RootedTree.ConnesKreimer.RoseTree.stripTrace (RoseTree.node (Sum.inl a) cs) = some (RoseTree.node a (RootedTree.ConnesKreimer.RoseTree.stripTraceList cs))

def RootedTree.ConnesKreimer.RoseTree.stripTraceList {α : Type u_2} {β : Type u_3} : List (RoseTree (α ⊕ β)) → List (RoseTree α)

Auxiliary: strip each tree in a children list, dropping nones.

Equations

• One or more equations did not get rendered due to their size.
• RootedTree.ConnesKreimer.RoseTree.stripTraceList [] = []

@[simp]

theorem RootedTree.ConnesKreimer.RoseTree.stripTrace_inr {α : Type u_2} {β : Type u_3} (b : β) (cs : List (RoseTree (α ⊕ β))) : stripTrace (RoseTree.node (Sum.inr b) cs) = none

@[simp]

theorem RootedTree.ConnesKreimer.RoseTree.stripTrace_inl {α : Type u_2} {β : Type u_3} (a : α) (cs : List (RoseTree (α ⊕ β))) : stripTrace (RoseTree.node (Sum.inl a) cs) = some (RoseTree.node a (stripTraceList cs))

@[simp]

theorem RootedTree.ConnesKreimer.RoseTree.stripTraceList_nil {α : Type u_2} {β : Type u_3} : stripTraceList [] = []

Descent to Nonplanar

Lift RoseTree.stripTrace through the quotient. The lift requires that stripTrace ∘ Nonplanar.mk be well-defined modulo PermEquiv, which holds because:

• PermEquiv permutes children; stripTraceList commutes with permutations up to List.Perm on the resulting list.
• At the Nonplanar.mk level, child-list order collapses, so PermEquiv-related stripped trees become equal.

noncomputable def RootedTree.ConnesKreimer.Nonplanar.stripTrace {α : Type u_2} {β : Type u_3} : Nonplanar (α ⊕ β) → Option (Nonplanar α)

Strip trace-placeholder subtrees from a Nonplanar tree.

Equations

• RootedTree.ConnesKreimer.Nonplanar.stripTrace = Quotient.lift RootedTree.ConnesKreimer.stripTraceQuotient✝ ⋯

@[simp]

theorem RootedTree.ConnesKreimer.Nonplanar.stripTrace_mk {α : Type u_2} {β : Type u_3} (t : RoseTree (α ⊕ β)) : stripTrace (Nonplanar.mk t) = Option.map Nonplanar.mk (RoseTree.stripTrace t)

Forest-level strip

Map Nonplanar.stripTrace over each tree in the forest, dropping the none results via Multiset.filterMap. The result is a forest in Nonplanar α.

noncomputable def RootedTree.ConnesKreimer.stripTraceForestAddHom {α : Type u_2} {β : Type u_3} : Forest (Nonplanar (α ⊕ β)) →+ Forest (Nonplanar α)

The additive monoid hom from forests in Nonplanar (α ⊕ β) to forests in Nonplanar α, given by stripping each tree componentwise and dropping the trace-rooted ones.

Equations

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

AlgHom lift — Π_{d,c}

The trace-strip algebra hom Π_{d,c} in MCB's notation.

noncomputable def RootedTree.ConnesKreimer.stripTraceAlgHom {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} : ConnesKreimer R (Nonplanar (α ⊕ β)) →ₐ[R] ConnesKreimer R (Nonplanar α)

The trace-strip algebra hom Π_{d,c} — ConnesKreimer R (Nonplanar (α ⊕ β)) →ₐ[R] ConnesKreimer R (Nonplanar α) induced by stripTraceForestAddHom via ConnesKreimer.mapDomainAlgHom.

Equations

• RootedTree.ConnesKreimer.stripTraceAlgHom = RootedTree.ConnesKreimer.mapDomainAlgHom RootedTree.ConnesKreimer.stripTraceForestAddHom

@[simp]

theorem RootedTree.ConnesKreimer.stripTraceAlgHom_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (F : Forest (Nonplanar (α ⊕ β))) : stripTraceAlgHom (of' F) = of' (Multiset.filterMap Nonplanar.stripTrace F)

Sum.inl embedding

The embedding α → α ⊕ β lifts componentwise to trees and forests via RoseTree.map / Nonplanar.map / Multiset.map.

def RootedTree.ConnesKreimer.Nonplanar.embedInl {α : Type u_2} {β : Type u_3} : Nonplanar α → Nonplanar (α ⊕ β)

Embed a Nonplanar α tree into Nonplanar (α ⊕ β) via Sum.inl.

Equations

• RootedTree.ConnesKreimer.Nonplanar.embedInl = RootedTree.Nonplanar.map Sum.inl

noncomputable def RootedTree.ConnesKreimer.embedInlForestAddHom {α : Type u_2} {β : Type u_3} : Forest (Nonplanar α) →+ Forest (Nonplanar (α ⊕ β))

Embed a forest of Nonplanar α trees into a forest of Nonplanar (α ⊕ β) trees, componentwise.

Equations

• RootedTree.ConnesKreimer.embedInlForestAddHom = Multiset.mapAddMonoidHom RootedTree.ConnesKreimer.Nonplanar.embedInl

noncomputable def RootedTree.ConnesKreimer.embedInlAlgHom {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} : ConnesKreimer R (Nonplanar α) →ₐ[R] ConnesKreimer R (Nonplanar (α ⊕ β))

The Sum.inl embedding algebra hom ConnesKreimer R (Nonplanar α) →ₐ[R] ConnesKreimer R (Nonplanar (α ⊕ β)) induced by Nonplanar.embedInl via ConnesKreimer.mapDomainAlgHom.

Equations

• RootedTree.ConnesKreimer.embedInlAlgHom = RootedTree.ConnesKreimer.mapDomainAlgHom RootedTree.ConnesKreimer.embedInlForestAddHom

@[simp]

theorem RootedTree.ConnesKreimer.embedInlAlgHom_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (F : Forest (Nonplanar α)) : embedInlAlgHom (of' F) = of' (Multiset.map Nonplanar.embedInl F)

Strip inverts embed

RoseTree.stripTrace (RoseTree.map Sum.inl p) = some p — embedding via Sum.inl then stripping recovers the original. Proven by mutual structural induction on the tree-level tree / its child list. Descends to the Nonplanar level via Quotient.inductionOn, and lifts to the algebra-hom level: stripTraceAlgHom ∘ embedInlAlgHom = id.

theorem RootedTree.ConnesKreimer.Nonplanar.stripTrace_embedInl {α : Type u_2} {β : Type u_3} (T : Nonplanar α) : stripTrace (embedInl T) = some T

theorem RootedTree.ConnesKreimer.stripTrace_embedInl_filterMap {α : Type u_2} {β : Type u_3} (F : Forest (Nonplanar α)) : Multiset.filterMap Nonplanar.stripTrace (Multiset.map Nonplanar.embedInl F) = F

stripTrace ∘ embedInl = some (as forest-level filterMap = identity). This is the multiset-level version of Nonplanar.stripTrace_embedInl.

theorem RootedTree.ConnesKreimer.stripTraceAlgHom_comp_embedInlAlgHom {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} : stripTraceAlgHom.comp embedInlAlgHom = AlgHom.id R (ConnesKreimer R (Nonplanar α))

stripTraceAlgHom ∘ embedInlAlgHom = id. The strip inverts the Sum.inl embedding at the AlgHom level: trace-free trees survive a round-trip through embedding + stripping.

Δ^d definition

comulDN := (Π_{d,c} ⊗ Π_{d,c}) ∘ Δ^c — MCB Lemma 1.3.10 by construction. Target carrier is Nonplanar α (trace-stripped).

noncomputable def RootedTree.ConnesKreimer.comulDN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : ConnesKreimer R (Nonplanar (α ⊕ β)) →ₐ[R] TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

The Δ^d coproduct on ConnesKreimer R (Nonplanar (α ⊕ β)) as an algebra hom, with trace-stripping applied to both channels of comulCAlgHomN τ.

Equations

• RootedTree.ConnesKreimer.comulDN τ = (Algebra.TensorProduct.map RootedTree.ConnesKreimer.stripTraceAlgHom RootedTree.ConnesKreimer.stripTraceAlgHom).comp (RootedTree.comulCAlgHomN τ)

theorem RootedTree.ConnesKreimer.comulDN_eq_strip_comp_comulCAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : comulDN τ = (Algebra.TensorProduct.map stripTraceAlgHom stripTraceAlgHom).comp (comulCAlgHomN τ)

MCB Lemma 1.3.10 (definitional in our construction): Δ^d = (Π_{d,c} ⊗ Π_{d,c}) ∘ Δ^c.

Equivalence with Δ^ρ via embedding

The substantive MCB-correspondence: starting from a trace-free T : Nonplanar α and embedding into Nonplanar (α ⊕ β) via Sum.inl, applying comulDN (= Δ^c then strip) gives the same result as applying comulAlgHomN (Δ^ρ) directly.

In MCB's binary substrate this requires the additional Π_{d,p} rebinarize step on the right channel; in our n-ary substrate, the strip is enough.

RoseTree-level cut-tensor builders

The tensors that arise when applying (S ⊗ S) to comulCTreeN's cut summands on the LHS, and to comulTreeN's cut summands on the RHS, both viewed at the Nonplanar α level.

Multiplicativity of cut-tensor builders under combine

Both unwrapped builders factor through the cons combiners as products.

theorem RootedTree.ConnesKreimer.cutListSummandsP_cons' {α : Type u_2} (t : RoseTree α) (ts : List (RoseTree α)) : cutListSummandsP (t :: ts) = Multiset.map RootedTree.ConnesKreimer.combineP_fn✝ (augActionP t ×ˢ cutListSummandsP ts)

Sum-of-product over cartesian product

Standard distributivity: when the integrand factors as f a * g b over s ×ˢ t, the sum equals (s.map f).sum * (t.map g).sum.

Universal identity: unwrapped tensor for singleton-remainder

For any t_c : RoseTree (α ⊕ β) (regardless of root), the unwrapped cutTensor for (F, [t_c]) equals cutTensorC_planar (F, t_c). This holds for both Sum.inl-rooted t_c (where strip succeeds, yielding the stripped tree) and Sum.inr-rooted t_c (where both sides reduce to ... ⊗ 1).

Mutual tree-level lemmas

The tree-level lemma uses the unwrapped list-level lemma (applied to children of the tree, with the root wrapped via bPlusLin on the right channel). The list-level lemma's cons case uses the tree-level lemma for the head child (via mutual call) + the unwrapped list-level lemma for the tail (via direct call).

Lift from tree-level to Nonplanar

theorem RootedTree.ConnesKreimer.comulDN_embedInl_eq_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : (comulDN τ).comp embedInlAlgHom = comulAlgHomN

MCB equivalence (n-ary specialization): the Δ^d-via-Δ^c construction agrees with Δ^ρ on trace-free trees.

comulDN ∘ embed_{Sum.inl} = comulAlgHomN

Closed via: (a) AlgHom extensionality + ConnesKreimer.induction_linear reduces to per-basis of' F; (b) Multiset multiplicativity of comulCForestN, comulForestN, and (stripTraceAlgHom ⊗ stripTraceAlgHom) reduces to per-tree; (c) Quotient.inductionOn reduces per-tree to tree-level; (d) tree-level mutual structural induction on tree / children-list closes the cut-summand bijection via strip_cutSummandsCP_sum_eq.