Connes-Kreimer Hopf algebra carrier on n-ary planar rooted trees

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

The Connes-Kreimer Hopf algebra on a tree type T is the formal R-linear combinations of forests (multisets of trees), with product = forest disjoint union and coproduct = sum over admissible cuts (defined in CoproductDeletion.lean for Δ^ρ, CoproductTrace.lean for Δ^c).

This file provides the carrier and counit generic over a tree type T (parameterized over Type u). The intended specializations:

• T = RootedTree.Planar α — n-ary planar rooted trees (this file).
• T = RootedTree.Nonplanar α — n-ary nonplanar (future Phase A.4).
• T = subtype of Planar — binary, at-most-n-ary, exactly-n-ary (subtypes from Subtypes.lean).

The product structure (algebra) doesn't depend on which T is used — forests are multisets, multiset addition is commutative (Hopf algebra is commutative). The coproduct depends on the cut substrate of T; see sibling files for specific instantiations.

Layer status

[UPSTREAM] candidate. No sorries.

MCB anchor

@cite{marcolli-chomsky-berwick-2025} §1.2 "Workspaces: Product and Coproduct" introduces the Hopf algebra of workspaces; the carrier is V(𝔉_{SO_0}) = AddMonoidAlgebra R (Multiset (FCM α)). This file generalizes the carrier to arbitrary tree type T, with binary FCM as one specialization (eventual Phase B target).

@cite{foissy-introduction-hopf-algebras-trees} §1.2: "The Hopf algebra H_R is the free associative commutative unitary K-algebra generated by T", where T is the set of rooted trees. Same structure here, with T parameterized.

Naming

Type: RootedTree.ConnesKreimer R T with eponymous namespace RootedTree.ConnesKreimer. Eponymous-type-and-namespace pattern matches mathlib idiom (Polynomial, WittVector, PowerSeries, etc.) — no abbreviation. The legacy open ConnesKreimer statements in soon-to-be- rebuilt consumer files (Adger2025, Merge/*, etc.) referred to the now- deleted top-level ConnesKreimer.{TraceTree, Hc, ...} and won't compile against the new substrate anyway, so the silent re-binding hazard is moot — those files need full Phase D rewrites.

The eventual upstream-mathlib home would be Mathlib.RingTheory.HopfAlgebra.RootedTree.ConnesKreimer or similar.

§1: Forest type alias

A forest is a multiset of trees. Multiset addition is the disjoint union (forest concatenation).

@[reducible, inline]

abbrev RootedTree.Forest (T : Type u_1) : Type u_1

A forest of T-shaped trees: finite multiset.

Equations

• RootedTree.Forest T = Multiset T

§2: The Connes-Kreimer Hopf algebra carrier

def RootedTree.ConnesKreimer (R : Type u_1) [CommSemiring R] (T : Type u_2) : Type (max u_2 u_1)

The Connes-Kreimer Hopf algebra on tree type T: AddMonoidAlgebra R (Forest T). As an algebra: product = forest disjoint union (commutative), unit = empty forest. The Bialgebra structure (coproduct + coassoc + counit laws) is in sibling files.

Equations

• RootedTree.ConnesKreimer R T = AddMonoidAlgebra R (RootedTree.Forest T)

§3: Forwarded mathlib instances

ConnesKreimer R T is a def, not abbrev, isolating its eventual Bialgebra structure from mathlib's default AddMonoidAlgebra.instBialgebra (group-like coproduct). Forward CommSemiring, Algebra, and FunLike explicitly.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instCommSemiring {R : Type u_1} [CommSemiring R] {T : Type u_2} : CommSemiring (ConnesKreimer R T)

Equations

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

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instAlgebra {R : Type u_1} [CommSemiring R] {T : Type u_2} : Algebra R (ConnesKreimer R T)

Equations

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

@[implicit_reducible]

instance RootedTree.ConnesKreimer.instFunLike {R : Type u_1} [CommSemiring R] {T : Type u_2} : FunLike (ConnesKreimer R T) (Forest T) R

Equations

• RootedTree.ConnesKreimer.instFunLike = { coe := RootedTree.ConnesKreimer.instFunLike._aux_1, coe_injective' := ⋯ }

§4: Basis embeddings — of', ofTree

The natural inclusions of basis elements (forests, single trees) into the algebra. Mirrors mathlib's MonoidAlgebra.of' (bare function form) and MonoidAlgebra.of (MonoidHom form).

noncomputable def RootedTree.ConnesKreimer.of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : ConnesKreimer R T

Bare embedding: a forest as the basis vector Finsupp.single F 1.

Equations

• RootedTree.ConnesKreimer.of' F = Finsupp.single F 1

noncomputable def RootedTree.ConnesKreimer.of {R : Type u_1} [CommSemiring R] {T : Type u_2} : Multiplicative (Forest T) →* ConnesKreimer R T

MonoidHom embedding: Multiplicative (Forest T) →* ConnesKreimer R T.

Equations

• RootedTree.ConnesKreimer.of = { toFun := fun (F : Multiplicative (RootedTree.Forest T)) => RootedTree.ConnesKreimer.of' (Multiplicative.toAdd F), map_one' := ⋯, map_mul' := ⋯ }

noncomputable def RootedTree.ConnesKreimer.ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) : ConnesKreimer R T

Embed a single tree as a singleton-forest basis vector.

Equations

• RootedTree.ConnesKreimer.ofTree t = RootedTree.ConnesKreimer.of' {t}

theorem RootedTree.ConnesKreimer.of_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Multiplicative (Forest T)) : of F = of' (Multiplicative.toAdd F)

theorem RootedTree.ConnesKreimer.of'_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : of' F = Finsupp.single F 1

@[simp]

theorem RootedTree.ConnesKreimer.of'_zero {R : Type u_1} [CommSemiring R] {T : Type u_2} : of' 0 = 1

@[simp]

theorem RootedTree.ConnesKreimer.of'_add {R : Type u_1} [CommSemiring R] {T : Type u_2} (F G : Forest T) : of' (F + G) = of' F * of' G

Headline algebraic fact: forest disjoint union ↔ algebra product.

@[simp]

theorem RootedTree.ConnesKreimer.of'_singleton {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) : of' {t} = ofTree t

§5: Counit

The counit ε : ConnesKreimer R T → R extracts the coefficient of the empty forest, packaged as an algebra hom.

noncomputable def RootedTree.ConnesKreimer.counitMonoidHom {R : Type u_1} [CommSemiring R] {T : Type u_2} : Multiplicative (Forest T) →* R

The counit as a Multiplicative (Forest T) →* R monoid hom.

Uses Multiset.card_eq_zero to avoid requiring DecidableEq T: test "is empty" via "has cardinality zero" (card is Nat, decidable).

Equations

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

noncomputable def RootedTree.ConnesKreimer.counit {R : Type u_1} [CommSemiring R] {T : Type u_2} : ConnesKreimer R T →ₐ[R] R

The counit on ConnesKreimer R T as an algebra hom.

Equations

• RootedTree.ConnesKreimer.counit = (AddMonoidAlgebra.lift R R (RootedTree.Forest T)) RootedTree.ConnesKreimer.counitMonoidHom

@[simp]

theorem RootedTree.ConnesKreimer.counit_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : counit (of' F) = if Multiset.card F = 0 then 1 else 0

counit (of' F) = if F.card = 0 then 1 else 0. The card formulation avoids needing DecidableEq T.

@[simp]

theorem RootedTree.ConnesKreimer.counit_one {R : Type u_1} [CommSemiring R] {T : Type u_2} : counit 1 = 1

@[simp]

theorem RootedTree.ConnesKreimer.counit_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) : counit (ofTree t) = 0