Physlib

PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Power.Associative

Strong power-associativity of a single Jordan element

i. Overview

Power-associativity is the classical fact (Albert 1947; see Jacobson, *Structure and Representations of Jordan Algebras*, or McCrimmon, *A Taste of Jordan Algebras*, Ch. II) that the subalgebra generated by a single element `a` of a Jordan algebra is *associative*: not merely that the fixed-bracketing powers `a^[n]` from `Operator.lean` are unambiguous (they always were, being defined by a single recursion), but that a[m]∘a[n]=a[m+n]for every m,n, a^{[m]} \circ a^{[n]} = a^{[m+n]} \quad \text{for every } m, n, and more generally that arbitrary polynomials in `a` associate under `∘`. This is what makes `J[a] := \operatorname{span}\{1, a, a^2, \dots\}` (`GeneratedByOne.lean`) into a genuine commutative *associative* ring, letting the whole downstream single-observable spectral theory (`JB/GeneratedByOne/*`) reduce to mathlib's ordinary associative machinery instead of needing a bespoke non-associative functional calculus.

**The operator recursion.** Polarizing the Jordan identity gives an expression for `L_{(a² * y)}` in terms of `L_a`, `L_{a²}`, `L_y`, and `L_{a*y}`. Applied to `y = a^[n]`, this shows recursively that every `L_{a^[n]}` is a polynomial in the commuting operators `L_a` and `L_{a²}`. In particular, `L_a` commutes with every multiplication operator of one of its powers.

Strong power-associativity then follows by a routine induction: assuming `a^{[m]} ∘ a^{[n]} = a^{[m+n]}`, a[m]∘a[n+1]=a[m]∘(a∘a[n])=a∘(a[m]∘a[n])=a∘a[m+n]=a[m+n+1], a^{[m]} \circ a^{[n+1]} = a^{[m]} \circ (a \circ a^{[n]}) = a \circ (a^{[m]} \circ a^{[n]}) = a \circ a^{[m+n]} = a^{[m+n+1]}, where the middle step is exactly `commute_mulLeft_pow m` evaluated at `a^{[n]}`.

ii. Key definitions and results

  • `JordanAlgebra.linearized_mul_sq`: the polarized Jordan identity used by the recursion
  • `JordanAlgebra.commute_mulLeft_pow`: `L_a` commutes with every `L_(a^[n])`
  • `JordanAlgebra.pow_add`: `a^[m] * a^[n] = a^[m+n]`

iii. Table of contents

  • A. Operator commutation for powers
  • B. Strong power-associativity

A. Operator commutation for powers

B. Strong power-associativity

8 declarations

theorem

LaL_a commutes with La2L_{a^2}

In a Jordan algebra EE, for any element a∈Ea \in E, the left multiplication operator LaL_a commutes with the left multiplication operator La2L_{a^2} (where a2=a∘aa^2 = a \circ a). Specifically, for any element b∈Eb \in E, the identity a∘(a2∘b)=a2∘(a∘b) a \circ (a^2 \circ b) = a^2 \circ (a \circ b) holds, where ∘\circ denotes the Jordan product.

theorem

Commutation of LaL_a and LxL_x implies a⋅(x⋅y)=x⋅(a⋅y)a \cdot (x \cdot y) = x \cdot (a \cdot y)

Let EE be a Jordan algebra. For any elements a,x∈Ea, x \in E, if the left multiplication operators LaL_a and LxL_x commute (that is, La∘Lx=Lx∘LaL_a \circ L_x = L_x \circ L_a), then for any element y∈Ey \in E, the following identity holds: a⋅(x⋅y)=x⋅(a⋅y) a \cdot (x \cdot y) = x \cdot (a \cdot y) where ⋅\cdot denotes the Jordan product and La(y)=a⋅yL_a(y) = a \cdot y.

theorem

Polarized Jordan Identity for ((a2)y)z((a^2) y) z

In a Jordan algebra EE, for any elements a,y,z∈Ea, y, z \in E, the following identity (known as the polarized Jordan identity) holds: ((a⋅a)⋅y)⋅z=−2(a⋅(y⋅(a⋅z)))+(a⋅a)⋅(y⋅z)+2((a⋅y)⋅(a⋅z)). ((a \cdot a) \cdot y) \cdot z = -2(a \cdot (y \cdot (a \cdot z))) + (a \cdot a) \cdot (y \cdot z) + 2((a \cdot y) \cdot (a \cdot z)). Here a⋅ba \cdot b denotes the Jordan product and a⋅aa \cdot a is often written as a2a^2.

theorem

(a∘a)∘a[n]=a[n+2](a \circ a) \circ a^{[n]} = a^{[n+2]}

In a Jordan algebra EE, let a[n]a^{[n]} denote the nn-th Jordan power of an element a∈Ea \in E. For any element a∈Ea \in E and any natural number nn, multiplying the nn-th Jordan power by the square a∘aa \circ a raises the degree by two: (a∘a)∘a[n]=a[n+2](a \circ a) \circ a^{[n]} = a^{[n+2]} where ∘\circ denotes the Jordan product.

theorem

Recursive identity for the Jordan multiplication operator La[n+2]L_{a^{[n+2]}}

In a Jordan algebra EE, for any element a∈Ea \in E and any natural number nn, the left multiplication operator La[n+2]L_{a^{[n+2]}} (where a[k]a^{[k]} denotes the kk-th Jordan power) can be expressed in terms of the operators of lower powers as: La[n+2]=−2(La∘La[n]∘La)+La2∘La[n]+2(La[n+1]∘La) L_{a^{[n+2]}} = -2 (L_a \circ L_{a^{[n]}} \circ L_a) + L_{a^2} \circ L_{a^{[n]}} + 2 (L_{a^{[n+1]}} \circ L_a) Here, LxL_x denotes the left multiplication operator defined by Lx(y)=x∘yL_x(y) = x \circ y.

theorem

LaL_a and La2L_{a^2} commute with La[n]L_{a^{[n]}}

In a Jordan algebra EE, for any element a∈Ea \in E and any natural number nn, let LxL_x denote the left multiplication operator Lx(y)=x∘yL_x(y) = x \circ y and a[n]a^{[n]} denote the nn-th Jordan power of aa. Then the operator La[n]L_{a^{[n]}} commutes with both LaL_a and La2L_{a^2} (where a2=a∘aa^2 = a \circ a). That is, LaLa[n]=La[n]LaandLa2La[n]=La[n]La2. L_a L_{a^{[n]}} = L_{a^{[n]}} L_a \quad \text{and} \quad L_{a^2} L_{a^{[n]}} = L_{a^{[n]}} L_{a^2}.

theorem

LaL_a Commutes with La[n]L_{a^{[n]}} in Jordan Algebras

In a Jordan algebra EE, for any element a∈Ea \in E and any natural number nn, the Jordan left multiplication operator LaL_a commutes with the Jordan left multiplication operator La[n]L_{a^{[n]}}. That is, LaLa[n]=La[n]La, L_a L_{a^{[n]}} = L_{a^{[n]}} L_a, where LxL_x is the linear operator defined by Lx(y)=x∘yL_x(y) = x \circ y, and a[n]a^{[n]} denotes the nn-th Jordan power of aa.

theorem

a[m]∘a[n]=a[m+n]a^{[m]} \circ a^{[n]} = a^{[m+n]} in Jordan Algebras

In a Jordan algebra, for any element aa and any natural numbers m,n∈Nm, n \in \mathbb{N}, the mm-th and nn-th Jordan powers of aa satisfy the identity a[m]∘a[n]=a[m+n]a^{[m]} \circ a^{[n]} = a^{[m+n]}, where ∘\circ denotes the Jordan product. This property demonstrates that powers of a single element in a Jordan algebra associate.