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; the concrete coproducts are its instantiations — Δ^ρ at cuts := cutSummandsN (Coproduct/Pruning.lean) and Δ^c at cuts := cutSummandsCN τ (Coproduct/Trace.lean, definitionally).

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.
• comulTreeNG_eq_sum / comulForestNG_eq_sum — the coproduct as a single sum over the cut convolutions treeCutsG/forestCutsG (Combinatorics/RootedTree/Cut.lean).
• WithCuts R cuts — the policy-indexed carrier, with Bialgebra gated on IsAdmissibleCuts cuts.

noncomputable def ConnesKreimer.comulTreeNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) (T : RoseTree.Nonplanar α) : TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.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 ConnesKreimer.comulForestNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))

Forest-level generic coproduct (multiplicative extension).

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def ConnesKreimer.comulMonoidHomNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) : Multiplicative (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) →* TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.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 ConnesKreimer.comulAlgHomNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) : ConnesKreimer R (RoseTree.Nonplanar α) →ₐ[R] TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))

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

Equations

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

@[simp]

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

@[simp]

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

The generic coproduct as a sum over cut convolutions

treeCutsG/forestCutsG (Combinatorics/RootedTree/Cut.lean) enumerate the (crown, trunk-forest) pairs of a tree and their convolution over a forest; cutTensor sends a pair to of' crown ⊗ of' trunk. These single-sum expansions serve the Δ^ρ cocycle substrate (Coproduct/Pruning.lean) and the Δ^c double-cut coassoc proof (Coproduct/Trace.lean).

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

Tensor-product factor of a (crown, trunk) cut pair.

Equations

• ConnesKreimer.cutTensor p = ConnesKreimer.of' p.1 ⊗ₜ[R] ConnesKreimer.of' p.2

theorem ConnesKreimer.cutTensor_combinerProjG {R : Type u_1} [CommSemiring R] {α : Type u_2} (p q : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α) × RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : cutTensor (combinerProjG (p, q)) = cutTensor p * cutTensor q

cutTensor is multiplicative over the cut convolution combinerProjG.

theorem ConnesKreimer.comulTreeNG_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) (T : RoseTree.Nonplanar α) : comulTreeNG cuts T = (Multiset.map cutTensor (treeCutsG cuts T)).sum

comulTreeNG as a single multiset sum over treeCutsG.

theorem ConnesKreimer.comulForestNG_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : comulForestNG cuts F = (Multiset.map cutTensor (forestCutsG cuts F)).sum

comulForestNG as a single multiset sum over forestCutsG.

The policy-indexed carrier WithCuts

The WithLp pattern: a type synonym indexed by the cut policy, whose Bialgebra instance is gated on an admissibility mixin. Δ^ρ keeps the plain carrier (instBialgebraRho, the Hopf algebra of [MCB25] Lemma 1.2.11); the marked variants live here.

def ConnesKreimer.WithCuts (R : Type u_1) [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) : Type (max u_2 u_1)

Type synonym for ConnesKreimer R (Nonplanar α) carrying the generic admissible-cut coproduct at the fixed policy cuts.

Equations

• ConnesKreimer.WithCuts R cuts = ConnesKreimer R (RoseTree.Nonplanar α)

@[instance_reducible]

noncomputable instance ConnesKreimer.instCommSemiringWithCuts {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) : CommSemiring (WithCuts R cuts)

Equations

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

@[instance_reducible]

noncomputable instance ConnesKreimer.instAlgebraWithCuts {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) : Algebra R (WithCuts R cuts)

Equations

• ConnesKreimer.instAlgebraWithCuts cuts = { smul := ConnesKreimer.instAlgebraWithCuts._aux_1 cuts, algebraMap := ConnesKreimer.instAlgebraWithCuts._aux_3 cuts, commutes' := ⋯, smul_def' := ⋯ }

class ConnesKreimer.IsAdmissibleCuts {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) : Prop

Admissibility of a cut policy: the generic coproduct comulAlgHomNG cuts is coassociative and counital, uniformly in the coefficient ring. Gates the Bialgebra instance on WithCuts (the Fact-style mixin of the WithLp pattern).

• coassoc (R : Type u_3) [CommRing R] [CharZero R] [NoZeroDivisors R] : (↑(Algebra.TensorProduct.assoc R R R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α)))).comp ((Algebra.TensorProduct.map (comulAlgHomNG cuts) (AlgHom.id R (ConnesKreimer R (RoseTree.Nonplanar α)))).comp (comulAlgHomNG cuts)) = (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (RoseTree.Nonplanar α))) (comulAlgHomNG cuts)).comp (comulAlgHomNG cuts)
• counit_rTensor (R : Type u_4) [CommSemiring R] : (Algebra.TensorProduct.map counit (AlgHom.id R (ConnesKreimer R (RoseTree.Nonplanar α)))).comp (comulAlgHomNG cuts) = ↑(Algebra.TensorProduct.lid R (ConnesKreimer R (RoseTree.Nonplanar α))).symm
• counit_lTensor (R : Type u_5) [CommSemiring R] : (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (RoseTree.Nonplanar α))) counit).comp (comulAlgHomNG cuts) = ↑(Algebra.TensorProduct.rid R R (ConnesKreimer R (RoseTree.Nonplanar α))).symm

@[instance_reducible]

noncomputable instance ConnesKreimer.WithCuts.instBialgebra {α : Type u_2} (cuts : RoseTree.Nonplanar α → Multiset (Multiset (RoseTree.Nonplanar α) × RoseTree.Nonplanar α)) {R : Type u_3} [CommRing R] [CharZero R] [NoZeroDivisors R] [IsAdmissibleCuts cuts] : Bialgebra R (WithCuts R cuts)

The generic admissible-cut bialgebra on the marked carrier: any admissible policy yields Bialgebra R (WithCuts R cuts). Δ^c is recovered at cuts := cutSummandsCN τ.

Equations

• ConnesKreimer.WithCuts.instBialgebra cuts = Bialgebra.ofAlgHom (ConnesKreimer.comulAlgHomNG cuts) ConnesKreimer.counit ⋯ ⋯ ⋯