Composition algebras over a field: the classification mechanism (GPR 23.12)

Over a field the general theory of the previous layers collapses to two statements, and every classification result in this layer is one of them applied to a field whose quadratic forms are understood.

Splitting is isotropy. A composition algebra of dimension 2, 4, or 8 over a field is split exactly when its norm has a nonzero null vector, equivalently exactly when it is not a division algebra (GPR 22.18). Over a field the two isotropy notions of the literature agree (QuadraticMap.isGPRIsotropic_iff_not_anisotropic), so no unimodularity bookkeeping survives.

The norm is a complete invariant. Two composition algebras over a field with isometric norm forms are isomorphic; this is Layer 9 applied with isLGRing_of_field.

Together these reduce classification over a particular field to two questions about quadratic forms over that field: which forms of dimension 2, 4, 8 are isotropic, and which anisotropic ones occur as norms.

⚠ On "division". Each division statement below comes in two forms: one with ConicAlgebra.HasTwoSidedInverses — every nonzero element has a two-sided inverse — and one with IsDivision, division in the sense of GPR 8.6. In general the first is weaker, but composition algebras are alternative, so the two agree once 1 ≠ 0 (GPR 13.8, ConicAlgebra.IsComposition.isDivision_iff_hasTwoSidedInverses), proved in this file); the IsDivision forms are derived from the others by that equivalence.

Main results

• ConicAlgebra.IsComposition.isSplitOfRank_iff_not_anisotropic : GPR 22.18 over a field, in dimensions.
• ConicAlgebra.IsComposition.isSplitOfRank_of_forall_not_anisotropic : the u-invariant mechanism — if all forms of the relevant dimension over K are isotropic, every composition algebra of that dimension is split.
• ConicAlgebra.IsComposition.isSplitOfRank_or_isDivision, ConicAlgebra.IsComposition.isSplitOfRank_or_hasTwoSidedInverses : the dichotomy — over a field a composition algebra of dimension 2, 4, or 8 is split or a division algebra, never both.
• ConicAlgebra.IsComposition.isSplitOfRank_iff_not_isDivision : GPR 22.18 over a field, with division in the sense of GPR 8.6.
• ConicAlgebra.IsComposition.isDivision_iff_hasTwoSidedInverses : GPR 13.8 for composition algebras over a field.
• ConicAlgebra.mul_assoc_of_finrank_eq_two, ConicAlgebra.mul_comm_of_finrank_eq_two : a two-dimensional conic algebra over a field is an associative commutative algebra (GPR 16.4).
• ConicAlgebra.IsSplitOfRank.isomorphic : the split algebra of a given dimension is unique.
• ConicAlgebra.IsComposition.isomorphic_of_isometryEquiv : composition algebras over a field with isometric norms are isomorphic (Layer 9 over a field).
• ConicAlgebra.IsComposition.isomorphic_iff_nonempty_isometryEquiv : the two previous results combined — isomorphism and norm isometry are the same relation over a field.

Implementation notes

The results of Layers 9 and 10 are stated with Module.rankAtStalk, which over a field is Module.finrank (Module.rankAtStalk_eq_of_finrank_eq). This file performs that translation once so that the field-specific files can speak about dimensions throughout.

⚠ Dimension one is excluded from the splitting criterion, not overlooked: the rank-one algebra is the base field, it is split and a division algebra at once, and its norm x ↦ x² is anisotropic. GPR 22.18 states the equivalence for dimensions greater than one for exactly this reason.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 8.6, 13.8, 16.4, 19.3, 19.18, 22.18, 23.12.

Splitting is isotropy

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_not_anisotropic {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ ¬QuadraticMap.Anisotropic C.norm

GPR 22.18 over a field. A composition algebra of dimension 2, 4, or 8 over a field is split if and only if its norm has a nonzero null vector.

This is the constant-rank equivalence over an LG ring, with Module.rankAtStalk traded for Module.finrank and GPR's unimodular isotropy traded for mathlib's failure of anisotropy — the two agree over a field.

theorem ConicAlgebra.IsComposition.isSplitOfRank_of_exists_ne_zero_norm_eq_zero {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) {x : A} (hx : x ≠ 0) (hnx : C.norm x = 0) : C.IsSplitOfRank r

GPR 22.18 over a field, in the form used by every classification below: a nonzero null vector splits a composition algebra of dimension 2, 4, or 8.

theorem ConicAlgebra.IsComposition.isSplitOfRank_of_forall_not_anisotropic {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) (hiso : ∀ (V : Type v) [inst : AddCommGroup V] [inst_1 : Module K V], Module.finrank K V = r → ∀ (q : QuadraticForm K V), ¬QuadraticMap.Anisotropic q) : C.IsSplitOfRank r

The u-invariant mechanism. If every quadratic form on a K-space of dimension r is isotropic, then every composition algebra of dimension r ∈ {2, 4, 8} over K is split.

This is how every "large enough dimension" classification in this layer is applied: over a finite field the hypothesis holds for r ≥ 3 (Chevalley–Warning, QuadraticForm.not_anisotropic_of_two_lt_finrank), and over a local field it holds for r ≥ 5, which covers the octonion case r = 8.

theorem ConicAlgebra.IsComposition.isSplitOfRank_or_hasTwoSidedInverses {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ∨ C.HasTwoSidedInverses

The dichotomy of GPR 22.18. Over a field a composition algebra of dimension 2, 4, or 8 is either split or a division algebra.

theorem ConicAlgebra.IsComposition.not_hasTwoSidedInverses_of_isSplitOfRank {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) (hs : C.IsSplitOfRank r) : ¬C.HasTwoSidedInverses

The dichotomy of GPR 22.18 is exclusive. A split composition algebra of dimension 2, 4, or 8 is not a division algebra.

Division in the sense of GPR 8.6

The theorems above are stated with ConicAlgebra.HasTwoSidedInverses. For a composition algebra over a field that is GPR's division property: composition algebras are alternative (GPR 19.3), so GPR 13.8 applies. The statements below are the same theorems with GPR's IsDivision.

theorem ConicAlgebra.IsComposition.isDivision_iff_hasTwoSidedInverses {K : Type u} {A : Type v} [Field 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} [Nontrivial A] (h : C.IsComposition) : IsDivision A ↔ C.HasTwoSidedInverses

GPR 13.8 for composition algebras over a field. A nonzero composition algebra is a division algebra in the sense of GPR 8.6 exactly when every nonzero element has a two-sided inverse, since composition algebras are alternative (ConicAlgebra.IsComposition.isAlternative).

theorem ConicAlgebra.IsComposition.isSplitOfRank_or_isDivision {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ∨ IsDivision A

The dichotomy of GPR 22.18, with GPR 8.6's division. Over a field a composition algebra of dimension 2, 4, or 8 is either split or a division algebra.

theorem ConicAlgebra.IsComposition.not_isDivision_of_isSplitOfRank {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) (hs : C.IsSplitOfRank r) : ¬IsDivision A

A split composition algebra of dimension 2, 4, or 8 is not a division algebra in the sense of GPR 8.6.

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_not_isDivision {K : Type u} {A : Type v} [Field 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 : ℕ} (h : C.IsComposition) (hA : Module.finrank K A = r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ ¬IsDivision A

GPR 22.18 over a field, with GPR 8.6's division: a composition algebra of dimension 2, 4, or 8 is split exactly when it is not a division algebra.

Algebras of dimension two are commutative and associative

theorem ConicAlgebra.mul_assoc_of_finrank_eq_two {K : Type u} {A : Type v} [Field 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) (hA : Module.finrank K A = 2) (x y z : A) : x * y * z = x * (y * z)

GPR 16.4 in dimension two. A two-dimensional conic algebra over a field is associative: it is generated by one element (ConicAlgebra.mul_assoc_of_isLGRing_of_rankAtStalk_eq_two).

theorem ConicAlgebra.mul_comm_of_finrank_eq_two {K : Type u} {A : Type v} [Field 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) (hA : Module.finrank K A = 2) (x y : A) : x * y = y * x

GPR 16.4 in dimension two. A two-dimensional conic algebra over a field is commutative: it is generated by one element (ConicAlgebra.mul_comm_of_isLGRing_of_rankAtStalk_eq_two).

The norm is a complete invariant

theorem ConicAlgebra.IsSplitOfRank.isomorphic {K : Type u} {A : Type v} {B : Type w} [Field K] [NonAssocRing A] [Module K A] [NonAssocRing B] [Module K B] {C : ConicAlgebra K A} {D : ConicAlgebra K B} {r : ℕ} (hC : C.IsSplitOfRank r) (hD : D.IsSplitOfRank r) (hr : r = 1 ∨ r = 2 ∨ r = 4 ∨ r = 8) : C.Isomorphic D

Uniqueness of the split algebra. Two conic algebras split of the same dimension are isomorphic, because both are isomorphic to the same standard model of GPR 21.19.

theorem ConicAlgebra.IsComposition.isomorphic_of_isometryEquiv {K : Type u} {A : Type v} {B : Type w} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] [Module.Finite K A] [Module.Projective K A] [NonAssocRing B] [Module K B] [SMulCommClass K B B] [IsScalarTower K B B] [Module.Finite K B] [Module.Projective K B] {C : ConicAlgebra K A} {D : ConicAlgebra K B} (hC : C.IsComposition) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) : C.Isomorphic D

Layer 9 over a field. Composition algebras over a field whose norm forms are isometric are isomorphic. This is the converse direction of the norm classification, specialized by passing isLGRing_of_field; no dimension hypothesis is needed because the isometry transports the dimension.

theorem ConicAlgebra.IsComposition.isomorphic_iff_nonempty_isometryEquiv {K : Type u} {A : Type v} {B : Type w} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] [Module.Finite K A] [Module.Projective K A] [NonAssocRing B] [Module K B] [SMulCommClass K B B] [IsScalarTower K B B] [Module.Finite K B] [Module.Projective K B] {C : ConicAlgebra K A} {D : ConicAlgebra K B} (hC : C.IsComposition) (hD : D.IsComposition) : C.Isomorphic D ↔ Nonempty (QuadraticMap.IsometryEquiv C.norm D.norm)

Layer 9 over a field, both directions. Over a field, two composition algebras are isomorphic exactly when their norm forms are isometric. The easy direction holds over any commutative ring; the converse is the matched-doubling argument of Layer 9.

theorem ConicAlgebra.IsComposition.isSplitOfRank_of_isometryEquiv {K : Type u} {A : Type v} {B : Type w} [Field K] [NonAssocRing A] [Module K A] [SMulCommClass K A A] [IsScalarTower K A A] [Module.Finite K A] [Module.Projective K A] [NonAssocRing B] [Module K B] [SMulCommClass K B B] [IsScalarTower K B B] [Module.Finite K B] [Module.Projective K B] {C : ConicAlgebra K A} {D : ConicAlgebra K B} {r : ℕ} (hC : C.IsComposition) (hD : D.IsComposition) (e : QuadraticMap.IsometryEquiv C.norm D.norm) (hD' : D.IsSplitOfRank r) (hr : r = 1 ∨ r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r

A composition algebra over a field whose norm is isometric to that of a split algebra of dimension 1, 2, 4, or 8 is itself split of that dimension.