The Peirce decomposition at a single idempotent

It is natural to expect the Peirce decomposition to depend on the spectral theorem. It does not, in the direction that matters, and this file is the evidence. The Peirce decomposition at a given idempotent needs the Jordan identity and the invertibility of 2, and nothing else: no spectral theorem, no formal reality, no finite dimension, no inner product, not even a unit. ★ The first draft of this sentence said "the Jordan identity and nothing else", which is wrong — peirce_poly divides by 2 (two_smul_eq_zero'), which is why every statement below it carries Module ℝ J. Only the linearised identities two_lin1_raw/two_lin1_apply are genuinely torsion-free, and they are, deliberately: their factor of 2 is carried in the statement rather than cancelled. Caught 2026-08-12 by reading the omit lines against this paragraph. What the spectral theorem is needed for is producing idempotents — a Jordan frame — not for decomposing at one that is already in hand. EuclideanJordan/FrameExists.lean does the producing; this file does the decomposing.

The mathematics

For an idempotent c, the multiplication operator L_c : y ↦ c ∘ y satisfies

2·L_c³ − 3·L_c² + L_c = 0, i.e. L_c (L_c − 1) (2L_c − 1) = 0,

so its only possible eigenvalues are 0, 1/2, 1, and the three Lagrange interpolants at those roots are projections summing to the identity. That is the Peirce decomposition J = J₁(c) ⊕ J_{1/2}(c) ⊕ J₀(c).

The polynomial identity comes from one substitution into the linearised Jordan identity. Writing ⁅·,·⁆ for the commutator of multiplication operators, polarising the Jordan identity ⁅L_x, L_{x²}⁆ = 0 at x = a ± b and subtracting gives

⁅L_{a²}, L_b⁆ + 2⁅L_{ab}, L_a⁆ = 0 (two_lin1_raw, up to a factor of 2),

and evaluating that at a := c, b := y, argument := c collapses immediately to the Peirce polynomial. Mathlib proves only the a ↔ b symmetrised consequence (two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add), which is strictly weaker; the a − b substitution is what separates the two halves, and it costs one extra line.

What is here, and what is not

Here: the polynomial identity, the three projections, the resolution of the identity, the three eigenvalue equations, existence and uniqueness of the decomposition, and the trichotomy (L_c has no eigenvalue outside {0, 1/2, 1}).

Not here: the Faraut–Korányi multiplication rules between Peirce components (J_i ∘ J_j ⊆ …), which are EuclideanJordan/PeirceMul.lean, and the decomposition relative to a whole Jordan frame, which is EuclideanJordan/FramePeirce.lean. Nothing in this file should be read as covering them.

References

Mathlib's Jordan support (Mathlib/Algebra/Jordan/Basic.lean, 237 lines) is the classes IsJordan / IsCommJordan, five operator-commutation lemmas and two linearised identities. There is no idempotent theory, no Peirce decomposition and no spectral theory in Mathlib; we are aware of none in any other proof assistant either, though we have not searched them systematically.

• Faraut and Korányi, Analysis on Symmetric Cones, Prop. IV.1.1.
• McCrimmon, A Taste of Jordan Algebras, §II.8.

Applying an AddMonoid.End expression to an element is definitional in every constructor we use, but Mathlib's corresponding lemmas are phrased for the AddMonoidHom coercion and do not match the AddMonoid.End one. Lean 4.28's simp set bridged this on its own; 4.30's does not, so the four rfls are stated here and passed to simpa explicitly.

theorem EuclideanJordan.two_lin1_raw {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] (a b : J) : 2 • ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (a * a)⁆ + 4 • ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (a * b)⁆ = 0

Twice the linearised Jordan identity. Polarising ⁅L_x, L_{x²}⁆ = 0 at x = a + b and at x = a − b and subtracting isolates the half that the symmetrised Mathlib version (two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add) leaves fused.

Stated with the factor 2 carried rather than cancelled, so that this lemma needs no torsion hypothesis and holds over any NonUnitalNonAssocCommRing.

theorem EuclideanJordan.two_lin1_apply {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] (a b w : J) : 2 • (b * (a * a * w) - a * a * (b * w)) + 4 • (a * (a * b * w) - a * b * (a * w)) = 0

two_lin1_raw evaluated at an element.

theorem EuclideanJordan.mul_smul_comm' {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (r : ℝ) (a b : J) : a * r • b = r • (a * b)

In a commutative algebra the scalar-tower rule already gives the SMulCommClass rule, so only IsScalarTower has to be assumed — which is what the concrete carrier HermitianMat supplies (EuclideanJordan/Vendor/HermitianMat/Jordan.lean).

def EuclideanJordan.mulL {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c : J) : J →ₗ[ℝ] J

The Jordan multiplication operator L_c : y ↦ c ∘ y, as an ℝ-linear map.

Equations

• EuclideanJordan.mulL c = { toFun := fun (y : J) => c * y, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem EuclideanJordan.mulL_apply {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c y : J) : (mulL c) y = c * y

def EuclideanJordan.peirceOne {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c : J) : J →ₗ[ℝ] J

The Peirce projection onto the 1-eigenspace of L_c: the Lagrange interpolant 2L² − L, which is 1 at 1 and 0 at 0 and 1/2.

Equations

• EuclideanJordan.peirceOne c = 2 • EuclideanJordan.mulL c ∘ₗ EuclideanJordan.mulL c - EuclideanJordan.mulL c

def EuclideanJordan.peirceHalf {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c : J) : J →ₗ[ℝ] J

The Peirce projection onto the 1/2-eigenspace of L_c: the Lagrange interpolant 4L − 4L².

Equations

• EuclideanJordan.peirceHalf c = 4 • EuclideanJordan.mulL c - 4 • EuclideanJordan.mulL c ∘ₗ EuclideanJordan.mulL c

def EuclideanJordan.peirceZero {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c : J) : J →ₗ[ℝ] J

The Peirce projection onto the 0-eigenspace of L_c: the Lagrange interpolant 1 − 3L + 2L².

Equations

• EuclideanJordan.peirceZero c = LinearMap.id - 3 • EuclideanJordan.mulL c + 2 • EuclideanJordan.mulL c ∘ₗ EuclideanJordan.mulL c

@[simp]

theorem EuclideanJordan.peirceOne_apply {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c y : J) : (peirceOne c) y = 2 • (c * (c * y)) - c * y

@[simp]

theorem EuclideanJordan.peirceHalf_apply {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c y : J) : (peirceHalf c) y = 4 • (c * y) - 4 • (c * (c * y))

@[simp]

theorem EuclideanJordan.peirceZero_apply {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c y : J) : (peirceZero c) y = y - 3 • (c * y) + 2 • (c * (c * y))

theorem EuclideanJordan.peirce_add_add {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] (c y : J) : (peirceOne c) y + (peirceHalf c) y + (peirceZero c) y = y

The resolution of the identity. The three Lagrange interpolants sum to 1.

★ This is pure polynomial arithmetic and holds for every c, idempotent or not — it is the Jordan identity that makes the three summands land in the eigenspaces, not the resolution itself. Keeping the two facts separate is what makes the failure mode visible: a decomposition into three pieces is worthless without knowing what the pieces are.

How the projections act on the eigenspaces

These six lemmas are the "already an eigenvector" direction, and — like peirce_add_add — they are polynomial arithmetic that needs no Jordan identity: they say what the Lagrange interpolants do to something already known to satisfy c ∘ y = μ • y.

theorem EuclideanJordan.peirceOne_of_eigen {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] {c y : J} (h : c * y = y) : (peirceOne c) y = y

On the 1-eigenspace, peirceOne is the identity.

theorem EuclideanJordan.peirceOne_of_eigen_half {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] {c y : J} (h : c * y = 2⁻¹ • y) : (peirceOne c) y = 0

peirceOne kills the 1/2-eigenspace.

theorem EuclideanJordan.peirceOne_of_eigen_zero {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] {c y : J} (h : c * y = 0) : (peirceOne c) y = 0

peirceOne kills the 0-eigenspace.

theorem EuclideanJordan.peirceHalf_of_eigen {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] {c y : J} (h : c * y = y) : (peirceHalf c) y = 0

peirceHalf kills the 1-eigenspace.

theorem EuclideanJordan.peirceHalf_of_eigen_half {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] {c y : J} (h : c * y = 2⁻¹ • y) : (peirceHalf c) y = y

On the 1/2-eigenspace, peirceHalf is the identity.

theorem EuclideanJordan.peirceHalf_of_eigen_zero {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] {c y : J} (h : c * y = 0) : (peirceHalf c) y = 0

peirceHalf kills the 0-eigenspace.

theorem EuclideanJordan.peirce_poly {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c : J} (hc : c * c = c) (y : J) : 2 • (c * (c * (c * y))) + c * y = 3 • (c * (c * y))

The Peirce polynomial identity. For an idempotent c,

2·L_c³ − 3·L_c² + L_c = 0, i.e. L_c (L_c − 1) (2L_c − 1) = 0.

Everything else in this file is a consequence. The proof is two_lin1_apply at a := c, b := y, argument := c, and nothing more: the hypotheses are the Jordan identity and c ∘ c = c.

theorem EuclideanJordan.peirce_cube {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c : J} (hc : c * c = c) (y : J) : c * (c * (c * y)) = (3 / 2) • (c * (c * y)) - 2⁻¹ • (c * y)

peirce_poly solved for the cube, over ℝ — the form every consumer below uses.

theorem EuclideanJordan.mul_peirceOne {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c : J} (hc : c * c = c) (y : J) : c * (peirceOne c) y = (peirceOne c) y

The image of peirceOne c lies in the 1-eigenspace of L_c.

theorem EuclideanJordan.mul_peirceHalf {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c : J} (hc : c * c = c) (y : J) : c * (peirceHalf c) y = 2⁻¹ • (peirceHalf c) y

The image of peirceHalf c lies in the 1/2-eigenspace of L_c.

theorem EuclideanJordan.mul_peirceZero {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c : J} (hc : c * c = c) (y : J) : c * (peirceZero c) y = 0

The image of peirceZero c lies in the 0-eigenspace of L_c.

theorem EuclideanJordan.exists_peirce_decomposition {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c : J} (hc : c * c = c) (y : J) : ∃ (y₁ : J) (yₕ : J) (y₀ : J), c * y₁ = y₁ ∧ c * yₕ = 2⁻¹ • yₕ ∧ c * y₀ = 0 ∧ y = y₁ + yₕ + y₀

The Peirce decomposition, existence half. Every element of a real commutative Jordan algebra splits, relative to any idempotent c, into a part fixed by L_c, a part halved by it, and a part killed by it.

theorem EuclideanJordan.peirce_eq_zero_of_add_eq_zero {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J] {c y₁ yₕ y₀ : J} (h₁ : c * y₁ = y₁) (hₕ : c * yₕ = 2⁻¹ • yₕ) (h₀ : c * y₀ = 0) (h : y₁ + yₕ + y₀ = 0) : y₁ = 0 ∧ yₕ = 0 ∧ y₀ = 0

The Peirce decomposition, uniqueness half. A vanishing sum of Peirce components is componentwise zero — so the decomposition of exists_peirce_decomposition is unique, and J = J₁(c) ⊕ J_{1/2}(c) ⊕ J₀(c) is a genuine direct sum.

The proof needs no independence-of-eigenspaces import: applying the two projections peirceOne and peirceHalf to the relation reads off two of the three components, and the third follows by subtraction.

theorem EuclideanJordan.eigenvalue_trichotomy {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c : J} (hc : c * c = c) {y : J} (hy : y ≠ 0) {μ : ℝ} (h : c * y = μ • y) : μ = 0 ∨ μ = 2⁻¹ ∨ μ = 1

The eigenvalue trichotomy. L_c has no eigenvalue outside {0, 1/2, 1}: the Peirce polynomial annihilates it, and its roots are exactly those three.

★ Stated for a nonzero eigenvector, which is the whole content — the equation c ∘ y = μ • y is satisfied by y = 0 for every μ.