The first Eulerian idempotent is idempotent on the commutative algebra

On the commutative Hopf algebra Hab k (over a ℚ-algebra k) the Adams operators are algebra morphisms with Ψᵖ ∘ Ψ^q = Ψ^{pq}, the image of the first Eulerian idempotent is an eigenvector, Ψⁱ ∘ e⁽¹⁾ = i · e⁽¹⁾, and a finite-difference identity collapses the convolution logarithm on eigenvectors. Hence e⁽¹⁾ ∘ e⁽¹⁾ = e⁽¹⁾ on Hab k; on the planar algebra this fails.

Main results

• ConnesKreimer.adamsAb_mul, ConnesKreimer.adamsAb_comp: Ψⁿ is an algebra morphism on Hab k, and Ψᵖ ∘ Ψ^q = Ψ^{pq}.
• ConnesKreimer.alternating_choose_weighted: Σᵢ (−1)^{j−i} C(j,i) · i = δ_{j,1}.
• ConnesKreimer.star_identity, ConnesKreimer.adamsAb_comp_JcAb_pow: the eigen-transport J_ab ↦ Yᵖ − 1 evaluated at the per-degree nilpotent J_ab.
• ConnesKreimer.adamsAb_eigen: Ψⁱ ∘ e⁽¹⁾ = i · e⁽¹⁾.
• ConnesKreimer.brickC: on an Adams eigenvector the truncated convolution logarithm is the identity.
• ConnesKreimer.eulerian1_idem_ab: π (e⁽¹⁾ (e⁽¹⁾ x)) = π (e⁽¹⁾ x).

The power-series input is PowerSeries.coeff_logTrunc_pow (Formalizations.RingTheory.PowerSeries.LogMul).

References

• F. Patras, L'algèbre des descentes d'une bigèbre graduée, J. Algebra 170 (1994) 547–566.
• J.-L. Loday, Opérations sur l'homologie cyclique des algèbres commutatives, Invent. Math. 96 (1989) 205–230.
• M. Aguiar, A. Lauve, The characteristic polynomial of the Adams operators on graded connected Hopf algebras, Algebra Number Theory 9 (2015) 547–583.
• 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).

Adams operators on H_ab

On the COMMUTATIVE H_ab the Eulerian idempotents e⁽ⁱ⁾ become orthogonal idempotents (Patras/Loday), so e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾ holds (unlike on the planar algebra). The principled route is via the Adams operators Ψⁿ: on a commutative Hopf algebra each Ψⁿ is an algebra morphism, whence Ψᵖ∘Ψq = Ψ^{pq}, whence the e⁽ⁱ⁾ are the orthogonal eigen-projectors.

First (no commutativity yet): the Adams operators on H_ab, and their naturality through π (Ψⁿ_ab ∘ π = π ∘ Ψⁿ), which both defines Ψⁿ_ab and ties it to the planar Ψⁿ.

noncomputable def ConnesKreimer.adamsAb (k : Type u_1) [CommRing k] (n : ℕ) : Hab k →ₗ[k] Hab k

The Adams operators Ψⁿ = id^{⋆n} on H_ab (convolution powers of the identity).

Equations

• ConnesKreimer.adamsAb k n = (WithConv.toConv LinearMap.id ^ n).ofConv

theorem ConnesKreimer.conv_apply_ab (k : Type u_1) [CommRing k] (F G : Hab k →ₗ[k] Hab k) (x : Hab k) : (WithConv.toConv F * WithConv.toConv G).ofConv x = (LinearMap.mul' k (Hab k)) ((TensorProduct.map F G) ((Δab k).toLinearMap x))

Element-level convolution on H_ab: (F⋆G)(x) = mu_ab((F⊗G)(Delta_ab x)).

theorem ConnesKreimer.adamsAb_succ_apply (k : Type u_1) [CommRing k] (n : ℕ) (x : Hab k) : (adamsAb k (n + 1)) x = (LinearMap.mul' k (Hab k)) ((TensorProduct.map LinearMap.id (adamsAb k n)) ((Δab k).toLinearMap x))

Ψⁿ⁺¹_ab = id ⋆ Ψⁿ_ab evaluated.

theorem ConnesKreimer.adamsAb_natural (k : Type u_1) [CommRing k] (n : ℕ) : adamsAb k n ∘ₗ (π k).toLinearMap = (π k).toLinearMap ∘ₗ adams k n

Adams naturality: Ψⁿ_ab ∘ π = π ∘ Ψⁿ. The planar Adams operators descend to H_ab through the bialgebra quotient map π.

Adams operators are algebra morphisms

Commutativity enters: each Adams operator `Ψⁿ` is an algebra morphism on the
commutative `H_ab`. We package `Ψⁿ` as an `AlgHom` built by composition:
`Ψⁿ⁺¹ = mu_ab∘(id⊗Ψⁿ)∘Delta_ab`. This is a composite of the algebra homs
`Delta_ab`, `id⊗Ψⁿ`, and `mu_ab`, and the multiplication is an algebra hom precisely
because `H_ab` is commutative. 

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

Ψⁿ packaged as an algebra hom on the commutative H_ab (Ψ₀ = u∘ε, Ψⁿ⁺¹ = mu_ab ∘ (id ⊗ Ψⁿ) ∘ Delta_ab).

Equations

• One or more equations did not get rendered due to their size.
• ConnesKreimer.adamsAbHom k 0 = (Algebra.ofId k (ConnesKreimer.Hab k)).comp (ConnesKreimer.εab k)

theorem ConnesKreimer.adamsAbHom_toLinearMap (k : Type u_1) [CommRing k] (n : ℕ) : (adamsAbHom k n).toLinearMap = adamsAb k n

The algebra-hom Ψⁿ and the convolution-power Ψⁿ agree as linear maps.

theorem ConnesKreimer.adamsAb_mul (k : Type u_1) [CommRing k] (n : ℕ) (a b : Hab k) : (adamsAb k n) (a * b) = (adamsAb k n) a * (adamsAb k n) b

Ψⁿ is an algebra morphism on H_ab: Ψⁿ(ab) = Ψⁿ(a)·Ψⁿ(b). The key commutative-Hopf fact behind the orthogonality of the Eulerian idempotents.

The Adams composition law

`Ψᵖ ∘ Ψq = Ψ^{pq}`. Post-composition by an algebra hom
distributes over convolution (`LinearMap.algHom_comp_convMul_distrib`), so an algebra-hom
`φ` post-composed with `Ψᵖ = id^{⋆p}` gives `(φ ∘ id)^{⋆p} = (toConv φ)^p`.
Taking `φ = Ψq` gives `Ψq ∘ Ψᵖ = (Ψq)^{⋆p} = id^{⋆qp} = Ψ^{qp}`. 

theorem ConnesKreimer.algHom_comp_adamsAb (k : Type u_1) [CommRing k] (φ : Hab k →ₐ[k] Hab k) (p : ℕ) : φ.toLinearMap ∘ₗ adamsAb k p = (WithConv.toConv φ.toLinearMap ^ p).ofConv

An algebra hom φ post-composed with the Adams operator Ψᵖ is the p-th convolution power of φ itself: φ ∘ Ψᵖ = (toConv φ)^p in WithConv.

theorem ConnesKreimer.adamsAb_comp (k : Type u_1) [CommRing k] (p q : ℕ) : adamsAb k p ∘ₗ adamsAb k q = adamsAb k (p * q)

The Adams composition law Ψᵖ ∘ Ψq = Ψ^{pq} on the commutative H_ab. The Adams (Hopf-power) operators form a commuting family of algebra endomorphisms realising the multiplicative monoid (ℕ, ·); this is the structural reason the Eulerian idempotents are orthogonal.

Toward e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾ on the commutative H_ab: the finite-difference engine

The route avoids the full Eulerian decomposition / Vandermonde inversion. The point:
if `v` is an Adams eigenvector with `Ψⁱ(v) = i·v` for all `i`, then expanding
`J^{⋆j} = (id − u∘ε)^{⋆j}` into Adams operators and applying to `v` collapses
each `J^{⋆j}(v)` to a scalar multiple of `v` by the finite-difference identity below.
Hence `e⁽¹⁾` is the identity on its own image. 

theorem ConnesKreimer.alternating_choose_weighted (j : ℕ) : ∑ i ∈ Finset.range (j + 1), (-1) ^ (j - i) * ↑(j.choose i) * ↑i = if j = 1 then 1 else 0

Finite-difference engine: the j-th finite difference of the identity sequence i ↦ i, ∑ᵢ (-1)^{j-i} C(j,i)·i = δ_{j,1}. This collapses the convolution-log of an Adams eigenvector to its weight-1 component, which is the combinatorial heart of the Eulerian idempotency on H_ab.

Binomial expansion of J_ab^{⋆j} into Adams operators on the commutative H_ab

Toward `e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾`: expand the convolution-log's `J^{⋆j}` into the Adams
basis so that, on an Adams eigenvector, `alternating_choose_weighted` collapses it. 

theorem ConnesKreimer.JcAb_pow_ofConv_eq_adams_sum (k : Type u_1) [CommRing k] (j : ℕ) (x : Hab k) : ((WithConv.toConv LinearMap.id - 1) ^ j).ofConv x = ∑ i ∈ Finset.range (j + 1), ((-1) ^ (j - i) * ↑(j.choose i)) • (adamsAb k i) x

J^{⋆j} naturality through π and per-degree nilpotency on H_ab

theorem ConnesKreimer.Jc_pow_ofConv_eq_adams_sum (k : Type u_1) [CommRing k] (j : ℕ) (z : H k) : (Jc k ^ j).ofConv z = ∑ i ∈ Finset.range (j + 1), ((-1) ^ (j - i) * ↑(j.choose i)) • (adams k i) z

theorem ConnesKreimer.Jc_pow_ofConv_natural (k : Type u_1) [CommRing k] (j : ℕ) (z : H k) : (π k) ((Jc k ^ j).ofConv z) = ((WithConv.toConv LinearMap.id - 1) ^ j).ofConv ((π k) z)

theorem ConnesKreimer.JcAb_pow_ofConv_sf_eq_zero (k : Type u_1) [CommRing k] (n : ℕ) (f : Forest) (h : sizeF f < n) : ((WithConv.toConv LinearMap.id - 1) ^ n).ofConv ((π k) (sf k f)) = 0

The ring-hom step: post-composition by Ψᵖ (adamsAb p, an

algebra hom) is a ⋆-ring hom, sending J_ab ↦ Yᵖ − 1 (Y = toConv id_ab). This is Ψᵖ ∘ e = log(Yᵖ).

theorem ConnesKreimer.algHom_comp_convPow (k : Type u_1) [CommRing k] (φ : Hab k →ₐ[k] Hab k) (g : WithConv (Hab k →ₗ[k] Hab k)) (j : ℕ) : φ.toLinearMap ∘ₗ (g ^ j).ofConv = (WithConv.toConv (φ.toLinearMap ∘ₗ g.ofConv) ^ j).ofConv

theorem ConnesKreimer.adamsAb_comp_JcAb_pow (k : Type u_1) [CommRing k] (p j : ℕ) (y : Hab k) : (adamsAb k p) (((WithConv.toConv LinearMap.id - 1) ^ j).ofConv y) = ((WithConv.toConv LinearMap.id ^ p - 1) ^ j).ofConv y

Evaluation: bridge the power-series coefficient identity (coeff_logTrunc_pow)

to the convolution sums via `eval₂ (X ↦ J_ab)`, then kill high powers with nilpotency. 

noncomputable def ConnesKreimer.JcAb (k : Type u_1) [CommRing k] : WithConv (Hab k →ₗ[k] Hab k)

J_ab = id − u∘ε on H_ab, as a convolution-ring element.

Equations

• ConnesKreimer.JcAb k = WithConv.toConv LinearMap.id - 1

noncomputable def ConnesKreimer.smulOne (k : Type u_1) [CommRing k] : k →+* WithConv (Hab k →ₗ[k] Hab k)

r ↦ r • 1 as a ring hom k →+* WithConv(H_ab) (image central; convCommRing).

Equations

• ConnesKreimer.smulOne k = { toFun := fun (r : k) => r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem ConnesKreimer.eulerCoef_eq_coeff_log (k : Type u_1) [CommRing k] [Algebra ℚ k] (j : ℕ) : eulerCoef k j = (PowerSeries.coeff j) (PowerSeries.log k)

The Eulerian coefficient (-1)^{j+1}/j equals the j-th coefficient of the formal log.

theorem ConnesKreimer.eval₂_ofConv (k : Type u_1) [CommRing k] (P : Polynomial k) (w : Hab k) : (Polynomial.eval₂ (smulOne k) (JcAb k) P).ofConv w = ∑ m ∈ Finset.range (P.natDegree + 1), P.coeff m • (JcAb k ^ m).ofConv w

eval₂ smulOne J_ab P, applied through .ofConv to w, is the explicit sum Σₘ (P.coeff m) • (J_ab^m).ofConv w.

theorem ConnesKreimer.PR_coeff (k : Type u_1) [CommRing k] [Algebra ℚ k] (N m : ℕ) (hm : m ≤ N) : (∑ j ∈ Finset.range (N + 1), Polynomial.C ((PowerSeries.coeff j) (PowerSeries.log k)) * Polynomial.X ^ j).coeff m = (PowerSeries.coeff m) (PowerSeries.log k)

The truncated ∑ⱼ cⱼ X^j polynomial has coeff m = cₘ for m ≤ N.

theorem ConnesKreimer.star_identity (k : Type u_1) [CommRing k] [Algebra ℚ k] (p N : ℕ) (w : Hab k) (hnil : ∀ (m : ℕ), N < m → (JcAb k ^ m).ofConv w = 0) : ∑ j ∈ Finset.range (N + 1), (PowerSeries.coeff j) (PowerSeries.log k) • ((WithConv.toConv LinearMap.id ^ p - 1) ^ j).ofConv w = ↑p • ∑ j ∈ Finset.range (N + 1), (PowerSeries.coeff j) (PowerSeries.log k) • (JcAb k ^ j).ofConv w

(★) — the eigen-transport identity on a per-degree-nilpotent w: applying Ψᵖ to the truncated convolution-log scales it by p. Proven by evaluating the polynomial coeff_logTrunc_pow identity at J_ab (eval₂), killing the surplus J_ab^{>N} by nilpotency.

theorem ConnesKreimer.pi_eulerian1_eq (k : Type u_1) [CommRing k] [Algebra ℚ k] (y : H k) (M : ℕ) (hMy : ∀ a ∈ y.coeff.support, sizeF a ≤ M) : (π k) ((eulerian1 k) y) = ∑ j ∈ Finset.range (M + 1), (PowerSeries.coeff j) (PowerSeries.log k) • (JcAb k ^ j).ofConv ((π k) y)

π(e⁽¹⁾ y) as a truncated convolution-log sum on H_ab, for any degree bound M ≥ deg(y).

theorem ConnesKreimer.adamsAb_eigen_basis (k : Type u_1) [CommRing k] [Algebra ℚ k] (p : ℕ) (f : Forest) : (adamsAb k p) ((π k) ((eulerian1 k) (sf k f))) = ↑p • (π k) ((eulerian1 k) (sf k f))

Adams eigen-relation on a basis forest: Ψᵖ(π(e⁽¹⁾(sf f))) = p · π(e⁽¹⁾(sf f)).

theorem ConnesKreimer.adamsAb_eigen (k : Type u_1) [CommRing k] [Algebra ℚ k] (p : ℕ) (x : H k) : (adamsAb k p) ((π k) ((eulerian1 k) x)) = ↑p • (π k) ((eulerian1 k) x)

Adams eigen-relation (general): Ψᵖ(π(e⁽¹⁾ x)) = p · π(e⁽¹⁾ x) for all x.

The finite-difference collapse: on an Adams eigenvector the convolution-log

truncation collapses to the eigenvector itself (only the weight-1 term survives).

theorem ConnesKreimer.brickC (k : Type u_1) [CommRing k] [Algebra ℚ k] (v : Hab k) (M : ℕ) (hM : 1 ≤ M) (heig : ∀ (i : ℕ), (adamsAb k i) v = ↑i • v) : ∑ j ∈ Finset.range (M + 1), (PowerSeries.coeff j) (PowerSeries.log k) • (JcAb k ^ j).ofConv v = v

Collapse. On an Adams eigenvector v (Ψⁱ(v) = i·v), the truncated convolution-log is the identity: Σⱼ≤M cⱼ · J_ab^{⋆j}(v) = v (M ≥ 1). The J_ab^{⋆j} expands into Adams ops, the eigen-relation turns each into a scalar, and alternating_choose_weighted kills all but j = 1.

theorem ConnesKreimer.eulerian1_idem_ab (k : Type u_1) [CommRing k] [Algebra ℚ k] (x : H k) : (π k) ((eulerian1 k) ((eulerian1 k) x)) = (π k) ((eulerian1 k) x)

e⁽¹⁾ ∘ e⁽¹⁾ = e⁽¹⁾ on the commutative H_ab (the Eulerian idempotency, via π). The first Eulerian idempotent is genuinely idempotent on the abelianized Connes–Kreimer / Butcher Hopf algebra. Combines pi_eulerian1_eq, the Adams eigen-relation adamsAb_eigen, and the collapse brickC.