The commutative Connes–Kreimer–Butcher Hopf algebra

The abelianization Hab k = H k / ⟨ab − ba⟩ of the planar Hopf algebra, built with Mathlib's RingQuot. Coproduct, counit and antipode descend through the projection π, so Hab k is the classical (commutative) Connes–Kreimer / Butcher Hopf algebra of rooted trees. Coassociativity is proved once on the planar algebra and transported.

Main results

• ConnesKreimer.Hab, ConnesKreimer.π, ConnesKreimer.π_mul_comm: the quotient and its commutative ring structure.
• ConnesKreimer.Δab, ConnesKreimer.εab, ConnesKreimer.Sab: the descended structure maps.
• ConnesKreimer.coassoc_Hab, ConnesKreimer.instHabCoalg, ConnesKreimer.instHabBialg.
• ConnesKreimer.instHabHopf: HopfAlgebra k (Hab k).

References

• A. Connes, D. Kreimer, Hopf algebras, renormalization and noncommutative geometry, Comm. Math. Phys. 199 (1998) 203–242.
• J. C. Butcher, An algebraic theory of integration methods, Math. Comp. 26 (1972) 79–106.
• C. Marín, How a Tree Forgets Its Order: the Eulerian idempotent and the Adams spectrum on the commutative Connes–Kreimer–Butcher Hopf algebra of rooted trees, machine-checked in Lean 4 (2026), doi:10.5281/zenodo.20774821. Ported from ConnesKreimer.lean of karlesmarin/connes-kreimer-lean (Lean v4.30.0-rc2).

The commutative quotient H_ab = H / ⟨ab − ba⟩

(Foissy's planar → commutative map).

Abelianizing the (forest) product turns the planar Hopf algebra into a commutative one. This is
the algebra step: the quotient ring `RingQuot` by the commutator relation, shown
commutative.
The coproduct, counit and antipode descend in the following sections, giving the classical
(commutative) Connes–Kreimer / Butcher Hopf algebra, where the Eulerian idempotents become
genuine orthogonal idempotents. 

inductive ConnesKreimer.commRel (k : Type u_1) [CommRing k] : H k → H k → Prop

The commutator relation x·y ∼ y·x on H.

• mul {k : Type u_1} [CommRing k] (x y : H k) : commRel k (x * y) (y * x)

@[reducible, inline]

abbrev ConnesKreimer.Hab (k : Type u_1) [CommRing k] : Type u_1

The commutative quotient H_ab = H / ⟨ab − ba⟩.

Equations

• ConnesKreimer.Hab k = RingQuot (ConnesKreimer.commRel k)

noncomputable def ConnesKreimer.π (k : Type u_1) [CommRing k] : H k →ₐ[k] Hab k

The quotient algebra map π : H → H_ab.

Equations

• ConnesKreimer.π k = RingQuot.mkAlgHom k (ConnesKreimer.commRel k)

@[instance_reducible]

noncomputable instance ConnesKreimer.instCommRingHab (k : Type u_1) [CommRing k] : CommRing (Hab k)

H_ab is commutative: the relation forces π(x)·π(y) = π(y)·x.

Equations

• ConnesKreimer.instCommRingHab k = { toRing := inferInstance, mul_comm := ⋯ }

theorem ConnesKreimer.π_surjective (k : Type u_1) [CommRing k] : Function.Surjective ⇑(π k)

theorem ConnesKreimer.π_mul_comm (k : Type u_1) [CommRing k] (x y : H k) : (π k) (x * y) = (π k) (y * x)

The coproduct descends to Delta_ab : H_ab → H_ab ⊗ H_ab.

noncomputable def ConnesKreimer.ΔAlg (k : Type u_1) [CommRing k] : H k →ₐ[k] TensorProduct k (H k) (H k)

Δ as an algebra homomorphism (the bialgebra coproduct), from Δ_one and Δ_mul.

Equations

• ConnesKreimer.ΔAlg k = AlgHom.ofLinearMap (ConnesKreimer.Δ k) ⋯ ⋯

theorem ConnesKreimer.ΔAlg_resp_commRel (k : Type u_1) [CommRing k] ⦃a b : H k⦄ (h : commRel k a b) : ((Algebra.TensorProduct.map (π k) (π k)).comp (ΔAlg k)) a = ((Algebra.TensorProduct.map (π k) (π k)).comp (ΔAlg k)) b

(π⊗π)∘Δ respects the commutator relation, since H_ab ⊗ H_ab is commutative.

noncomputable def ConnesKreimer.Δab (k : Type u_1) [CommRing k] : Hab k →ₐ[k] TensorProduct k (Hab k) (Hab k)

The descended coproduct Delta_ab : H_ab → H_ab ⊗ H_ab.

Equations

• ConnesKreimer.Δab k = (RingQuot.liftAlgHom k) ⟨(Algebra.TensorProduct.map (ConnesKreimer.π k) (ConnesKreimer.π k)).comp (ConnesKreimer.ΔAlg k), ⋯⟩

theorem ConnesKreimer.Δab_π (k : Type u_1) [CommRing k] (x : H k) : (Δab k) ((π k) x) = (Algebra.TensorProduct.map (π k) (π k)) ((ΔAlg k) x)

The descent square commutes: Delta_ab ∘ π = (π⊗π) ∘ Δ.

The counit descends to epsilon_ab : H_ab → k.

theorem ConnesKreimer.εalg_resp_commRel (k : Type u_1) [CommRing k] ⦃a b : H k⦄ (h : commRel k a b) : (εalg k) a = (εalg k) b

ε respects the commutator relation (k is commutative).

noncomputable def ConnesKreimer.εab (k : Type u_1) [CommRing k] : Hab k →ₐ[k] k

The descended counit epsilon_ab : H_ab → k.

Equations

• ConnesKreimer.εab k = (RingQuot.liftAlgHom k) ⟨ConnesKreimer.εalg k, ⋯⟩

theorem ConnesKreimer.εab_π (k : Type u_1) [CommRing k] (x : H k) : (εab k) ((π k) x) = (εalg k) x

H_ab is a coalgebra (coassoc + counit laws descend through π).

theorem ConnesKreimer.Hab_lhom_ext (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] {g₁ g₂ : Hab k →ₗ[k] M} (h : ∀ (x : H k), g₁ ((π k) x) = g₂ ((π k) x)) : g₁ = g₂

Extensionality on H_ab: a linear map out of H_ab is determined by its values on π.

theorem ConnesKreimer.εab_rTensor_natural (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (εab k).toLinearMap ∘ₗ (Algebra.TensorProduct.map (π k) (π k)).toLinearMap = TensorProduct.map (ε k) (π k).toLinearMap

ε (right) counit naturality: (epsilon_ab⊗id)∘(π⊗π) = ε⊗π.

theorem ConnesKreimer.εab_lTensor_natural (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (εab k).toLinearMap ∘ₗ (Algebra.TensorProduct.map (π k) (π k)).toLinearMap = TensorProduct.map (π k).toLinearMap (ε k)

ε (left) counit naturality: (id⊗epsilon_ab)∘(π⊗π) = π⊗ε.

theorem ConnesKreimer.rTensor_εab_comp_Δab (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (εab k).toLinearMap ∘ₗ (Δab k).toLinearMap = (TensorProduct.mk k k (Hab k)) 1

Left counitality on H_ab: (epsilon_ab ⊗ id) ∘ Delta_ab = 1 ⊗ ·.

theorem ConnesKreimer.lTensor_εab_comp_Δab (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (εab k).toLinearMap ∘ₗ (Δab k).toLinearMap = (TensorProduct.mk k (Hab k) k).flip 1

Right counitality on H_ab: (id ⊗ epsilon_ab) ∘ Delta_ab = · ⊗ 1.

theorem ConnesKreimer.Δab_π' (k : Type u_1) [CommRing k] (x : H k) : (Δab k) ((π k) x) = (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) ((Δ k) x)

Delta_ab ∘ π = (π⊗π) ∘ Δ in purely linear (TensorProduct.map) form.

theorem ConnesKreimer.Δab_tl_π (k : Type u_1) [CommRing k] (x : H k) : (Δab k).toLinearMap ((π k) x) = (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) ((Δ k) x)

Delta_ab ∘ π in .toLinearMap form (for use inside compositions).

theorem ConnesKreimer.Δab_rTensor_natural (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (Δab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) (π k).toLinearMap ∘ₗ LinearMap.rTensor (H k) (Δ k)

Coproduct (right) naturality for the descent: (Delta_ab⊗id)∘(π⊗π) = ((π⊗π)⊗π)∘(Δ⊗id).

theorem ConnesKreimer.Δab_lTensor_natural (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (Δab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (π k).toLinearMap (TensorProduct.map (π k).toLinearMap (π k).toLinearMap) ∘ₗ LinearMap.lTensor (H k) (Δ k)

Coproduct (left) naturality for the descent: (id⊗Delta_ab)∘(π⊗π) = (π⊗(π⊗π))∘(id⊗Δ).

theorem ConnesKreimer.coassoc_Hab (k : Type u_1) [CommRing k] : ↑(TensorProduct.assoc k (Hab k) (Hab k) (Hab k)) ∘ₗ LinearMap.rTensor (Hab k) (Δab k).toLinearMap ∘ₗ (Δab k).toLinearMap = LinearMap.lTensor (Hab k) (Δab k).toLinearMap ∘ₗ (Δab k).toLinearMap

Coassociativity on H_ab, descended from the planar coassociativity via π.

@[instance_reducible]

noncomputable instance ConnesKreimer.instCoalgebraStructHab (k : Type u_1) [CommRing k] : CoalgebraStruct k (Hab k)

H_ab is a coalgebra (the commutative Connes–Kreimer coalgebra).

Equations

• ConnesKreimer.instCoalgebraStructHab k = { comul := (ConnesKreimer.Δab k).toLinearMap, counit := (ConnesKreimer.εab k).toLinearMap }

@[instance_reducible]

noncomputable instance ConnesKreimer.instHabCoalg (k : Type u_1) [CommRing k] : Coalgebra k (Hab k)

Equations

• ConnesKreimer.instHabCoalg k = { toCoalgebraStruct := ConnesKreimer.instCoalgebraStructHab k, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

H_ab is a bialgebra.

`Δab`, `εab` are algebra homs by construction, so the four `Bialgebra.mk'`
compatibilities are just `map_one`/`map_mul` (cf. planar `instCKBialg`, which
needed a separate `Δ_mul` because there `Δ` was not yet packaged as an AlgHom). 

@[instance_reducible]

noncomputable instance ConnesKreimer.instHabBialg (k : Type u_1) [CommRing k] : Bialgebra k (Hab k)

Equations

• ConnesKreimer.instHabBialg k = Bialgebra.mk' k (ConnesKreimer.Hab k) ⋯ ⋯ ⋯ ⋯

The antipode descends to S_ab : H_ab → H_ab, giving HopfAlgebra k (H_ab).

S = antipode k is an algebra anti-homomorphism; composing with π into the COMMUTATIVE quotient H_ab turns it into a genuine algebra hom, so it lifts through RingQuot. The two antipode axioms then descend through π exactly like coassociativity in S4.

noncomputable def ConnesKreimer.SalgHom (k : Type u_1) [CommRing k] : H k →ₐ[k] Hab k

π ∘ S : H → H_ab as an algebra hom: on the commutative quotient the antipode anti-homomorphism becomes a homomorphism (π(S(ab)) = π(Sb·Sa) = π(Sa)·π(Sb)).

Equations

• ConnesKreimer.SalgHom k = AlgHom.ofLinearMap ((ConnesKreimer.π k).toLinearMap ∘ₗ ConnesKreimer.antipode k) ⋯ ⋯

theorem ConnesKreimer.SalgHom_resp_commRel (k : Type u_1) [CommRing k] ⦃a b : H k⦄ (h : commRel k a b) : (SalgHom k) a = (SalgHom k) b

π ∘ S respects the commutator relation (H_ab is commutative).

noncomputable def ConnesKreimer.Sab (k : Type u_1) [CommRing k] : Hab k →ₐ[k] Hab k

The descended antipode S_ab : H_ab → H_ab.

Equations

• ConnesKreimer.Sab k = (RingQuot.liftAlgHom k) ⟨ConnesKreimer.SalgHom k, ⋯⟩

theorem ConnesKreimer.Sab_π (k : Type u_1) [CommRing k] (x : H k) : (Sab k) ((π k) x) = (π k) ((antipode k) x)

The descent square: S_ab ∘ π = π ∘ S.

theorem ConnesKreimer.mul'_π (k : Type u_1) [CommRing k] : LinearMap.mul' k (Hab k) ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = (π k).toLinearMap ∘ₗ LinearMap.mul' k (H k)

mu_ab ∘ (π⊗π) = π ∘ μ (multiplication naturality, π an algebra hom).

theorem ConnesKreimer.Sab_rTensor_natural (k : Type u_1) [CommRing k] : LinearMap.rTensor (Hab k) (Sab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (π k).toLinearMap (π k).toLinearMap ∘ₗ LinearMap.rTensor (H k) (antipode k)

Antipode (left) naturality for the descent: (S_ab⊗id)∘(π⊗π) = (π⊗π)∘(S⊗id).

theorem ConnesKreimer.Sab_lTensor_natural (k : Type u_1) [CommRing k] : LinearMap.lTensor (Hab k) (Sab k).toLinearMap ∘ₗ TensorProduct.map (π k).toLinearMap (π k).toLinearMap = TensorProduct.map (π k).toLinearMap (π k).toLinearMap ∘ₗ LinearMap.lTensor (H k) (antipode k)

Antipode (right) naturality for the descent: (id⊗S_ab)∘(π⊗π) = (π⊗π)∘(id⊗S).

theorem ConnesKreimer.lTensor_antipode_eq (k : Type u_1) [CommRing k] : LinearMap.mul' k (H k) ∘ₗ LinearMap.lTensor (H k) (antipode k) ∘ₗ Δ k = Algebra.linearMap k (H k) ∘ₗ ε k

The (right-factor) left antipode identity, stated for antipode k rather than antipode' k (id ⋆ S = u∘ε re-expressed via antipode = antipode').

theorem ConnesKreimer.rTensor_Sab_Δab (k : Type u_1) [CommRing k] : LinearMap.mul' k (Hab k) ∘ₗ LinearMap.rTensor (Hab k) (Sab k).toLinearMap ∘ₗ (Δab k).toLinearMap = Algebra.linearMap k (Hab k) ∘ₗ (εab k).toLinearMap

Left antipode identity on H_ab, descended through π.

theorem ConnesKreimer.lTensor_Sab_Δab (k : Type u_1) [CommRing k] : LinearMap.mul' k (Hab k) ∘ₗ LinearMap.lTensor (Hab k) (Sab k).toLinearMap ∘ₗ (Δab k).toLinearMap = Algebra.linearMap k (Hab k) ∘ₗ (εab k).toLinearMap

Right antipode identity on H_ab, descended through π.

@[instance_reducible]

noncomputable instance ConnesKreimer.instHopfAlgebraStructHab (k : Type u_1) [CommRing k] : HopfAlgebraStruct k (Hab k)

Equations

• ConnesKreimer.instHopfAlgebraStructHab k = { toBialgebra := ConnesKreimer.instHabBialg k, antipode := (ConnesKreimer.Sab k).toLinearMap }

@[instance_reducible]

noncomputable instance ConnesKreimer.instHabHopf (k : Type u_1) [CommRing k] : HopfAlgebra k (Hab k)

H_ab is a Hopf algebra: the commutative Connes–Kreimer / Butcher Hopf algebra of rooted forests, obtained from the planar one by the abelianization quotient.

Equations

• ConnesKreimer.instHabHopf k = { toHopfAlgebraStruct := ConnesKreimer.instHopfAlgebraStructHab k, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }