The admissible-cut coproduct on planar rooted trees

Planar rooted trees (RTree.node : List RTree → RTree, so B₊ = node), forests (List RTree), and the Connes–Kreimer / Foissy coproduct by admissible cuts, defined through the B₊ cocycle Δ(B₊ F) = B₊ F ⊗ 𝟙 + (id ⊗ B₊)(Δ F) on formal sums List (Forest × Forest). Coassociativity holds up to List.Perm (equality of formal sums).

Main results

• ConnesKreimer.coprodTree, ConnesKreimer.coprodForest: the coproduct on trees and forests.
• ConnesKreimer.tmul_assoc: the leg-wise forest product on formal tensors is associative.
• ConnesKreimer.coprodForest_append: Δ is multiplicative (combinatorially).
• ConnesKreimer.coprod_coassoc: (Δ ⊗ id) Δ t and (id ⊗ Δ) Δ t agree up to permutation.

Implementation notes

Mathlib's RootedTree (Mathlib.Order.SuccPred.Tree) is a rooted tree given by its ancestorship order on a carrier type. It is not used here: the Hopf algebra needs a type whose elements are the (isomorphism classes of) finite planar trees, to serve as a basis, and an inductive type gives that with decidable, computable cuts. Trees are planar (ordered children); the commutative algebra is the quotient of Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Abelianization.

References

• A. Connes, D. Kreimer, Hopf algebras, renormalization and noncommutative geometry, Comm. Math. Phys. 199 (1998) 203–242.
• L. Foissy, Les algèbres de Hopf des arbres enracinés décorés, I, Bull. Sci. Math. 126 (2002) 193–239.
• C. Marín, How a Tree Remembers Its Cuts: the Connes–Kreimer–Foissy Hopf Algebra of Rooted Trees, Machine-Checked in Lean 4 (2026), doi:10.5281/zenodo.20762280. Ported from ConnesKreimer.lean of karlesmarin/connes-kreimer-lean (Lean v4.30.0-rc2).

inductive ConnesKreimer.RTree : Type

Planar rooted trees, represented by the forest of children below the root.

• node : List RTree → RTree

@[instance_reducible]

instance ConnesKreimer.instReprRTree : Repr RTree

Equations

• ConnesKreimer.instReprRTree = { reprPrec := ConnesKreimer.instReprRTree.repr }

partial def ConnesKreimer.instReprRTree.repr : RTree → ℕ → Std.Format

@[instance_reducible]

instance ConnesKreimer.instInhabitedRTree : Inhabited RTree

Equations

• ConnesKreimer.instInhabitedRTree = { default := ConnesKreimer.instInhabitedRTree.default }

@[reducible, inline]

abbrev ConnesKreimer.Forest : Type

A planar rooted forest is a list of planar rooted trees.

Equations

• ConnesKreimer.Forest = List ConnesKreimer.RTree

@[reducible, inline]

abbrev ConnesKreimer.Tens : Type

Formal sums of coproduct tensor monomials, represented by their forest pairs.

Equations

• ConnesKreimer.Tens = List (ConnesKreimer.Forest × ConnesKreimer.Forest)

def ConnesKreimer.tmul (x y : Tens) : Tens

Product on formal tensor monomials, multiplying the two tensor legs by forest concatenation.

Equations

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

def ConnesKreimer.coprodTree : RTree → Tens

The Connes-Kreimer coproduct on one rooted tree, as a formal list of tensor terms.

Equations

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

def ConnesKreimer.coprodForest : Forest → Tens

The multiplicative extension of the coproduct from trees to forests.

Equations

• ConnesKreimer.coprodForest [] = [([], [])]
• ConnesKreimer.coprodForest (t :: ts) = ConnesKreimer.tmul (ConnesKreimer.coprodTree t) (ConnesKreimer.coprodForest ts)

@[simp]

theorem ConnesKreimer.tmul_unit_left (y : Tens) : tmul [([], [])] y = y

@[simp]

theorem ConnesKreimer.tmul_unit_right (x : Tens) : tmul x [([], [])] = x

theorem ConnesKreimer.tmul_append_left (x₁ x₂ y : Tens) : tmul (x₁ ++ x₂) y = tmul x₁ y ++ tmul x₂ y

theorem ConnesKreimer.tmul_cons (p r : Forest) (xs y : Tens) : tmul ((p, r) :: xs) y = List.map (fun (x : Forest × Forest) => match x with | (p', r') => (p ++ p', r ++ r')) y ++ tmul xs y

theorem ConnesKreimer.tmul_assoc (x y z : Tens) : tmul (tmul x y) z = tmul x (tmul y z)

theorem ConnesKreimer.coprodForest_append (F G : Forest) : coprodForest (F ++ G) = tmul (coprodForest F) (coprodForest G)

theorem ConnesKreimer.perm_middle_swap {α : Type u_1} (A B C D : List α) : (A ++ B ++ (C ++ D)).Perm (A ++ C ++ (B ++ D))

theorem ConnesKreimer.flatMap_append_distrib {α : Type u_1} {β : Type u_2} (l : List α) (X Y : α → List β) : (List.flatMap (fun (a : α) => X a ++ Y a) l).Perm (List.flatMap X l ++ List.flatMap Y l)

theorem ConnesKreimer.flatMap_const_nil {α : Type u_1} {β : Type u_2} (l : List α) : List.flatMap (fun (x : α) => []) l = []

theorem ConnesKreimer.flatMap_singleton_eq_map {α : Type u_1} {β : Type u_2} (g : α → β) (l : List α) : List.flatMap (fun (a : α) => [g a]) l = List.map g l

theorem ConnesKreimer.flatMap_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l1 : List α) (l2 : List β) (f : α → β → List γ) : (List.flatMap (fun (a : α) => List.flatMap (fun (b : β) => f a b) l2) l1).Perm (List.flatMap (fun (b : β) => List.flatMap (fun (a : α) => f a b) l1) l2)

theorem ConnesKreimer.Perm.flatMap_congr_right {α : Type u_1} {β : Type u_2} (l : List α) {f g : α → List β} (h : ∀ (a : α), (f a).Perm (g a)) : (List.flatMap f l).Perm (List.flatMap g l)

@[reducible, inline]

abbrev ConnesKreimer.Tens3 : Type

Formal sums of triple tensor monomials, represented by forest triples.

Equations

• ConnesKreimer.Tens3 = List (ConnesKreimer.Forest × ConnesKreimer.Forest × ConnesKreimer.Forest)

def ConnesKreimer.coLeft (x : Tens) : Tens3

Expand the left tensor leg of every coproduct term.

Equations

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

def ConnesKreimer.coRight (x : Tens) : Tens3

Expand the right tensor leg of every coproduct term.

Equations

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

def ConnesKreimer.tmul3 (x y : Tens3) : Tens3

Product on formal triple tensor monomials, multiplying all three tensor legs.

Equations

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

theorem ConnesKreimer.coLeft_tmul (x y : Tens) : List.Perm (coLeft (tmul x y)) (tmul3 (coLeft x) (coLeft y))

theorem ConnesKreimer.coRight_tmul (x y : Tens) : List.Perm (coRight (tmul x y)) (tmul3 (coRight x) (coRight y))

theorem ConnesKreimer.coprodTree_node (F : Forest) : coprodTree (RTree.node F) = ([RTree.node F], []) :: List.map (fun (pr : Forest × Forest) => (pr.fst, [RTree.node pr.snd])) (coprodForest F)

theorem ConnesKreimer.coprodForest_single (t : RTree) : coprodForest [t] = coprodTree t

theorem ConnesKreimer.tmul3_perm {a a' b b' : Tens3} (ha : List.Perm a a') (hb : List.Perm b b') : List.Perm (tmul3 a b) (tmul3 a' b')

theorem ConnesKreimer.coassocTree (t : RTree) : List.Perm (coLeft (coprodTree t)) (coRight (coprodTree t))

theorem ConnesKreimer.coassocForest (F : Forest) : List.Perm (coLeft (coprodForest F)) (coRight (coprodForest F))

theorem ConnesKreimer.coprod_coassoc (t : RTree) : List.Perm (coLeft (coprodTree t)) (coRight (coprodTree t))

Coassociativity of the Connes–Kreimer / Foissy (planar) coproduct on rooted trees: (Δ⊗id)∘Δ and (id⊗Δ)∘Δ agree as formal sums (multiset equality / List.Perm). Proved by mutual induction tree ↔ forest via the B₊ Hochschild 1-cocycle, on top of multiplicativity and a Fubini swap.

Examples: Δ(•) = •⊗1 + 1⊗•, Δ(ℓ₂) has three terms, and

`Δ(cherry) = cherry⊗1 + 2 •⊗ℓ₂ + ••⊗• + 1⊗cherry` five.