The Euclidean Jordan algebra class

The abstract modules of this library built before this one — Peirce, PeirceMul, Orthogonal, Frame, Power, PowerAssoc, FormallyReal, Subalgebra, Block, Pattern and Spectral — state their hypotheses as a tuple drawn from [NonUnitalNonAssocCommRing J] [IsCommJordan J] [Module ℝ J] [IsScalarTower ℝ J J] [IsFormallyReal J] [Module.Finite ℝ J], each module taking the sub-tuple it needs; or — on the Euclidean side of EuclideanJordan/Order.lean and in Spectral's interface section — as a bilinear map m : J →ₗ[ℝ] J →ₗ[ℝ] J carrying hcomm/hjordan/hassoc as ordinary hypotheses. (Witness and Spectral's concrete section state theirs over HermitianMat instead.) Both abstract vocabularies are correct and neither is a class, so a theorem about a Euclidean Jordan algebra cannot be stated by naming one.

This file names one. EuclideanJordanAlgebra J is a real inner-product space with a commutative bilinear product with unit, satisfying the Jordan identity and the associativity of the inner product — Faraut–Korányi's definition (FK III.1).

★ Hypothesis direction. The class is weaker than the textbook definition in two respects, which is the correct direction for an import — a theorem proved over this class applies to the textbook setting, not the other way round. First, finite-dimensionality is folded into the textbook definition and is carried here as a separate [FiniteDimensional ℝ J] argument. Second, a common presentation fixes the inner product to be the trace form ⟪x, y⟫ = tr(x ∘ y) for the Jordan trace, whereas the class asks only that some positive-definite associative inner product exist. inner_mul_one below shows the gap is smaller than it looks: any associative inner product satisfies ⟪x ∘ y, 1⟫ = ⟪x, y⟫, so it is the trace form of the linear functional z ↦ ⟪z, 1⟫. It need not be the form of the Jordan trace — rescaling an associative inner product by a positive constant keeps it associative — and nothing here claims otherwise.

The shape, and the diamond it dodges

★ The product is placed on top of the additive group of the inner-product space, never alongside a second one. Assuming [NormedAddCommGroup J] and [NonUnitalNonAssocCommRing J] simultaneously produces two AddCommGroup J instances and Module ℝ J then fails to synthesise; EuclideanJordan/Bridge.lean records that diamond and ringOfBilinear dodges it by building the multiplicative structure on the ambient additive group. This class is that dodge promoted from a def to a class: it extends Mul J, One J over [NormedAddCommGroup J] [InnerProductSpace ℝ J], so only one AddCommGroup J is ever in play and instNonUnitalNonAssocCommRing below is built from inferInstance on the nose.

Consequently ringOfBilinear (jmulₗ J) mul_comm = instNonUnitalNonAssocCommRing holds by rfl (ringOfBilinear_jmulₗ), which is the statement that the class and the bilinear vocabulary of EuclideanJordan/Order.lean are the same structure and not merely isomorphic ones.

What finite-dimensionality is, and is not, needed for

FiniteDimensional ℝ J is deliberately not a field of the class. It is genuinely required downstream: EuclideanJordan/Spectral.lean records that its spectral_resolution_bilinear — which is spectral_resolution_complete in bilinear vocabulary, and carries the same hypotheses minus the inner product — is false without it, ℝ[X] satisfying every other hypothesis with no nonconstant resolution. So the dimension is carried as a separate instance argument at exactly the theorems that need it, and spectral_resolution_complete' below is one of them.

★ It is not needed for formal reality. instIsFormallyReal below is unconditional: pairing a vanishing sum of squares against the unit turns ∑ᵢ ⟪xᵢ ∘ xᵢ, 1⟫ into ∑ᵢ ⟪xᵢ, xᵢ⟫ by one application of inner_assoc, and a vanishing sum of nonnegative reals has vanishing terms.

This corrects the build plan on two points. The plan derived the instance from EuclideanJordan/Spectral.lean's isFormallyReal_of_fin under [FiniteDimensional ℝ J]. That lemma cannot supply it: isFormallyReal_of_fin takes formal reality as a hypothesis, in Fin k form, and does nothing but reindex it to the Finset form the class IsFormallyReal carries. The derivation had to come from the inner product instead — and once it does, the dimension hypothesis turns out to be unused.

Scope

Almost all of this file is repackaging: the two restatements at the end (spectral_resolution_complete', peirce_add_add') discharge the claim that the existing layer is reachable from the class, and are not new results.

★ Two declarations are not repackaging, and the file should not be described as if they were. inner_mul_one, and instIsFormallyReal resting on it, derive formal reality from the associative inner product, and the existing layer does not contain that derivation anywhere: it takes formal reality as a hypothesis at every abstract site (EuclideanJordan/Spectral.lean's isFormallyReal_of_fin receives it and does nothing but reindex; EuclideanJordan/Order.lean's orderUnitSpaceOfBilinear receives it as [IsFormallyReal J]), and derives it only on the concrete carrier, in EuclideanJordan/Witness.lean's instIsFormallyReal for HermitianMat d 𝕜. Both new declarations are short; the point is only that "this file contains no new mathematics" would be false.

★ One hazard to record for later modules. instNonUnitalNonAssocCommRing fires on any type carrying EuclideanJordanAlgebra, and HermitianMat d 𝕜 already carries a Mul — from EuclideanJordan/Vendor/HermitianMat/Jordan.lean's scoped instance : CommMagma (HermitianMat d 𝕜), whose product is HermitianMat.symmMul. Nothing declares EuclideanJordanAlgebra (HermitianMat d 𝕜) today, and until something does the two never meet; if one is ever declared, that scoped instance and this class's toMul will both be in scope inside open HermMul sections and one of them has to give way.

class EuclideanJordan.EuclideanJordanAlgebra (J : Type u_1) [NormedAddCommGroup J] [InnerProductSpace ℝ J] extends Mul J, One J : Type u_1

A Euclidean Jordan algebra: a real inner-product space carrying a commutative bilinear product with unit, satisfying the Jordan identity and the associativity of the inner product.

This is Faraut–Korányi's definition (FK III.1), weakened in the two ways the module docstring records: finite-dimensionality is not a field, and the inner product is an arbitrary associative one rather than the Jordan trace form. Both weakenings run in the import-safe direction.

• mul : J → J → J
• one : J
• mul_comm (x y : J) : x * y = y * x

  The Jordan product is commutative.

• add_mul (x y z : J) : (x + y) * z = x * z + y * z

  The Jordan product is additive in its left argument.

• smul_mul (r : ℝ) (x y : J) : r • x * y = r • (x * y)

  The Jordan product is homogeneous in its left argument.

• one_mul (x : J) : 1 * x = x

  1 is a unit for the Jordan product.

• jordan (x y : J) : x * (x * x * y) = x * x * (x * y)

  The Jordan identity, x ∘ (x² ∘ y) = x² ∘ (x ∘ y).

• inner_assoc (x y z : J) : inner ℝ (x * y) z = inner ℝ y (x * z)

  The inner product is associative: ⟪x ∘ y, z⟫ = ⟪y, x ∘ z⟫. This is what "Euclidean" adds to "formally real"; EuclideanJordan/Order.lean carries the same condition as the hypothesis hassoc.

theorem EuclideanJordan.EuclideanJordanAlgebra.zero_mul' {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (a : J) : 0 * a = 0

Left multiplication by 0 is 0 — the one ring axiom the class does not state, obtained from additivity at (0, 0, a).

@[instance_reducible]

instance EuclideanJordan.EuclideanJordanAlgebra.instNonUnitalNonAssocCommRing {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] : NonUnitalNonAssocCommRing J

The ring structure, built on the ambient additive group.

Equations

• One or more equations did not get rendered due to their size.

instance EuclideanJordan.EuclideanJordanAlgebra.instIsCommJordan {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] : IsCommJordan J

Mathlib's Jordan class. Its field lmul_comm_rmul_rmul is oriented a ∘ b ∘ (a ∘ a) = a ∘ (b ∘ (a ∘ a)), which is the class's jordan field read through commutativity twice.

instance EuclideanJordan.EuclideanJordanAlgebra.instIsScalarTower {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] : IsScalarTower ℝ J J

instance EuclideanJordan.EuclideanJordanAlgebra.instSMulCommClass {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] : SMulCommClass ℝ J J

Required by Submodule-valued and NonUnitalSubalgebra-valued subobject constructions downstream; do not remove because nothing in this file uses it.

theorem EuclideanJordan.EuclideanJordanAlgebra.mul_one' {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (x : J) : x * 1 = x

theorem EuclideanJordan.EuclideanJordanAlgebra.inner_mul_one {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (x y : J) : inner ℝ (x * y) 1 = inner ℝ x y

The inner product is a trace form. ⟪x ∘ y, 1⟫ = ⟪x, y⟫: one application of inner_assoc against the unit. So the linear functional z ↦ ⟪z, 1⟫ plays the role the article's tr plays, and the inner product's positive-definiteness is available as positive-definiteness of that form on products. It is not claimed that this functional is the Jordan trace — see the module docstring.

instance EuclideanJordan.EuclideanJordanAlgebra.instIsFormallyReal {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] : IsFormallyReal J

Formal reality, from the inner product. Unconditional on the dimension — see the module docstring.

theorem EuclideanJordan.EuclideanJordanAlgebra.inner_assoc' {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (x y z : J) : inner ℝ (x * y) z = inner ℝ x (y * z)

The associativity of the inner product in its other orientation, ⟪x ∘ y, z⟫ = ⟪x, y ∘ z⟫, obtained from the field by commuting the product.

The bridge to the bilinear-map vocabulary

EuclideanJordan/Order.lean's Euclidean section and EuclideanJordan/Spectral.lean's interface section state everything over a bundled m : J →ₗ[ℝ] J →ₗ[ℝ] J carrying hcomm, hjordan, hassoc and a Fin k-indexed formal-reality hypothesis. jmulₗ is the class's product in that vocabulary and the five lemmas after it are exactly that hypothesis tuple, so a consumer of orderUnitSpaceOfBilinear, inner_left_coeff, isArchimedean_ofBilinear, isSoS_iff_exists_sq or spectral_resolution_bilinear supplies them by name rather than rebuilding them.

def EuclideanJordan.jmulₗ (J : Type u_1) [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] : J →ₗ[ℝ] J →ₗ[ℝ] J

The Jordan product of a EuclideanJordanAlgebra as a bundled bilinear map.

Equations

• EuclideanJordan.jmulₗ J = LinearMap.mk₂ ℝ (fun (x1 x2 : J) => x1 * x2) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem EuclideanJordan.jmulₗ_apply {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (x y : J) : ((jmulₗ J) x) y = x * y

theorem EuclideanJordan.ringOfBilinear_jmulₗ {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] : ringOfBilinear (jmulₗ J) ⋯ = EuclideanJordanAlgebra.instNonUnitalNonAssocCommRing

★ The class and EuclideanJordan/Bridge.lean's ringOfBilinear produce the same ring structure, definitionally. This is the precise sense in which the class does not introduce a second multiplicative structure alongside the one the existing layer runs on.

theorem EuclideanJordan.jmulₗ_comm {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (x y : J) : ((jmulₗ J) x) y = ((jmulₗ J) y) x

theorem EuclideanJordan.jmulₗ_jordan {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (a b : J) : ((jmulₗ J) (((jmulₗ J) a) b)) (((jmulₗ J) a) a) = ((jmulₗ J) a) (((jmulₗ J) b) (((jmulₗ J) a) a))

theorem EuclideanJordan.jmulₗ_inner_assoc {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (x y z : J) : inner ℝ (((jmulₗ J) x) y) z = inner ℝ y (((jmulₗ J) x) z)

theorem EuclideanJordan.jmulₗ_one_mul {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (y : J) : ((jmulₗ J) 1) y = y

theorem EuclideanJordan.jmulₗ_formallyReal {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (k : ℕ) (f : Fin k → J) (h : ∑ i : Fin k, ((jmulₗ J) (f i)) (f i) = 0) (i : Fin k) : f i = 0

Formal reality in the Fin k form spectral_resolution_bilinear and isFormallyReal_of_fin take.

The existing layer, restated over the class

theorem EuclideanJordan.spectral_resolution_complete' {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] [FiniteDimensional ℝ J] (x : J) : ∃ (n : ℕ) (c : Fin n → J) (lam : Fin n → ℝ), IsOrthIdemFamily c ∧ ∑ i : Fin n, c i = 1 ∧ x = ∑ i : Fin n, lam i • c i

The spectral theorem with completeness, over the class. EuclideanJordan/Spectral.lean's spectral_resolution_complete carries the unit as an explicit hypothesis he : ∀ y, e ∘ y = y because it has no One; the class supplies it.

theorem EuclideanJordan.peirce_add_add' {J : Type u_1} [NormedAddCommGroup J] [InnerProductSpace ℝ J] [EuclideanJordanAlgebra J] (c y : J) : (peirceOne c) y + (peirceHalf c) y + (peirceZero c) y = y

The Peirce decomposition at a single idempotent, over the class. EuclideanJordan/Peirce.lean's peirce_add_add needs no idempotency hypothesis: the three projections sum to the identity for every c.