The deletion coproduct Δ^d

The deletion variant of the Connes-Kreimer admissible-cut coproduct ([MCB25] Lemma 1.3.10, p. 44), obtained from the trace coproduct Δ^c (Coproduct/Trace.lean) by erasing trace-placeholder leaves from both tensor channels: Δ^d = (Π_{d,c} ⊗ Π_{d,c}) ∘ Δ^c, where Π_{d,c} erases trace-placeholder leaves.

Main definitions

• ConnesKreimer.eraseTracesAlgHom — Π_{d,c} as an algebra hom ConnesKreimer R (Nonplanar (α ⊕ β)) →ₐ[R] ConnesKreimer R (Nonplanar α), induced by the tree-level partial map (Core/Data/RoseTree/FilterMap.lean) via ConnesKreimer.mapDomainAlgHom.
• ConnesKreimer.embedInlAlgHom — the Sum.inl embedding as an algebra hom.
• ConnesKreimer.comulDN — the deletion coproduct, as the composite above.

Main results

• ConnesKreimer.eraseTracesAlgHom_comp_embedInlAlgHom — erasure inverts the embedding.
• ConnesKreimer.comulDN_embedInl_eq_comulAlgHomN — on embedded trace-free trees, Δ^d agrees with the pruning coproduct Δ^ρ.

Implementation notes

[MCB25] work with binary trees: their Δ^d composes with a second projection Π_{d,p} contracting degree-1 vertices to restore binary structure, and their comparison Δ^d = (id ⊗ Π_{d,p}) ∘ Δ^ρ holds only weakly (Lemma 1.2.12, a distance-≤-1 multiplicity discrepancy). On n-ary Nonplanar trees Π_{d,p} is the identity, the erasure alone defines Δ^d, and the Δ^ρ comparison is an exact equality. We erase on both tensor channels so the target carrier is uniformly trace-free; on the embedded trace-free inputs of the comparison the crown-channel erasure is the identity, recovering MCB's one-channel form (id ⊗ Π_{d,c}) ∘ Δ^c.

Δ^d carries no separate Bialgebra structure: consumers compose through embedInlAlgHom and use the Δ^ρ instance (instBialgebraRho, Coproduct/PruningDuality.lean).

Status

[UPSTREAM] candidate.

The trace-erasure algebra hom Π_{d,c}

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

The trace-erasure algebra hom Π_{d,c}: erase trace subtrees componentwise across each basis forest, dropping trace-rooted trees (Multiset.filterMapAddMonoidHom (Nonplanar.filterMap Sum.getLeft?)), lifted through ConnesKreimer.mapDomainAlgHom.

Equations

• ConnesKreimer.eraseTracesAlgHom = ConnesKreimer.mapDomainAlgHom (Multiset.filterMapAddMonoidHom (RoseTree.Nonplanar.filterMap Sum.getLeft?))

@[simp]

theorem ConnesKreimer.eraseTracesAlgHom_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar (α ⊕ β))) : eraseTracesAlgHom (of' F) = of' (Multiset.filterMap (RoseTree.Nonplanar.filterMap Sum.getLeft?) F)

@[simp]

theorem ConnesKreimer.eraseTracesAlgHom_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (T : RoseTree.Nonplanar (α ⊕ β)) : eraseTracesAlgHom (ofTree T) = (RoseTree.Nonplanar.filterMap Sum.getLeft? T).elim 1 ofTree

eraseTracesAlgHom on a single tree: the trace-erased tree if the root survives, 1 if the root is a trace placeholder.

Sum.inl embedding

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

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

The Sum.inl embedding algebra hom: relabel every basis forest componentwise along Sum.inl, embedding trace-free trees into the marked alphabet.

Equations

• ConnesKreimer.embedInlAlgHom = ConnesKreimer.mapDomainAlgHom (Multiset.mapAddMonoidHom (RoseTree.Nonplanar.map Sum.inl))

@[simp]

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

Erasure inverts embed

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

Erasure inverts the Sum.inl embedding: trace-free trees survive the round trip.

Δ^d definition

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

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

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

Equations

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

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 erasure) 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 erasure is enough.

The cut-summand tensor builder

Option-tolerant on both channels: a filtered-out crown entry (none) is dropped, a filtered-out trunk contributes 1. The filtered Δ^c summands and the some-embedded Δ^ρ summands of Core/Combinatorics/RootedTree/CutFilterMap.lean both land in its domain.

Lift from tree-level to Nonplanar

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

On embedded trace-free trees the deletion coproduct agrees with the pruning coproduct Δ^ρ: the n-ary form of the [MCB25] comparison Δ^d = (id ⊗ Π_{d,p}) ∘ Δ^ρ, exact here because the rebinarize step Π_{d,p} is the identity.