Split composition algebras (GPR 21.19)

GPR 21.19 first defines a composition algebra of constant rank 1, 2, 4, or 8 to be split when it is isomorphic to the corresponding standard model: k, k × k, Mat₂(k), or Zor(k). For a composition algebra whose rank varies across Spec k, it then applies this condition to the four factors of the rank decomposition (GPR Exc. 9.31).

This file formalizes both levels. Since mathlib's AlgEquiv requires associative multiplication, an isomorphism of conic algebras is expressed by a norm isometry which preserves 1 and multiplication. This is the same representation used by Composition/NormClassification.lean.

Main definitions

• ConicAlgebra.Isomorphic : existence of a unital multiplicative norm isometry.
• ConicAlgebra.IsSplitOfRank : the four constant-rank clauses of GPR 21.19.
• ConicAlgebra.SplitRankFactor, ConicAlgebra.splitRankComponent : the factor ring and base-changed conic algebra cut out by a rank idempotent.
• ConicAlgebra.IsSplit : the composition property together with splitness on all four rank components.

Main results

• ConicAlgebra.Isomorphic.refl, .symm, .trans : conic-algebra isomorphism is an equivalence relation.
• ConicAlgebra.Isomorphic.of_subsingleton : over the zero ring, any two conic algebras are isomorphic.
• ConicAlgebra.Isomorphic.isComposition : composition transports across an isomorphism.
• ConicAlgebra.isSplitOfRank_baseRing, .isSplitOfRank_splitEtale, .isSplitOfRank_splitQuaternion, .isSplitOfRank_zor : the four standard models are split.
• ConicAlgebra.IsSplitOfRank.hasElementaryIdempotent_of_two_or_four_or_eight : the constant-rank form of the easy direction of GPR 22.16.

Implementation notes

IsSplitOfRank C r does not separately store the assertion that C has rank r: an isomorphism to the standard model already forces that equality. The general predicate uses the quotients

k ⧸ (1 - rankIdempotent k A r)

for r = 1, 2, 4, 8, exactly as in the rank decomposition. Zero factors are retained, as in GPR 21.19; this also handles the zero base ring without a separate definition.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Exc. 9.31, 21.19, 22.16.

def ConicAlgebra.Isomorphic {k : Type u} {A : Type v} {B : Type w} [CommRing k] [NonAssocRing A] [Module k A] [NonAssocRing B] [Module k B] (C : ConicAlgebra k A) (D : ConicAlgebra k B) : Prop

Two conic algebras are isomorphic when there is a norm isometry preserving 1 and multiplication.

⚠ Mathlib's AlgEquiv is not used because the algebras need not be associative.

Equations

• C.Isomorphic D = ∃ (e : QuadraticMap.IsometryEquiv C.norm D.norm), e 1 = 1 ∧ ∀ (x y : A), e (x * y) = e x * e y

theorem ConicAlgebra.Isomorphic.of_subsingleton {k : Type u} {A : Type v} {B : Type w} [CommRing k] [NonAssocRing A] [Module k A] [NonAssocRing B] [Module k B] {C : ConicAlgebra k A} {D : ConicAlgebra k B} [Subsingleton k] : C.Isomorphic D

Over a subsingleton base ring, any two conic algebras are isomorphic. Their underlying modules, the norm values, and all algebra elements are subsingletons.

theorem ConicAlgebra.Isomorphic.refl {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) : C.Isomorphic C

A conic algebra is isomorphic to itself.

theorem ConicAlgebra.Isomorphic.symm {k : Type u} {A : Type v} {B : Type w} [CommRing k] [NonAssocRing A] [Module k A] [NonAssocRing B] [Module k B] {C : ConicAlgebra k A} {D : ConicAlgebra k B} (h : C.Isomorphic D) : D.Isomorphic C

The inverse of an isomorphism of conic algebras.

theorem ConicAlgebra.Isomorphic.trans {k : Type u} {A : Type v} {B : Type w} [CommRing k] [NonAssocRing A] [Module k A] [NonAssocRing B] [Module k B] {C : ConicAlgebra k A} {D : ConicAlgebra k B} {E : Type t} [NonAssocRing E] [Module k E] {G : ConicAlgebra k E} (hCD : C.Isomorphic D) (hDG : D.Isomorphic G) : C.Isomorphic G

The composite of two isomorphisms of conic algebras.

theorem ConicAlgebra.Isomorphic.isComposition {k : Type u} {A : Type v} {B : Type w} [CommRing k] [NonAssocRing A] [Module k A] [NonAssocRing B] [Module k B] {C : ConicAlgebra k A} {D : ConicAlgebra k B} [Module.Finite k A] [Module.Projective k A] [Module.Finite k B] [Module.Projective k B] (h : C.Isomorphic D) (hD : D.IsComposition) : C.IsComposition

Composition transports backwards across an isomorphism of conic algebras.

theorem ConicAlgebra.IsElementaryIdempotent.map_isometryEquiv {k : Type u} {A : Type v} {B : Type w} [CommRing k] [NonAssocRing A] [Module k A] [NonAssocRing B] [Module k B] {C : ConicAlgebra k A} {D : ConicAlgebra k B} {c : A} (hc : C.IsElementaryIdempotent c) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (he1 : e 1 = 1) : D.IsElementaryIdempotent (e c)

A unital norm isometry carries elementary idempotents to elementary idempotents.

theorem ConicAlgebra.Isomorphic.hasElementaryIdempotent_iff {k : Type u} {A : Type v} {B : Type w} [CommRing k] [NonAssocRing A] [Module k A] [NonAssocRing B] [Module k B] {C : ConicAlgebra k A} {D : ConicAlgebra k B} (h : C.Isomorphic D) : C.HasElementaryIdempotent ↔ D.HasElementaryIdempotent

Having an elementary idempotent is invariant under conic-algebra isomorphism.

Constant-rank splitness

def ConicAlgebra.IsSplitOfRank {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) : ℕ → Prop

GPR 21.19(a)–(d). A conic algebra is split of rank r if it is isomorphic to the standard model of rank r. The predicate is false for ranks other than 1, 2, 4, and 8.

This definition is intended for composition algebras; Isomorphic.isComposition shows that being isomorphic to one of the standard models supplies the composition laws.

Equations

• C.IsSplitOfRank 1 = C.Isomorphic (ConicAlgebra.baseRing k)
• C.IsSplitOfRank 2 = C.Isomorphic (ConicAlgebra.splitEtale k)
• C.IsSplitOfRank 4 = C.Isomorphic (ConicAlgebra.splitQuaternion k)
• C.IsSplitOfRank 8 = C.Isomorphic (ConicAlgebra.zor k)
• C.IsSplitOfRank x✝ = False

@[simp]

theorem ConicAlgebra.isSplitOfRank_one_iff {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} : C.IsSplitOfRank 1 ↔ C.Isomorphic (baseRing k)

@[simp]

theorem ConicAlgebra.isSplitOfRank_two_iff {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} : C.IsSplitOfRank 2 ↔ C.Isomorphic (splitEtale k)

@[simp]

theorem ConicAlgebra.isSplitOfRank_four_iff {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} : C.IsSplitOfRank 4 ↔ C.Isomorphic (splitQuaternion k)

@[simp]

theorem ConicAlgebra.isSplitOfRank_eight_iff {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} : C.IsSplitOfRank 8 ↔ C.Isomorphic (zor k)

theorem ConicAlgebra.isSplitOfRank_baseRing (k : Type u) [CommRing k] : (baseRing k).IsSplitOfRank 1

The standard rank-one composition algebra is split of rank one.

theorem ConicAlgebra.isSplitOfRank_splitEtale (k : Type u) [CommRing k] : (splitEtale k).IsSplitOfRank 2

The split quadratic étale algebra is split of rank two.

theorem ConicAlgebra.isSplitOfRank_splitQuaternion (k : Type u) [CommRing k] : (splitQuaternion k).IsSplitOfRank 4

The split quaternion algebra is split of rank four.

theorem ConicAlgebra.isSplitOfRank_zor (k : Type u) [CommRing k] : (zor k).IsSplitOfRank 8

The Zorn vector matrix algebra is split of rank eight.

theorem ConicAlgebra.IsSplitOfRank.hasElementaryIdempotent_of_two_or_four_or_eight {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {r : ℕ} (h : C.IsSplitOfRank r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.HasElementaryIdempotent

GPR 22.16, constant-rank easy direction. A split algebra of rank 2, 4, or 8 has an elementary idempotent. The three standard models have visible elementary idempotents, and the property is transported back across the defining isomorphism.

Splitness through the rank decomposition

@[reducible, inline]

abbrev ConicAlgebra.SplitRankFactor (k : Type u) (A : Type v) [CommRing k] [AddCommGroup A] [Module k A] [Module.Finite k A] [Module.Projective k A] (r : ℕ) : Type u

The factor of the base ring on which A has constant rank r (GPR Exc. 9.31).

Equations

• ConicAlgebra.SplitRankFactor k A r = (k ⧸ Ideal.span {1 - Module.rankIdempotent k A r})

noncomputable def ConicAlgebra.splitRankComponent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] (C : ConicAlgebra k A) (r : ℕ) : ConicAlgebra (SplitRankFactor k A r) (TensorProduct k (SplitRankFactor k A r) A)

The conic algebra on the rank-r factor of the rank decomposition.

Equations

• C.splitRankComponent r = ConicAlgebra.baseChangeOfProjective (ConicAlgebra.SplitRankFactor k A r) C

def ConicAlgebra.IsSplit {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] (C : ConicAlgebra k A) : Prop

GPR 21.19, general splitness. A conic algebra is split when each of its rank 1, 2, 4, and 8 components is isomorphic to the corresponding standard split composition algebra.

The composition hypothesis is included because GPR 21.19 defines splitness only for composition algebras; it also ensures through GPR 19.18 that these four idempotent factors exhaust the base.

Equations

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

theorem ConicAlgebra.IsSplit.isComposition {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} (h : C.IsSplit) : C.IsComposition

A split conic algebra is a composition algebra, by definition.