Δ^ρ on ConnesKreimer R (Nonplanar α) via projection from Planar

@cite{marcolli-chomsky-berwick-2025} @cite{foissy-introduction-hopf-algebras-trees}

The Nonplanar Δ^ρ is obtained by descending the planar Δ^ρ (Coproduct.lean) through the projection mk : Planar α → Nonplanar α. The descent requires showing that the projected cut summands ((cutSummandsP T).map projSummand) depend on T : Planar α only through mk T, i.e., are invariant under Planar.PlanarEquiv. Once established, Nonplanar.lift produces cutSummandsN, which extends to comulTreeN, comulForestN, and the algebra hom comulAlgHomN.

Status

[UPSTREAM] candidate. Sorry-free for the full Bialgebra structure: the descent (comulAlgHomN), the Hochschild 1-cocycle (comulTreeN_node_cocycle, comulAlgHomN_bPlusLin_cocycle), Foissy clean coassoc (coassocSubalg_eq_top), the counit laws (counit_rTensor_comulAlgHomN, counit_lTensor_comulAlgHomN), and the Bialgebra (ConnesKreimer R (Nonplanar α)) instance.

The full HopfAlgebra instance (with antipode) lives in the sibling HopfAlgebraNonplanar.lean (Phase A.8).

Architecture

• Projection algebra hom (planarToNonplanarAlg): directly on top of mathlib's AddMonoidAlgebra.mapDomainAlgHom, applied to the additive monoid hom Multiset.mapAddMonoidHom Nonplanar.mk. The universal property of AddMonoidAlgebra does the heavy lifting.
• Cut-summand descent (§3): pointwise projection (projSummand/projForest/projAugAction) plus a clean factoring of the cutListSummandsP cons case as a Nonplanar-level cartesian product (cutListSummandsP_cons_proj); structural induction on PlanarStep for the headline invariance, with pure EqvGen/Forall₂ lifts for PlanarEquiv and List.Forall₂ versions.

Projection algebra hom Planar → Nonplanar

Nonplanar.mk : Planar α → Nonplanar α extends to an algebra hom on ConnesKreimer R via AddMonoidAlgebra.mapDomainAlgHom. Surjective at the carrier level; the kernel encodes PlanarEquiv-equivalence of forests of trees, which is what subsequent sub-phases will need to factor through.

noncomputable def RootedTree.ConnesKreimer.forestProjAddHom {α : Type u_2} : Forest (Planar α) →+ Forest (Nonplanar α)

The additive monoid hom from forests of planar trees to forests of nonplanar trees, given by mapping Nonplanar.mk componentwise.

Equations

• RootedTree.ConnesKreimer.forestProjAddHom = Multiset.mapAddMonoidHom RootedTree.Nonplanar.mk

noncomputable def RootedTree.ConnesKreimer.planarToNonplanarAlg {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (Planar α) →ₐ[R] ConnesKreimer R (Nonplanar α)

The projection algebra hom ConnesKreimer R (Planar α) →ₐ[R] ConnesKreimer R (Nonplanar α) induced by Nonplanar.mk.

Equations

• RootedTree.ConnesKreimer.planarToNonplanarAlg = AddMonoidAlgebra.mapDomainAlgHom R R RootedTree.ConnesKreimer.forestProjAddHom

API lemmas — action on of' and ofTree

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (Planar α)) : planarToNonplanarAlg (of' F) = of' (Multiset.map Nonplanar.mk F)

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (t : Planar α) : planarToNonplanarAlg (ofTree t) = ofTree (Nonplanar.mk t)

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_one {R : Type u_1} [CommSemiring R] {α : Type u_2} : planarToNonplanarAlg 1 = 1

@[simp]

theorem RootedTree.ConnesKreimer.planarToNonplanarAlg_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : ConnesKreimer R (Planar α)) : planarToNonplanarAlg (x * y) = planarToNonplanarAlg x * planarToNonplanarAlg y

Phase A.7-β — projection of cut summands, descent of Δ^ρ

To descend Δ^ρ from Planar to Nonplanar, we need a Nonplanar-side cut-summand multiset that is PlanarEquiv-invariant. The strategy: project each planar cut summand through mk componentwise, then prove the resulting multiset depends on T : Planar α only through mk T.

The proof factors through three layers:

• Pointwise projection (projSummand, projForest, projAugAction): the per-element Nonplanar.mk lifts.
• Combine factoring (cutListSummandsP_cons_proj): the cons case of cutListSummandsP distributes over the projection, giving a clean cartesian-product recursion at the Nonplanar level.
• Headline lifts (cutSummandsP_proj_planarStep, cutSummandsP_proj_planarEquiv, cutListSummandsP_proj_componentwise): structural induction on PlanarStep for the substantive content; pure EqvGen / Forall₂ lifts for the rest.

Pointwise projection

def RootedTree.ConnesKreimer.projSummand {α : Type u_2} : Forest (Planar α) × Planar α → Forest (Nonplanar α) × Nonplanar α

Project a planar cut summand to a nonplanar one.

Equations

• RootedTree.ConnesKreimer.projSummand p = (Multiset.map RootedTree.Nonplanar.mk p.1, RootedTree.Nonplanar.mk p.2)

def RootedTree.ConnesKreimer.projForest {α : Type u_2} : Forest (Planar α) × List (Planar α) → Forest (Nonplanar α) × Multiset (Nonplanar α)

Project a cutListSummandsP summand to nonplanar level, discarding the list-order of the remainder children. The discarded order doesn't affect the eventual mk (.node a remainder), since mk is invariant under children-list permutation (Planar.planarEquiv_root_perm).

Equations

• RootedTree.ConnesKreimer.projForest p = (Multiset.map RootedTree.Nonplanar.mk p.1, ↑(List.map RootedTree.Nonplanar.mk p.2))

def RootedTree.ConnesKreimer.projAugAction {α : Type u_2} : Forest (Planar α) × Option (Planar α) → Forest (Nonplanar α) × Option (Nonplanar α)

Project an augActionP summand to nonplanar level (per-child decision).

Equations

• RootedTree.ConnesKreimer.projAugAction p = (Multiset.map RootedTree.Nonplanar.mk p.1, Option.map RootedTree.Nonplanar.mk p.2)

theorem RootedTree.ConnesKreimer.projSummand_node_factors {α : Type u_2} (a : α) (p : Forest (Planar α) × List (Planar α)) : projSummand (p.1, Planar.node a p.2) = ((projForest p).1, Nonplanar.node a (projForest p).2)

Bridge: applying cutSummandsP_node's wrapper (p.1, .node a p.2) then projSummand factors through projForest followed by the Nonplanar.node a smart constructor.

Combine factoring through projection

The cons case of cutListSummandsP combines a per-child decision (augActionP) with the cut-summands of the remaining children. This combination distributes over the Nonplanar projection: the "projected combiner" innerCombinerProj operates on (Forest × Option) × (Forest × Multiset) and matches projForest of the inline planar combiner. The headline result is cutListSummandsP_cons_proj, which expresses the cons case of the projected cutListSummandsP as a clean cartesian product at the Nonplanar level.

Cartesian-product distributivity

The pair-componentwise Prod.map distributes over Multiset.product (×ˢ). Mathlib has the bind-side analogues but not this exact form for multiset products; the proof is one inductive line via cons_product.

Headline factoring: cons case of projected cutListSummandsP

List-side projection invariants

These three theorems establish that the projected cutListSummandsP is invariant under (1) substituting an "augAction-projection-equal" child, (2) substituting a "projForest-equal" tail, and (3) any list permutation.

theorem RootedTree.ConnesKreimer.cutListSummandsP_proj_perm {α : Type u_2} {cs ds : List (Planar α)} (h : cs.Perm ds) : Multiset.map projForest (cutListSummandsP cs) = Multiset.map projForest (cutListSummandsP ds)

The projected cutListSummandsP is List.Perm-invariant: two permutation-related child lists yield the same projected cut-summand multiset.

Headline: PlanarStep + EqvGen lift

Substantive content: cutSummandsP_proj_planarStep proves projection invariance under a single elementary step (PlanarStep). The PlanarEquiv (EqvGen) and Forall₂ versions follow as straightforward lifts. The structural induction on PlanarStep handles the recursion: the recurse case calls itself on a strictly smaller child tree.

theorem RootedTree.ConnesKreimer.cutSummandsP_proj_planarStep {α : Type u_2} {t s : Planar α} (h : t.PlanarStep s) : Multiset.map projSummand (cutSummandsP t) = Multiset.map projSummand (cutSummandsP s)

Projection invariance under a single PlanarStep. Structural induction on the step constructor: swapAtRoot uses cutListSummandsP_proj_perm; recurse uses the inductive hypothesis combined with cutListSummandsP_proj_at_via_augAction.

theorem RootedTree.ConnesKreimer.cutSummandsP_proj_planarEquiv {α : Type u_2} {t s : Planar α} (h : t.PlanarEquiv s) : Multiset.map projSummand (cutSummandsP t) = Multiset.map projSummand (cutSummandsP s)

Projection invariance under PlanarEquiv. Pure EqvGen lift of cutSummandsP_proj_planarStep.

theorem RootedTree.ConnesKreimer.cutListSummandsP_proj_componentwise {α : Type u_2} {cs ds : List (Planar α)} (h : List.Forall₂ Planar.PlanarEquiv cs ds) : Multiset.map projForest (cutListSummandsP cs) = Multiset.map projForest (cutListSummandsP ds)

Componentwise PlanarEquiv invariance for child lists. Pure Forall₂ induction using cutListSummandsP_proj_at_via_augAction on the head and the IH on the tail.

Δ^ρ on Nonplanar via descent

The cutSummandsP_proj_planarEquiv invariance lifts cutSummandsP through Nonplanar.lift, giving a well-defined cutSummandsN. The tree-level coproduct comulTreeN then extends multiplicatively to a forest-level monoid hom and finally to the algebra hom comulAlgHomN.

noncomputable def RootedTree.ConnesKreimer.cutSummandsN {α : Type u_2} : Nonplanar α → Multiset (Forest (Nonplanar α) × Nonplanar α)

The Nonplanar cut-summand multiset, defined via Nonplanar.lift using the cutSummandsP_proj_planarEquiv invariance.

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.cutSummandsN_mk {α : Type u_2} (T : Planar α) : cutSummandsN (Nonplanar.mk T) = Multiset.map projSummand (cutSummandsP T)

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

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

Equations

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

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

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

Equations

• RootedTree.ConnesKreimer.comulForestN F = (Multiset.map RootedTree.ConnesKreimer.comulTreeN F).prod

@[simp]

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

@[simp]

theorem RootedTree.ConnesKreimer.comulForestN_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : Forest (Nonplanar α)) : comulForestN (F + G) = comulForestN F * comulForestN G

@[simp]

theorem RootedTree.ConnesKreimer.comulForestN_cons {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) : comulForestN (T ::ₘ F) = comulTreeN T * comulForestN F

Recursive formula: comulForestN (T ::ₘ F) = comulTreeN T * comulForestN F.

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

comulForestN packaged as a MonoidHom from Multiplicative (Forest (Nonplanar α)).

Equations

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

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

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

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomN_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (Nonplanar α)) : comulAlgHomN (of' F) = comulForestN F

@[simp]

theorem RootedTree.ConnesKreimer.comulAlgHomN_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) : comulAlgHomN (ofTree T) = comulTreeN T

Phase A.7-γ — Hochschild 1-cocycle for B+_a

B+_a : Forest (Nonplanar α) → Nonplanar α is the smart constructor Nonplanar.node a. Linearly extended to bPlusLin a : H →ₗ[R] H (sending basis element of' F to ofTree (Nonplanar.node a F)), it satisfies the Hochschild 1-cocycle property (Foissy / MCB §1.2.11):

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

i.e., for every x : H:

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

This is the algebraic input to Foissy's clean inductive proof of coassociativity (§A.7-δ): the subalgebra A := {x | (Δ ⊗ id)(Δ x) = (id ⊗ Δ)(Δ x)} is closed under B+_a, contains all leaves (which are B+_a 1), hence equals the whole algebra.

B+_a as a function, smart constructor, and linear map

noncomputable def RootedTree.ConnesKreimer.bPlus {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : Nonplanar α

The B+_a operator: graft an unordered forest of Nonplanar trees under a new root labeled a. Identical to the smart constructor.

Equations

• RootedTree.ConnesKreimer.bPlus a F = RootedTree.Nonplanar.node a F

@[simp]

theorem RootedTree.ConnesKreimer.bPlus_def {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : bPlus a F = Nonplanar.node a F

noncomputable def RootedTree.ConnesKreimer.bPlusLin {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : ConnesKreimer R (Nonplanar α) →ₗ[R] ConnesKreimer R (Nonplanar α)

The B+_a linear map: linearly extend the smart constructor bPlus a to an R-linear endomorphism of ConnesKreimer R (Nonplanar α), sending the basis element of' F to ofTree (Nonplanar.node a F).

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.bPlusLin_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : (bPlusLin a) (of' F) = ofTree (Nonplanar.node a F)

@[simp]

theorem RootedTree.ConnesKreimer.bPlusLin_one {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : (bPlusLin a) 1 = ofTree (Nonplanar.leaf a)

augActionN and cutForestSummandsN substrate

cutForestSummandsN F is the Nonplanar-level multiset of (cut_forest, remainder_forest) pairs ranging over per-tree decisions on the forest F. Each per-tree decision (augActionN T) is either "extract T whole" (pair ({T}, none)) or "recurse with a cut summand of T" (pair (s.1, some s.2) for s ∈ cutSummandsN T).

Defined recursively at the Nonplanar level via Multiset.foldr, with the LeftCommutative obligation discharged by swap_double_combinerProj (the per-tree-decision swap symmetry, established for the planar projection in §3 above and reused here verbatim).

noncomputable def RootedTree.ConnesKreimer.augActionN {α : Type u_2} (T : Nonplanar α) : Multiset (Forest (Nonplanar α) × Option (Nonplanar α))

Per-tree decision multiset at the Nonplanar level: extract this tree whole (({T}, none)), or recurse into a cut summand.

Equations

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

noncomputable def RootedTree.ConnesKreimer.cutForestSummandsN {α : Type u_2} (F : Forest (Nonplanar α)) : Multiset (Forest (Nonplanar α) × Forest (Nonplanar α))

The forest cut summand multiset: every per-tree decision tuple on F : Forest (Nonplanar α) produces a pair (cut_forest, remainder_forest), and cutForestSummandsN F enumerates them all (as a multiset). The public Nonplanar-level analog of (cutListSummandsP ps).map projForest, independent of the planar list representation.

Equations

• RootedTree.ConnesKreimer.cutForestSummandsN F = Multiset.foldr RootedTree.ConnesKreimer.cutForestCombinerN✝ {(0, 0)} F

@[simp]

theorem RootedTree.ConnesKreimer.cutForestSummandsN_zero {α : Type u_2} : cutForestSummandsN 0 = {(0, 0)}

@[simp]

theorem RootedTree.ConnesKreimer.cutForestSummandsN_cons {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) : cutForestSummandsN (T ::ₘ F) = Multiset.map RootedTree.ConnesKreimer.innerCombinerProj✝ (augActionN T ×ˢ cutForestSummandsN F)

Bridges to the planar list representation

The planar substrate cutListSummandsP (defined on List (Planar α)) is reused to evaluate cutForestSummandsN on a planar list rep, and to characterize cuts of a Nonplanar node. These bridges are private — the public cutSummandsN_node and comulForestN_eq_sum are stated purely at the Nonplanar level.

Tensor-algebra and multiset distributivity helpers

Public API

The two structural facts that drive the cocycle: cuts of a node decompose along cutForestSummandsN, and comulForestN expands as the multiset sum over cutForestSummandsN. Both are pure Nonplanar-level statements; planar substrate is invisible to consumers.

@[simp]

theorem RootedTree.ConnesKreimer.cutSummandsN_node {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : cutSummandsN (Nonplanar.node a F) = Multiset.map (fun (pf : Forest (Nonplanar α) × Forest (Nonplanar α)) => (pf.1, Nonplanar.node a pf.2)) (cutForestSummandsN F)

Cuts of Nonplanar.node a F decompose along the per-tree decisions of F: each pair (cf, rem) ∈ cutForestSummandsN F gives a cut summand (cf, Nonplanar.node a rem). The Nonplanar-level form.

theorem RootedTree.ConnesKreimer.comulForestN_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : Forest (Nonplanar α)) : comulForestN F = (Multiset.map (fun (pf : Forest (Nonplanar α) × Forest (Nonplanar α)) => of' pf.1 ⊗ₜ[R] of' pf.2) (cutForestSummandsN F)).sum

The forest coproduct comulForestN F expands as a multiset sum of of' cf ⊗ of' rem over (cf, rem) ∈ cutForestSummandsN F.

The cocycle theorem (basis-level)

@[simp]

theorem RootedTree.ConnesKreimer.node_zero_eq_leaf {α : Type u_2} (a : α) : Nonplanar.node a 0 = Nonplanar.leaf a

For the empty forest: Nonplanar.node a 0 = Nonplanar.leaf a.

theorem RootedTree.ConnesKreimer.cutSummandsN_leaf {α : Type u_2} (a : α) : cutSummandsN (Nonplanar.leaf a) = {(0, Nonplanar.leaf a)}

The cut summands of a leaf: only one summand (0, leaf a), corresponding to the empty cut.

theorem RootedTree.ConnesKreimer.comulTreeN_leaf {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : comulTreeN (Nonplanar.leaf a) = ofTree (Nonplanar.leaf a) ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ofTree (Nonplanar.leaf a)

The tree-level coproduct on a leaf: comulTreeN (leaf a) = ofTree (leaf a) ⊗ 1 + 1 ⊗ ofTree (leaf a).

theorem RootedTree.ConnesKreimer.comulTreeN_node_cocycle {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : comulTreeN (Nonplanar.node a F) = ofTree (Nonplanar.node a F) ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (Nonplanar α)) (bPlusLin a)) (comulForestN F)

The Hochschild 1-cocycle property of B+_a, on basis elements: for every forest F, the coproduct of the grafted tree Nonplanar.node a F decomposes as the explicit primitive term plus the right-channel B+ application of comulForestN F. Proven via the substrate cutSummandsN_node (cuts of a node decompose along cutForestSummandsN F) and comulForestN_eq_sum (forest coproduct expands as the matching multiset sum); the LinearMap.lTensor distributes over the sum via map_multiset_sum, and the per-summand check reduces to LinearMap.lTensor_tmul + bPlusLin_of'.

theorem RootedTree.ConnesKreimer.comulAlgHomN_bPlusLin_cocycle {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : comulAlgHomN ((bPlusLin a) (of' F)) = (bPlusLin a) (of' F) ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (Nonplanar α)) (bPlusLin a)) (comulAlgHomN (of' F))

The cocycle, lifted to the algebra-hom level on tree basis elements.

Phase A.7-δ — Foissy clean coassoc + Bialgebra instance

Foissy's clean proof: define A := { x : H | (id ⊗ Δ)(Δ x) = assoc((Δ ⊗ id)(Δ x)) } as the equalizer of two algebra homs H →ₐ[R] H ⊗ H ⊗ H. By the cocycle comulTreeN_node_cocycle, A is closed under B+_a; by tree induction, A contains every ofTree T and hence (closed under sum and product) all of H. Therefore A = ⊤, giving coassociativity of Δ. The counit laws follow analogously by reducing to the tree case via AddMonoidAlgebra.algHom_ext + multiplicativity. The final Bialgebra instance is assembled via Bialgebra.ofAlgHom.

Empty cut existence (substrate for counit laws)

The empty cut (0, T) is always a cut summand of T. The planar substrate cutSummandsP T always contains (0, T), by mutual structural induction with cutListSummandsP; the nonplanar cutForestSummandsN F contains (0, F) by descent. These witnesses split the (counit ⊗ id) sum into a single non-vanishing summand 1 ⊗ of' F.

Tree-depth induction substrate

theorem RootedTree.ConnesKreimer.Nonplanar.depth_lt_of_mem {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) (hT : T ∈ F) (a : α) : T.depth < (Nonplanar.node a F).depth

A tree's depth is strictly less than the depth of any node containing it as a child.

Counit ⊗ id commutation with lTensor (bPlusLin a)

The factor-wise commutation (counit ⊗ id) ∘ (id ⊗ B+_a) = (id ⊗ B+_a) ∘ (counit ⊗ id) (where the right id is on different domains: H on the left, R on the right). Pure TensorProduct.induction_on calculation; both sides reduce to counit x ⊗ B+_a y on simple tensors. Used in the tree-level counit law and in the bPlus closure proof.

Symmetric: id ⊗ counit commutation with lTensor (bPlusLin a)

Mirror of counit_rTensor_lTensor_bPlus_apply. Acting on the right factor with counit and on the left factor with B+_a — they don't interact.

Tree-level counit law (depth induction)

(counit ⊗ id)(Δ T) = 1 ⊗ T for every nonplanar tree T. Strong induction on T.depth: leaves close directly via comulTreeN_leaf; nodes use the cocycle comulTreeN_node_cocycle, the commutation counit_rTensor_lTensor_bPlus_apply, and the forest law on the children.

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

The "compute coassociativity left-hand side" algebra hom: x ↦ assoc((Δ ⊗ id)(Δ x)).

Equations

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

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

The "compute coassociativity right-hand side" algebra hom: x ↦ (id ⊗ Δ)(Δ x).

Equations

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

noncomputable def RootedTree.ConnesKreimer.coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} : Subalgebra R (ConnesKreimer R (Nonplanar α))

The Foissy coassociativity subalgebra: elements where the two sides of coassociativity agree. By Foissy's clean argument (coassocSubalg_eq_top), this is all of H.

Equations

• RootedTree.ConnesKreimer.coassocSubalg = AlgHom.equalizer RootedTree.ConnesKreimer.coassocLHS RootedTree.ConnesKreimer.coassocRHS

theorem RootedTree.ConnesKreimer.mem_coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (Nonplanar α)) : x ∈ coassocSubalg ↔ coassocLHS x = coassocRHS x

Linear extension of the cocycle

The cocycle comulAlgHomN_bPlusLin_cocycle is stated for of' F. Since both sides are R-linear in x : H, it extends to arbitrary x via Finsupp.lhom_ext (all linear maps out of H = R[Forest] are determined by their action on basis vectors of' F = Finsupp.single F 1).

theorem RootedTree.ConnesKreimer.comulAlgHomN_bPlusLin_cocycle_general {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (x : ConnesKreimer R (Nonplanar α)) : comulAlgHomN ((bPlusLin a) x) = (bPlusLin a) x ⊗ₜ[R] 1 + (LinearMap.lTensor (ConnesKreimer R (Nonplanar α)) (bPlusLin a)) (comulAlgHomN x)

The cocycle, extended to arbitrary x : H via linearity.

Closure of coassocSubalg under B+_a

The substantive Foissy bit. Uses the cocycle (twice) plus tensor-algebra calculations. Sketch (Sweedler-style, with Δ x = Σᵢ aᵢ ⊗ bᵢ):

• Δ(B+_a x) = (B+_a x) ⊗ 1 + Σᵢ aᵢ ⊗ B+_a bᵢ (cocycle).
• (Δ ⊗ id)(Δ(B+_a x)) = Δ(B+_a x) ⊗ 1 + Σᵢ Δ(aᵢ) ⊗ B+_a bᵢ. Re-apply cocycle to Δ(B+_a x) to expand the first summand.
• assoc((Δ ⊗ id)(Δ(B+_a x))) = (B+_a x) ⊗ (1 ⊗ 1) + Σᵢ aᵢ ⊗ (B+_a bᵢ ⊗ 1) + Σᵢ assoc(Δ(aᵢ) ⊗ B+_a bᵢ).
• (id ⊗ Δ)(Δ(B+_a x)) = (B+_a x) ⊗ (1 ⊗ 1) + Σᵢ aᵢ ⊗ (B+_a bᵢ ⊗ 1) + Σᵢ aᵢ ⊗ ((id ⊗ B+_a)(Δ bᵢ)).
• The "shared" first two summands match by inspection. The third summands match via (id ⊗ id ⊗ B+_a) applied to the hypothesis assoc((Δ ⊗ id)(Δ x)) = (id ⊗ Δ)(Δ x).

A clean Lean implementation would extract a LinearMap-level helper assoc_lTensor_bPlus_eq : assoc ∘ (Δ ⊗ id) ∘ (id ⊗ B+_a) = (id ⊗ id ⊗ B+_a) ∘ assoc ∘ (Δ ⊗ id) (provable by TensorProduct.induction_on), then close by congrArg ((id ⊗ id ⊗ B+_a)) on hx.

Helper commutations for the bPlus closure proof

Three commutation/identity lemmas for the substantive Foissy bit:

• comulAlgHomN_lTensor_bPlus_commute: (Δ ⊗ id) ∘ (id ⊗ B+) = (id ⊗ id ⊗ B+) ∘ (Δ ⊗ id), i.e., the comul on the left factor commutes with B+ on the right factor.
• assoc_lTensor_bPlus_commute: assoc ∘ (id ⊗ id_R ⊗ B+ on (H⊗H)⊗H) = (id ⊗ id ⊗ B+ on H⊗(H⊗H)) ∘ assoc, i.e., the associator commutes with B+ acting on the rightmost factor.
• lTensor_id_Δ_bPlus_eq: (id ⊗ Δ) ∘ (id ⊗ B+) z = assoc((id ⊗ B+)(z) ⊗ 1) + (id ⊗ id ⊗ B+) ∘ (id ⊗ Δ)(z), by cocycle on the right factor of (id ⊗ B+)(z).

theorem RootedTree.ConnesKreimer.bPlus_mem_coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (x : ConnesKreimer R (Nonplanar α)) (hx : x ∈ coassocSubalg) : (bPlusLin a) x ∈ coassocSubalg

Tree induction: every ofTree T is in coassocSubalg

theorem RootedTree.ConnesKreimer.ofTree_mem_coassocSubalg {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) : ofTree T ∈ coassocSubalg

Every Nonplanar tree's ofTree lies in coassocSubalg. By strong induction on tree depth: leaves are B+_a 1 (closed under B+_a from 1); nodes are B+_a (of' F) where of' F is a product of ofTree of smaller-depth trees.

coassocSubalg = ⊤

Since H is generated as an algebra by {ofTree T | T : Nonplanar α} and each generator is in coassocSubalg, the subalgebra is the whole thing.

theorem RootedTree.ConnesKreimer.coassocSubalg_eq_top {R : Type u_1} [CommSemiring R] {α : Type u_2} : coassocSubalg = ⊤

Coassociativity at the algebra-hom level

Direct corollary: coassocLHS = coassocRHS as algebra homs. The Bialgebra.ofAlgHom constructor takes this in its unfolded form (without going through the coassocLHS/coassocRHS named bundles), so we expose both.

theorem RootedTree.ConnesKreimer.coassocLHS_eq_coassocRHS {R : Type u_1} [CommSemiring R] {α : Type u_2} : coassocLHS = coassocRHS

theorem RootedTree.ConnesKreimer.comulAlgHomN_coassoc_algHom {R : Type u_1} [CommSemiring R] {α : Type u_2} : (↑(Algebra.TensorProduct.assoc R R R (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α)) (ConnesKreimer R (Nonplanar α)))).comp ((Algebra.TensorProduct.map comulAlgHomN (AlgHom.id R (ConnesKreimer R (Nonplanar α)))).comp comulAlgHomN) = (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (Nonplanar α))) comulAlgHomN).comp comulAlgHomN

Counit laws (algebra-hom level)

Strategy: reduce to of' F via AddMonoidAlgebra.algHom_ext. For each F, expand comulAlgHomN (of' F) = comulForestN F via comulForestN_eq_sum, then identify the unique cut summand (0, F) ∈ cutForestSummandsN F (the "all empty cuts" tuple). Other summands have pf.1.card > 0, so counit (of' pf.1) = 0 and (counit ⊗ id) kills them. The surviving (0, F) summand contributes 1 ⊗ of' F = (lid).symm (of' F).

Helper lemmas needed (substantive):

• mem_cutSummandsN_zero (T : Nonplanar α) : (0, T) ∈ cutSummandsN T — the empty cut exists at every tree.
• cutForestSummandsN_zero_mem (F : Forest (Nonplanar α)) : (0, F) ∈ cutForestSummandsN F.
• cutForestSummandsN_pos_pi : ∀ pf ∈ cutForestSummandsN F, pf ≠ (0, F) → pf.1.card > 0.

theorem RootedTree.ConnesKreimer.counit_rTensor_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : (Algebra.TensorProduct.map counit (AlgHom.id R (ConnesKreimer R (Nonplanar α)))).comp comulAlgHomN = ↑(Algebra.TensorProduct.lid R (ConnesKreimer R (Nonplanar α))).symm

theorem RootedTree.ConnesKreimer.counit_lTensor_comulAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (Nonplanar α))) counit).comp comulAlgHomN = ↑(Algebra.TensorProduct.rid R R (ConnesKreimer R (Nonplanar α))).symm

Bialgebra instance

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instBialgebraNonplanar {R : Type u_1} [CommSemiring R] {α : Type u_2} : Bialgebra R (ConnesKreimer R (Nonplanar α))

Equations

• RootedTree.ConnesKreimer.instBialgebraNonplanar = Bialgebra.ofAlgHom RootedTree.ConnesKreimer.comulAlgHomN RootedTree.ConnesKreimer.counit ⋯ ⋯ ⋯