Generic admissible-cut coproduct on ConnesKreimer R (Nonplanar α)

[MCB25]

The three MCB coproducts — Δ^ρ (pruning), Δ^c (contraction/trace), Δ^d (deletion) — share one shape: a primitive ofTree T ⊗ 1 plus a sum over cut summands (crown, trunk) of of' crown ⊗ ofTree trunk. They differ only in the cut enumeration cuts T. This file factors that shape into a single cuts-parameterized algebra hom comulAlgHomNG, recovering the existing comulTreeN/comulAlgHomN (Δ^ρ, cuts := cutSummandsN) and comulCTreeN/comulCAlgHomN τ (Δ^c, cuts := cutSummandsCN τ) as instances — the bridges are definitional (rfl).

The cut-enumeration layer was already generic (ConnesKreimer.cutSummandsG, over an extraction policy); this lifts that genericity to the coproduct operator, so one Merge operator (Minimalist.Merge.mergeOpG, downstream) serves every coproduct instead of one bespoke copy per Δ.

Main definitions

• comulTreeNG cuts / comulForestNG cuts — the generic coproduct.
• comulAlgHomNG cuts — packaged as an AlgHom.
• comulTreeN_eq_G, comulCTreeN_eq_G, comulAlgHomN_eq_G, comulCAlgHomN_eq_G — the Δ^ρ / Δ^c instance bridges.

noncomputable def RootedTree.ConnesKreimer.comulTreeNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) (T : Nonplanar α) : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

The generic admissible-cut coproduct (tree level), parameterized by a cut enumeration cuts. Specializing cuts to cutSummandsN gives Δ^ρ, to cutSummandsCN τ gives Δ^c, to the deletion enumeration gives Δ^d.

Equations

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

noncomputable def RootedTree.ConnesKreimer.comulForestNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) (F : Forest (Nonplanar α)) : TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

Forest-level generic coproduct (multiplicative extension).

Equations

• RootedTree.ConnesKreimer.comulForestNG cuts F = (Multiset.map (RootedTree.ConnesKreimer.comulTreeNG cuts) F).prod

@[simp]

theorem RootedTree.ConnesKreimer.comulForestNG_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) : comulForestNG cuts 0 = 1

@[simp]

theorem RootedTree.ConnesKreimer.comulForestNG_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) (F G : Forest (Nonplanar α)) : comulForestNG cuts (F + G) = comulForestNG cuts F * comulForestNG cuts G

@[simp]

theorem RootedTree.ConnesKreimer.comulForestNG_cons {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) (T : Nonplanar α) (F : Forest (Nonplanar α)) : comulForestNG cuts (T ::ₘ F) = comulTreeNG cuts T * comulForestNG cuts F

noncomputable def RootedTree.ConnesKreimer.comulMonoidHomNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) : Multiplicative (Forest (Nonplanar α)) →* TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

Forest-level generic coproduct as a MonoidHom on the additive forest monoid.

Equations

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

noncomputable def RootedTree.ConnesKreimer.comulAlgHomNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) : ConnesKreimer R (Nonplanar α) →ₐ[R] TensorProduct R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α))

The generic admissible-cut coproduct as an algebra hom, parameterized by the cut enumeration cuts.

Equations

• RootedTree.ConnesKreimer.comulAlgHomNG cuts = RootedTree.ConnesKreimer.lift (RootedTree.ConnesKreimer.comulMonoidHomNG cuts)

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomNG_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) (F : Forest (Nonplanar α)) : (comulAlgHomNG cuts) (of' F) = comulForestNG cuts F

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomNG_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)) (T : Nonplanar α) : (comulAlgHomNG cuts) (ofTree T) = comulTreeNG cuts T

Instance bridges (Δ^ρ, Δ^c) — definitional

theorem RootedTree.ConnesKreimer.comulTreeN_eq_G {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) : comulTreeN T = comulTreeNG cutSummandsN T

Δ^ρ is the generic coproduct at cuts := cutSummandsN.

theorem RootedTree.ConnesKreimer.comulCTreeN_eq_G {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) (T : Nonplanar (α ⊕ β)) : comulCTreeN τ T = comulTreeNG (cutSummandsCN τ) T

Δ^c is the generic coproduct at cuts := cutSummandsCN τ.

theorem RootedTree.ConnesKreimer.comulAlgHomN_eq_G {R : Type u_1} [CommSemiring R] {α : Type u_2} : comulAlgHomN = comulAlgHomNG cutSummandsN

theorem RootedTree.ConnesKreimer.comulCAlgHomN_eq_G {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : Nonplanar (α ⊕ β) → β) : comulCAlgHomN τ = comulAlgHomNG (cutSummandsCN τ)