Adams operators and the first Eulerian idempotent on the planar algebra

In the convolution ring WithConv (H k →ₗ[k] H k) the identity is a unit with inverse the antipode; its convolution powers are the Adams operators Ψₙ = id^{⋆n}. The augmentation J = id − u∘ε is locally nilpotent, so over a ℚ-algebra the convolution logarithm e⁽¹⁾ = log_⋆ id is a finite sum on each forest.

Main results

• ConnesKreimer.adams, ConnesKreimer.toConv_adams_add, ConnesKreimer.adamsUnit, ConnesKreimer.adamsUnit_inv_val: Adams operators, Ψₘ ⋆ Ψₙ = Ψₘ₊ₙ, and Ψ₋₁ = S.
• ConnesKreimer.Jc_pow_ofConv_sf_eq_zero: J^{⋆n} vanishes on forests with fewer than n nodes.
• ConnesKreimer.adams_primitive: Ψₙ x = n • x for a primitive x.
• ConnesKreimer.eulerian1, ConnesKreimer.eulerian1_eq_logTrunc: the first Eulerian idempotent and its truncation formula.
• ConnesKreimer.eulerian1_primitive: e⁽¹⁾ fixes every primitive element.
• ConnesKreimer.eulerian1_idem_dot: e⁽¹⁾ (e⁽¹⁾ •) = e⁽¹⁾ • on the one-node tree.

References

• M. Aguiar, A. Lauve, The characteristic polynomial of the Adams operators on graded connected Hopf algebras, Algebra Number Theory 9 (2015) 547–583.
• J.-L. Loday, Opérations sur l'homologie cyclique des algèbres commutatives, Invent. Math. 96 (1989) 205–230.
• 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 Ψₙ = id^{⋆n} and the antipode as Ψ₋₁.

The convolution ring `WithConv (H k →ₗ[k] H k)` (Mathlib `LinearMap.convRing`) turns the
identity into a ring element whose convolution powers are the Adams (Hopf-power) operators.
`Ψ₀ = u∘ε` (the convolution unit), `Ψ₁ = id`, the semigroup law `Ψₘ ⋆ Ψₙ = Ψₘ₊ₙ`, and the
identity is a convolution unit whose inverse is the antipode — i.e. `Ψ₋₁ = S`
(Aguiar–Lauve theory; the Eulerian idempotent `e⁽¹⁾ = log_⋆ id` is the next step, needing
connected-graded nilpotence). 

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

The n-th Adams operator Ψₙ = id^{⋆n}: the n-th convolution power of the identity in the convolution ring WithConv (H k →ₗ[k] H k).

Equations

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

theorem ConnesKreimer.toConv_adams (k : Type u_1) [CommRing k] (n : ℕ) : WithConv.toConv (adams k n) = WithConv.toConv LinearMap.id ^ n

@[simp]

theorem ConnesKreimer.toConv_adams_zero (k : Type u_1) [CommRing k] : WithConv.toConv (adams k 0) = 1

Ψ₀ = u∘ε is the convolution unit.

@[simp]

theorem ConnesKreimer.adams_one (k : Type u_1) [CommRing k] : adams k 1 = LinearMap.id

Ψ₁ = id.

theorem ConnesKreimer.toConv_adams_add (k : Type u_1) [CommRing k] (m n : ℕ) : WithConv.toConv (adams k (m + n)) = WithConv.toConv (adams k m) * WithConv.toConv (adams k n)

The convolution-power semigroup law Ψₘ ⋆ Ψₙ = Ψₘ₊ₙ.

theorem ConnesKreimer.antipode_convMul_id (k : Type u_1) [CommRing k] : WithConv.toConv (antipode k) * WithConv.toConv LinearMap.id = 1

S ⋆ id = u∘ε: the antipode is a left convolution inverse of Ψ₁ = id.

theorem ConnesKreimer.id_convMul_antipode (k : Type u_1) [CommRing k] : WithConv.toConv LinearMap.id * WithConv.toConv (antipode k) = 1

id ⋆ S = u∘ε: the antipode is also a right convolution inverse of Ψ₁ = id.

noncomputable def ConnesKreimer.adamsUnit (k : Type u_1) [CommRing k] : (WithConv (H k →ₗ[k] H k))ˣ

Ψ₁ = id is a convolution UNIT, with the antipode as its (two-sided) inverse. This is the precise sense in which Ψ₋₁ = S.

Equations

• ConnesKreimer.adamsUnit k = { val := WithConv.toConv LinearMap.id, inv := WithConv.toConv (ConnesKreimer.antipode k), val_inv := ⋯, inv_val := ⋯ }

theorem ConnesKreimer.adamsUnit_inv_val (k : Type u_1) [CommRing k] : ↑(adamsUnit k)⁻¹ = WithConv.toConv (antipode k)

Ψ₋₁ = S: the inverse of the Adams unit Ψ₁ is the antipode.

Local nilpotency of J = id − u∘ε (the connected-graded engine for log_⋆).

`J` kills the empty forest and is the identity on nonempty ones. Its convolution powers
`J^{⋆k}` vanish on every basis forest of fewer than `k` nodes (`Jc_pow_ofConv_sf_eq_zero`):
each of the `k` convolution factors must absorb at least one node, so `k` nodes are needed.
Hence the series `log_⋆(id) = Σ_{k≥1} ((-1)^{k+1}/k)·J^{⋆k}` is finite in each degree — the
connected-graded local nilpotency on which the Aguiar–Lauve Eulerian spectrum rests. 

theorem ConnesKreimer.Δ_sf (k : Type u_1) [CommRing k] (f : Forest) : (Δ k) (sf k f) = Δ₀ k f

Δ on a basis forest, packaged for sf.

theorem ConnesKreimer.ε_sf (k : Type u_1) [CommRing k] (p : Forest) : (ε k) (sf k p) = (εmon k) p

ε on a basis forest: the counit of sf f is εmon f.

theorem ConnesKreimer.mul_map_e2 (k : Type u_1) [CommRing k] (F G : H k →ₗ[k] H k) (pr : Forest × Forest) : (LinearMap.mul' k (H k)) ((TensorProduct.map F G) (e2 k pr)) = F (sf k pr.1) * G (sf k pr.2)

μ ∘ (F ⊗ G) on a pure cut-tensor e2 (p,r) is F(p)·G(r).

theorem ConnesKreimer.comul_sf (k : Type u_1) [CommRing k] (f : Forest) : CoalgebraStruct.comul (sf k f) = Δ₀ k f

comul on a basis forest equals the combinatorial Δ₀.

theorem ConnesKreimer.conv_ofConv_sf (k : Type u_1) [CommRing k] (F G : H k →ₗ[k] H k) (f : Forest) : (WithConv.toConv F * WithConv.toConv G).ofConv (sf k f) = (List.map (fun (pr : Forest × Forest) => F (sf k pr.1) * G (sf k pr.2)) (coprodForest f)).sum

Convolution-on-basis engine. (F ⋆ G) on a basis forest is the sum over cuts: (F ⋆ G)(f) = Σ_{(p,r) ∈ coprodForest f} F(p)·G(r).

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

The augmentation projector J = id − u∘ε, as an element of the convolution ring.

Equations

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

theorem ConnesKreimer.convOne_ofConv_sf (k : Type u_1) [CommRing k] (p : Forest) : (WithConv.ofConv 1) (sf k p) = (εmon k) p • 1

The convolution unit 1 = u∘ε on a basis forest: ε(f)·1.

theorem ConnesKreimer.Jc_ofConv_sf (k : Type u_1) [CommRing k] (p : Forest) : (Jc k).ofConv (sf k p) = sf k p - (εmon k) p • 1

J = id − u∘ε on a basis forest: kills the empty forest, identity otherwise.

theorem ConnesKreimer.Jc_pow_ofConv_sf_eq_zero (k : Type u_1) [CommRing k] (n : ℕ) (f : Forest) : sizeF f < n → (Jc k ^ n).ofConv (sf k f) = 0

Local nilpotency. J^{⋆n} = (id − u∘ε)^{⋆n} vanishes on every basis forest with fewer than n nodes. Proof: induction on n via the convolution engine and degree conservation; in a nonzero cut the left leg carries ≥1 node, so the right leg has < n−1 nodes and the induction hypothesis kills it, while an empty left leg is killed by J directly.

The Adams eigenvalue on primitives: Ψₙ(x) = n·x for primitive x.

The first piece of the Aguiar–Lauve spectrum, valid on ANY connected graded bialgebra (no
commutativity needed): the primitives are the eigenspace of every Adams operator `Ψₙ` with
eigenvalue `n`. Proof is at the element level (not the basis): on a primitive `x`, the recursion
`Ψₙ₊₁ = id ⋆ Ψₙ` and `Δx = x⊗1 + 1⊗x` give `Ψₙ₊₁(x) = x + Ψₙ(x)`, and `Ψₙ` fixes the unit. 

def ConnesKreimer.IsPrimitive (k : Type u_1) [CommRing k] (x : H k) : Prop

A primitive element: Δx = x⊗1 + 1⊗x.

Equations

• ConnesKreimer.IsPrimitive k x = ((ConnesKreimer.Δ k) x = x ⊗ₜ[k] 1 + 1 ⊗ₜ[k] x)

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

Convolution at the element level: (F ⋆ G)(x) = μ((F⊗G)(Δx)).

theorem ConnesKreimer.Δ_one_tmul (k : Type u_1) [CommRing k] : (Δ k) 1 = 1 ⊗ₜ[k] 1

Δ(1) = 1⊗1 (the unit is grouplike), in pure-tensor form.

theorem ConnesKreimer.adams_succ_apply (k : Type u_1) [CommRing k] (n : ℕ) (x : H k) : (adams k (n + 1)) x = (LinearMap.mul' k (H k)) ((TensorProduct.map LinearMap.id (adams k n)) ((Δ k) x))

Ψₙ₊₁ = id ⋆ Ψₙ evaluated: Ψₙ₊₁(x) = μ((id⊗Ψₙ)(Δx)).

theorem ConnesKreimer.adams_unit (k : Type u_1) [CommRing k] (n : ℕ) : (adams k n) 1 = 1

Every Adams operator fixes the unit: Ψₙ(1) = 1.

theorem ConnesKreimer.adams_primitive (k : Type u_1) [CommRing k] (n : ℕ) {x : H k} (hx : IsPrimitive k x) : (adams k (n + 1)) x = (n + 1) • x

Adams eigenvalue on primitives: for primitive x, Ψₙ₊₁(x) = (n+1)·x. The primitives are the eigenspace of Ψₙ with eigenvalue n, and S = Ψ₋₁ acts as −1, recovering S(x) = −x.

The first Eulerian idempotent e⁽¹⁾ = log_⋆(id) as a linear map.

Over a `ℚ`-algebra the series `log_⋆(id) = Σ_{k≥1} ((-1)^{k+1}/k)·J^{⋆k}` is, by the local
nilpotency above, finite on each basis forest (only `k ≤ |f|` contribute). We define `e⁽¹⁾`
by that finite per-degree sum, mirroring how `Δ` and the antipode are defined on the basis.
`e⁽¹⁾` kills the unit and fixes primitives (eigenvalue `1`) — the connected-graded projector
onto primitives that begins the Aguiar–Lauve spectral decomposition. 

noncomputable def ConnesKreimer.eulerCoef (k : Type u_1) [CommRing k] [Algebra ℚ k] (j : ℕ) : k

Coefficient (-1)^{j+1}/j of the convolution-log series, pushed into k. j = 0 ↦ 0.

Equations

• ConnesKreimer.eulerCoef k j = (algebraMap ℚ k) ((-1) ^ (j + 1) / ↑j)

@[simp]

theorem ConnesKreimer.eulerCoef_zero (k : Type u_1) [CommRing k] [Algebra ℚ k] : eulerCoef k 0 = 0

@[simp]

theorem ConnesKreimer.eulerCoef_one (k : Type u_1) [CommRing k] [Algebra ℚ k] : eulerCoef k 1 = 1

noncomputable def ConnesKreimer.eulerian1F (k : Type u_1) [CommRing k] [Algebra ℚ k] (f : Forest) : H k

e⁽¹⁾ on a basis forest: the finite log series Σ_{j=0}^{|f|} ((-1)^{j+1}/j)·J^{⋆j}(f) (the j=0 term is 0; terms with j > |f| are absent — and would vanish anyway).

Equations

• ConnesKreimer.eulerian1F k f = (List.map (fun (j : ℕ) => ConnesKreimer.eulerCoef k j • (ConnesKreimer.Jc k ^ j).ofConv (ConnesKreimer.sf k f)) (List.range (ConnesKreimer.sizeF f + 1))).sum

noncomputable def ConnesKreimer.eulerian1 (k : Type u_1) [CommRing k] [Algebra ℚ k] : H k →ₗ[k] H k

The first Eulerian idempotent e⁽¹⁾ : H → H, linear extension of eulerian1F.

Equations

• ConnesKreimer.eulerian1 k = Finsupp.linearCombination k (ConnesKreimer.eulerian1F k) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

theorem ConnesKreimer.eulerian1_sf (k : Type u_1) [CommRing k] [Algebra ℚ k] (f : Forest) : (eulerian1 k) (sf k f) = eulerian1F k f

@[simp]

theorem ConnesKreimer.eulerian1_one (k : Type u_1) [CommRing k] [Algebra ℚ k] : (eulerian1 k) 1 = 0

e⁽¹⁾ kills the unit: there are no positive-degree terms on the empty forest.

theorem ConnesKreimer.eulerian1_dot (k : Type u_1) [CommRing k] [Algebra ℚ k] : (eulerian1 k) (sf k [RTree.node []]) = sf k [RTree.node []]

e⁽¹⁾ fixes the generating primitive • (eigenvalue 1): only the j=1 term survives, with coefficient 1, and J(•) = •.

theorem ConnesKreimer.eulerian1_idem_dot (k : Type u_1) [CommRing k] [Algebra ℚ k] : (eulerian1 k) ((eulerian1 k) (sf k [RTree.node []])) = (eulerian1 k) (sf k [RTree.node []])

Idempotency on the primitive •: e⁽¹⁾(e⁽¹⁾ •) = e⁽¹⁾ •. Immediate from eulerian1_dot (since e⁽¹⁾ fixes •); likewise e⁽¹⁾ is idempotent on anything it fixes or kills.

NOTE (honest scope): the GENERAL projector identity e⁽¹⁾∘e⁽¹⁾ = e⁽¹⁾ is false on this planar (Foissy) Hopf algebra — it is neither commutative nor cocommutative, and the Eulerian idempotents are orthogonal idempotents only in the (co)commutative case (Patras, Loday). On the cherry, e⁽¹⁾∘e⁽¹⁾ and e⁽¹⁾ differ in the •·ℓ₂ vs ℓ₂·• terms (computed by evaluation, not proved here) — exactly the planar non-commutativity. Genuine idempotency (the Hodge/Eulerian decomposition) lives on the commutative quotient (Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Eulerian), not here.

e⁽¹⁾ fixes every primitive (element-level primitive facts).

For primitive `x`: `ε(x)=0`, `J(x)=x`, and `J^{⋆k}(x)=0` for `k ≥ 2` (each higher factor must
absorb the unit, which `J` kills). These feed the operator identity below. 

theorem ConnesKreimer.IsPrimitive.counit_zero (k : Type u_1) [CommRing k] {x : H k} (hx : IsPrimitive k x) : (ε k) x = 0

A primitive element has zero counit (forced by the counit axiom (ε⊗id)∘Δ = 1⊗·).

theorem ConnesKreimer.Jc_ofConv_apply (k : Type u_1) [CommRing k] (x : H k) : (Jc k).ofConv x = x - (ε k) x • 1

J = id − u∘ε at the element level: J(x) = x − ε(x)·1.

theorem ConnesKreimer.Jc_ofConv_one (k : Type u_1) [CommRing k] : (Jc k).ofConv 1 = 0

J kills the unit.

theorem ConnesKreimer.Jc_pow_succ_ofConv_one (k : Type u_1) [CommRing k] (j : ℕ) : (Jc k ^ (j + 1)).ofConv 1 = 0

J^{⋆(j+1)} kills the unit (the first factor J(1)=0).

theorem ConnesKreimer.Jc_ofConv_primitive (k : Type u_1) [CommRing k] {x : H k} (hx : IsPrimitive k x) : (Jc k).ofConv x = x

J fixes a primitive: J(x) = x.

theorem ConnesKreimer.Jc_pow_ofConv_primitive (k : Type u_1) [CommRing k] {x : H k} (hx : IsPrimitive k x) (j : ℕ) : (Jc k ^ (j + 2)).ofConv x = 0

J^{⋆(k+2)} kills a primitive: each of the two top factors absorbs the unit (J(1)=0).

e⁽¹⁾ fixes every primitive (the operator identity).

`e⁽¹⁾` agrees on degree-`≤N` elements with the finite truncation `Σ_{j≤N} c_j J^{⋆j}` (extra
terms vanish by nilpotency); on a primitive only the `j=1` term survives, giving `e⁽¹⁾(x)=x`. 

theorem ConnesKreimer.list_range_sum_eq {M : Type u_2} [AddCommMonoid M] (m : ℕ) (g : ℕ → M) : (List.map g (List.range m)).sum = ∑ j ∈ Finset.range m, g j

Bridge: a List.range map-sum equals the corresponding Finset.range sum.

noncomputable def ConnesKreimer.logTrunc (k : Type u_1) [CommRing k] [Algebra ℚ k] (N : ℕ) : H k →ₗ[k] H k

The degree-N truncation of log_⋆(id), as a linear map.

Equations

• ConnesKreimer.logTrunc k N = ∑ j ∈ Finset.range (N + 1), ConnesKreimer.eulerCoef k j • (ConnesKreimer.Jc k ^ j).ofConv

theorem ConnesKreimer.logTrunc_apply (k : Type u_1) [CommRing k] [Algebra ℚ k] (N : ℕ) (y : H k) : (logTrunc k N) y = ∑ j ∈ Finset.range (N + 1), eulerCoef k j • (Jc k ^ j).ofConv y

theorem ConnesKreimer.eulerian1F_eq_logTrunc (k : Type u_1) [CommRing k] [Algebra ℚ k] (f : Forest) (N : ℕ) (h : sizeF f ≤ N) : eulerian1F k f = (logTrunc k N) (sf k f)

On a basis forest of degree ≤ N, e⁽¹⁾ equals the degree-N truncation (nilpotency kills the surplus terms).

theorem ConnesKreimer.lmap_eq_sum (k : Type u_1) [CommRing k] (g : H k →ₗ[k] H k) (y : H k) : g y = y.coeff.sum fun (a : FreeMonoid RTree) (b : k) => g (MonoidAlgebra.single a b)

A linear endomorphism of H is the basis-sum of its values on the singletons (proved by exact, sidestepping the MonoidAlgebra/Finsupp syntactic wall in rw).

theorem ConnesKreimer.eulerian1_eq_logTrunc (k : Type u_1) [CommRing k] [Algebra ℚ k] (x : H k) (N : ℕ) (hN : ∀ f ∈ x.coeff.support, sizeF f ≤ N) : (eulerian1 k) x = (logTrunc k N) x

e⁽¹⁾ agrees with the truncation logTrunc N on any element supported in degrees ≤ N.

theorem ConnesKreimer.eulerian1_primitive (k : Type u_1) [CommRing k] [Algebra ℚ k] {x : H k} (hx : IsPrimitive k x) : (eulerian1 k) x = x

e⁽¹⁾ fixes every primitive: e⁽¹⁾(x) = x for primitive x. Only the j=1 term of the log series survives (J(x)=x; j=0 has coefficient 0; j≥2 vanish), so e⁽¹⁾(x)=x. The primitives are exactly the eigenvalue-1 eigenspace of e⁽¹⁾.