Documentation

LeanPool.EuclideanJordan.EuclideanJordan.PeirceMul

The Peirce multiplication rules #

EuclideanJordan/Peirce.lean decomposes J = J₁(c) ⊕ J_{1/2}(c) ⊕ J₀(c) for an idempotent c. This file proves how the three components multiply — the Faraut–Korányi relations:

J₁J_{1/2}J₀
J₁⊆ J₁⊆ J_{1/2}= 0
J_{1/2}⊆ J_{1/2}⊆ J₁ ⊕ J₀⊆ J_{1/2}
J₀= 0⊆ J_{1/2}⊆ J₀

As in EuclideanJordan/Peirce.lean, the hypotheses are the Jordan identity and the invertibility of the integers used (2 for the commuting rules, 4 for the half-half rule): no spectral theorem, no formal reality, no finite dimension, no unit.

The two ingredients #

EuclideanJordan/Peirce.lean needed only the once-linearised Jordan identity two_lin1_raw. Five of the six rules follow from a single consequence of it — L_x commutes with L_c whenever x lies in J₁(c) or J₀(c) (mul_comm_of_eigen_one, mul_comm_of_eigen_zero) — after which each rule is one rewrite.

The sixth, J_{1/2} ∘ J_{1/2} ⊆ J₁ ⊕ J₀, is genuinely deeper and needs the fully linearised identity four_lin2_raw, obtained here by polarising two_lin1_raw a second time. Evaluated at the right point it collapses to L_c² = L_c on the product, which is exactly "the 1/2-component vanishes".

Why opCommute_eigen_one_zero is the one to look at #

The Faraut–Korányi simultaneous-diagonalisation fact — an element scalar on range q and an element of J₂(q) operator-commute — is the load-bearing hypothesis in the coalescence arguments that run over a Jordan frame. Its single-idempotent case is opCommute_eigen_one_zero below, and it is three lines from four_lin2_raw.

★ That is a case, not the frame-level statement. The frame-level version quantifies over a rank-two q = pᵢ + pⱼ drawn from a Jordan frame, and this file has no frame. EuclideanJordan/Frame.lean puts it in frame shape (opCommute_scalarOn_frame) once orthogonal idempotent families are available, and EuclideanJordan/Block.lean supplies the projection commutation (peirceOne_comm_peirceOne and siblings) and the exact characterisation of the rank-two block.

References #

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.

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

Four times the fully linearised Jordan identity. Polarising two_lin1_raw a second time, in a := p + q, and subtracting the two pure terms leaves the cyclic sum

⁅L_b, L_{pq}⁆ + ⁅L_p, L_{qb}⁆ + ⁅L_q, L_{pb}⁆ = 0,

which is the identity every Peirce multiplication rule beyond the commuting ones needs. The factor 4 is carried rather than cancelled so that this holds with no torsion hypothesis.

source
theorem EuclideanJordan.four_lin2_apply {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] (p q b w : J) :
4 • (b * (p * q * w) - p * q * (b * w) + (p * (q * b * w) - q * b * (p * w)) + (q * (p * b * w) - p * b * (q * w))) = 0

four_lin2_raw evaluated at an element.

source
theorem EuclideanJordan.nsmul_eq_zero_iff' {J : Type u_1} [NonUnitalNonAssocCommRing J] [Module ℝ J] {n : ℕ} (hn : n ≠ 0) {x : J} (h : n • x = 0) :
x = 0

Cancel a nonzero natural multiple in a real vector space.

source
theorem EuclideanJordan.mul_comm_of_eigen_one {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c x : J} (hc : c * c = c) (hx : c * x = x) (w : J) :
c * (x * w) = x * (c * w)

L_x commutes with L_c when c ∘ x = x. The 1-eigenvectors of L_c are operator-compatible with c. Five of the six multiplication rules come from this and its 0-eigenvalue twin.

source
theorem EuclideanJordan.mul_comm_of_eigen_zero {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c x : J} (hc : c * c = c) (hx : c * x = 0) (w : J) :
c * (x * w) = x * (c * w)

L_x commutes with L_c when c ∘ x = 0.

source
theorem EuclideanJordan.eigen_one_mul_one {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c x y : J} (hc : c * c = c) (hx : c * x = x) (hy : c * y = y) :
c * (x * y) = x * y

J₁(c) ∘ J₁(c) ⊆ J₁(c).

source
theorem EuclideanJordan.eigen_zero_mul_zero {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c x y : J} (hc : c * c = c) (hx : c * x = 0) (hy : c * y = 0) :
c * (x * y) = 0

J₀(c) ∘ J₀(c) ⊆ J₀(c).

source
theorem EuclideanJordan.eigen_one_mul_zero {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c x y : J} (hc : c * c = c) (hx : c * x = x) (hy : c * y = 0) :
x * y = 0

J₁(c) ∘ J₀(c) = 0 — the two extreme Peirce components annihilate each other, and not merely land in a common component.

The proof reads the same product twice: L_c fixes it because x ∈ J₁, and L_c kills it because y ∈ J₀.

source
theorem EuclideanJordan.opCommute_eigen_one_zero {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] {c x y : J} (hc : c * c = c) (hx : c * x = x) (hy : c * y = 0) (w : J) :
x * (y * w) = y * (x * w)

The single-idempotent case of Faraut–Korányi simultaneous diagonalisation.

An element of J₁(c) and an element of J₀(c) operator-commute: L_x L_y = L_y L_x, which is strictly more than the product x ∘ y vanishing. It falls straight out of the cyclic identity, because two of its three brackets vanish.

★ This is the case q = c, not the field: the field ranges over a rank-two q = pᵢ + pⱼ inside a Jordan frame, and there is no frame in this file.

source
theorem EuclideanJordan.eigen_one_mul_half {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c x y : J} (hc : c * c = c) (hx : c * x = x) (hy : c * y = 2⁻¹ • y) :
c * (x * y) = 2⁻¹ • (x * y)

J₁(c) ∘ J_{1/2}(c) ⊆ J_{1/2}(c).

source
theorem EuclideanJordan.eigen_zero_mul_half {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c x y : J} (hc : c * c = c) (hx : c * x = 0) (hy : c * y = 2⁻¹ • y) :
c * (x * y) = 2⁻¹ • (x * y)

J₀(c) ∘ J_{1/2}(c) ⊆ J_{1/2}(c).

source
theorem EuclideanJordan.eigen_half_mul_half {J : Type u_1} [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] {c x y : J} (hc : c * c = c) (hx : c * x = 2⁻¹ • x) (hy : c * y = 2⁻¹ • y) :
c * (c * (x * y)) = c * (x * y)

J_{1/2}(c) ∘ J_{1/2}(c) ⊆ J₁(c) ⊕ J₀(c), stated as the polynomial relation L_c² = L_c on the product — which is exactly "no 1/2-component", since peirceHalf c z = 4•(c ∘ z) − 4•(c ∘ (c ∘ z)) collapses to 0 under it (peirceHalf_mul_half_eq_zero). ★ An earlier draft attributed this to the eigenvalue trichotomy. It does not use the trichotomy — it is the projection formula directly.

This is the one rule that needs the fully linearised identity: evaluating four_lin2_raw at (c, y, x) and argument c, the four 1/4-terms cancel in pairs and what survives is L_c²(xy) − L_c(xy) = 0.

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

The 1/2-component of a product of two 1/2-elements vanishes — eigen_half_mul_half read through the projection of EuclideanJordan/Peirce.lean.