The regular-or-rank-one dichotomy for composition algebras

This file proves the regular-or-rank-one dichotomy of GPR 19.11. Over a field, the norm of a composition algebra is regular unless the algebra has dimension one; in the exceptional case the field has characteristic two. The field result then globalizes: a constant-rank composition algebra over a commutative ring is regular unless its rank is one and 2 is not a unit.

The quadratic-form dichotomy of GPR Exercise 11.37 says that a nonregular nonsingular form has a one-dimensional polar radical and that the field has characteristic two. The extra algebraic step is to show that the whole algebra, not merely that radical, is one-dimensional. Choose a nonzero element u in the polar radical. Its norm is nonzero because the quadratic radical vanishes. Norm-associativity and right alternativity then make right multiplication by conj u surjective, so orthogonality of u forces the trace to vanish identically. Multiplicativity now forces the whole polar form to vanish, and its one-dimensional kernel is therefore the whole algebra.

Main results

• ConicAlgebra.IsComposition.isGPRRegular_or_finrank_eq_one : the field-fibre dichotomy in GPR 19.11.
• ConicAlgebra.IsComposition.isGPRRegular_of_forall_rankAtStalk_ne_one : GPR 19.11 for a composition algebra whose rank is never 1, without a constant-rank hypothesis.
• ConicAlgebra.IsComposition.isGPRRegular_or_rank_eq_one : the constant-rank ring statement.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 19.9, 19.11.

theorem ConicAlgebra.IsComposition.isGPRRegular_or_finrank_eq_one {F : Type u} {A : Type v} [Field F] [NonAssocRing A] [Module F A] [SMulCommClass F A A] [IsScalarTower F A A] [Module.Finite F A] [Module.Projective F A] {C : ConicAlgebra F A} (h : C.IsComposition) : C.norm.IsGPRRegular ∨ Module.finrank F A = 1 ∧ ringChar F = 2

The field-fibre core of GPR 19.11. A composition algebra over a field has regular norm, or it has dimension one and the field has characteristic two.

theorem ConicAlgebra.IsComposition.isGPRRegular_of_forall_rankAtStalk_ne_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] {D : ConicAlgebra k B} (h : D.IsComposition) (hrank : ∀ (p : PrimeSpectrum k), Module.rankAtStalk B p ≠ 1) : D.norm.IsGPRRegular

GPR 19.11, pointwise on Spec k. A composition algebra whose rank is different from 1 at every prime has regular norm. No constant-rank hypothesis is needed: regularity is checked after base change to each field F (QuadraticForm.isGPRRegular_of_forall_baseChangeOfProjective_isGPRRegular), and the dimension of F ⊗ A is the rank of A at the single prime under the zero ideal of F. ConicAlgebra.IsComposition.isGPRRegular_of_rankAtStalk_ne_one is the constant-rank case.

theorem ConicAlgebra.IsComposition.isGPRRegular_of_rankAtStalk_ne_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] {D : ConicAlgebra k B} (h : D.IsComposition) {r : ℕ} (hrank : Module.rankAtStalk B = fun (x : PrimeSpectrum k) => r) (hr : r ≠ 1) : D.norm.IsGPRRegular

The non-rank-one half of GPR 19.11. If a composition algebra has constant rank other than one, its norm is regular.

The field-fibre dichotomy proves regularity after every field base change. Regularity then descends by the local-global principle for the polar map (ConicAlgebra.IsComposition.isGPRRegular_of_forall_rankAtStalk_ne_one).

theorem ConicAlgebra.IsComposition.isGPRRegular_or_rank_eq_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] [Module.Finite k B] [Module.Projective k B] {D : ConicAlgebra k B} (h : D.IsComposition) {r : ℕ} (hrank : Module.rankAtStalk B = fun (x : PrimeSpectrum k) => r) : D.norm.IsGPRRegular ∨ r = 1 ∧ ¬IsUnit 2

GPR 19.11, for the project's finitely generated definition of composition algebra. If a composition algebra has constant rank r, then its norm is regular, or r = 1 and 2 is not a unit in the base ring.

The finite-generation conclusion of GPR 19.11 is already an instance hypothesis in this project's deliberately narrower ConicAlgebra.IsComposition API.

theorem ConicAlgebra.eq_unitForm_smul_one_of_rankAtStalk_eq_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [Module.Finite k B] [Module.Projective k B] (D : ConicAlgebra k B) [Nontrivial k] (hB : Module.rankAtStalk B = fun (x : PrimeSpectrum k) => 1) (x : B) : x = D.unitForm x • 1

In a constant-rank-one conic algebra, every element is its unitForm coefficient times 1.

The unit splits off a free rank-one summand. Since the whole module already has rank one, the kernel of unitForm has rank zero and is trivial. This argument remains valid in characteristic two, where the polar norm itself may be nonregular.