Reduced and split composition algebras (GPR 22.16)

The structure theorems in ranks two, four, and eight identify a reduced composition algebra with the split quadratic algebra, twisted matrices on a line bundle, or twisted Zorn matrices on a rank-three projective module. If constant-rank finite projectives over every idempotent factor are free, the latter two presentations are the standard split models. This proves the converse half of GPR 22.16; the LG-ring theorem follows because idempotent factors remain LG and their constant-rank projectives are free (GPR 11.24, GN 2.6(b)).

⚠ On "division". In this file "division algebra" is expressed by ConicAlgebra.HasTwoSidedInverses — every nonzero element has a two-sided inverse — which in general is weaker than being a division algebra in the sense of GPR 8.6. For composition algebras over a field, which are alternative, the two agree once 1 ≠ 0 (GPR 13.8, ConicAlgebra.IsComposition.isDivision_iff_hasTwoSidedInverses), and ConicAlgebra.IsComposition.isSplitOfRank_iff_not_isDivision restates the field case of GPR 22.18 with IsDivision; both are in Composition/Fields/Basic.lean.

Main results

• ConicAlgebra.isSplitOfRank_one : the rank-one case.
• ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_two : the rank-two case.
• ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_four_of_isLGRing : the rank-four case.
• ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_eight_of_isLGRing : the rank-eight case.
• ConicAlgebra.IsReduced.isSplit_of_projectiveConstantRankFree : the converse of GPR 22.16 under GPR's own hypothesis, that constant-rank finite projective k-modules are free; ConicAlgebra.IsElementaryIdempotent.ProjectiveConstantRankFree.onFactors passes the hypothesis to the idempotent factors.
• ConicAlgebra.IsReduced.isSplit_of_projective_constantRank_free_on_factors : the same under the factorwise freeness hypothesis.
• ConicAlgebra.IsReduced.isSplit_of_isLGRing : GPR 22.16, reduced implies split over an LG ring.
• ConicAlgebra.IsComposition.isSplitOfRank_iff_isGPRIsotropic_of_projectiveConstantRankFree, IsComposition.isSplitOfRank_iff_exists_isometryEquiv_dualProd_of_projectiveConstantRankFree : GPR 22.18 (i) ↔ (ii) ↔ (iii) under GPR's hypothesis, in ranks two, four, and eight.
• ConicAlgebra.IsComposition.isSplitOfRank_iff_isGPRIsotropic_of_isLGRing, ConicAlgebra.IsComposition.isSplitOfRank_iff_exists_isometryEquiv_dualProd_of_isLGRing, ConicAlgebra.IsComposition.isSplitOfRank_of_isometryEquiv_dualProd : the LG-ring case.
• ConicAlgebra.isGPRIsotropic_norm_of_isometryEquiv_dualProd : a hyperbolic norm is isotropic (GPR 22.9, (iv) ⇒ (iii)), with no hypothesis on the hyperbolic module.
• ConicAlgebra.IsComposition.isSplitOfRank_iff_not_hasTwoSidedInverses : over a field, splitness is equivalent to failure of the division property (GPR 22.18).
• ConicAlgebra.IsComposition.isSplitOfRank_iff_not_anisotropic_of_pid : over a PID, splitness is equivalent to the existence of a nonzero null vector (GPR 22.19).
• ConicAlgebra.IsComposition.isSplitOfRank_iff_not_noZeroDivisors_of_pid : over a PID, splitness is equivalent to having zero divisors (GPR 22.19).

Together with isSplitOfRank_iff_isGPRIsotropic_of_pid these are conditions (ii)–(v) of GPR 22.19. Condition (i), splitness after extension to the fraction field, is Composition/Fields/FractionField.lean.

References

• [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, Lemma 2.6(b).
• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.24, 22.16, 22.18--22.19.

theorem ConicAlgebra.isSplitOfRank_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} [Nontrivial k] (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 1) : C.IsSplitOfRank 1

A constant-rank-one conic algebra over a nontrivial ring is the standard rank-one algebra.

def ConicAlgebra.IsElementaryIdempotent.ProjectiveConstantRankFreeOnFactors (k : Type u) [CommRing k] : Prop

The factor-stable freeness hypothesis used in the converse of GPR 22.16: every finite projective module of constant rank over every idempotent factor of k is free.

Equations

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

def ConicAlgebra.IsElementaryIdempotent.ProjectiveConstantRankFree (k : Type u) [CommRing k] : Prop

GPR's freeness hypothesis in GPR 22.16–22.18: every finitely generated projective k-module of constant rank (in the universe w) is free. It holds over every LG ring (ProjectiveConstantRankFree.of_isLGRing, GPR 11.24), and its factorwise form ProjectiveConstantRankFreeOnFactors follows from it (ProjectiveConstantRankFree.onFactors).

Equations

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

theorem ConicAlgebra.IsElementaryIdempotent.ProjectiveConstantRankFree.onFactors {k : Type u} [CommRing k] (h : ProjectiveConstantRankFree k) : ProjectiveConstantRankFreeOnFactors k

GPR's freeness hypothesis implies its factorwise form: a constant-rank projective module over an idempotent factor k ⧸ (1 - e) is free, by Module.free_of_forall_free_of_isIdempotentElem.

theorem ConicAlgebra.IsElementaryIdempotent.ProjectiveConstantRankFree.of_isLGRing {k : Type u} [CommRing k] (hLG : IsLGRing k) : ProjectiveConstantRankFree k

Over an LG ring every finitely generated projective module of constant rank is free (GPR 11.24, GN 2.6(b)), so GPR's freeness hypothesis holds.

theorem ConicAlgebra.IsElementaryIdempotent.ProjectiveConstantRankFree.of_isPrincipalIdealRing {k : Type u} [CommRing k] [IsDomain k] [IsPrincipalIdealRing k] : ProjectiveConstantRankFree k

Over a PID every finitely generated projective module is free, being torsion-free, so GPR's freeness hypothesis holds; this is the freeness step of GPR 22.19.

theorem ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_two {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} {c : A} (hc : C.IsElementaryIdempotent c) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 2) : C.IsSplitOfRank 2

GPR 22.16, rank two: a reduced constant-rank-two composition algebra is split.

theorem ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_four_of_projective_constantRank_free {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} [Nontrivial k] (hc : C.IsElementaryIdempotent c) (hfree : ∀ (M : Type v) [inst : AddCommGroup M] [inst_1 : Module k M] [Module.Finite k M] [Module.Projective k M] (r : ℕ), (Module.rankAtStalk M = fun (x : PrimeSpectrum k) => r) → Module.Free k M) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : C.IsSplitOfRank 4

GPR 22.16, rank four under its abstract freeness hypothesis.

theorem ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_four_of_isLGRing {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} [Nontrivial k] (hc : C.IsElementaryIdempotent c) (hLG : IsLGRing k) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : C.IsSplitOfRank 4

GPR 22.16, rank four: over a nontrivial LG ring, a reduced constant-rank-four composition algebra is split.

theorem ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_four_of_pid {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} [IsDomain k] [IsPrincipalIdealRing k] (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : C.IsSplitOfRank 4

GPR 22.19, rank four: over a PID, a reduced constant-rank-four composition algebra is split. The twisting line is projective, hence flat and torsion-free, and a finite torsion-free module over a PID is free.

theorem ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_eight_of_projective_constantRank_free {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} [Nontrivial k] (hc : C.IsElementaryIdempotent c) (hfree : ∀ (M : Type v) [inst : AddCommGroup M] [inst_1 : Module k M] [Module.Finite k M] [Module.Projective k M] (r : ℕ), (Module.rankAtStalk M = fun (x : PrimeSpectrum k) => r) → Module.Free k M) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 8) : C.IsSplitOfRank 8

GPR 22.16, rank eight under its abstract freeness hypothesis.

theorem ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_eight_of_isLGRing {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} [Nontrivial k] (hc : C.IsElementaryIdempotent c) (hLG : IsLGRing k) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 8) : C.IsSplitOfRank 8

GPR 22.16, rank eight: over a nontrivial LG ring, a reduced constant-rank-eight composition algebra is split.

theorem ConicAlgebra.IsElementaryIdempotent.isSplitOfRank_eight_of_pid {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} [IsDomain k] [IsPrincipalIdealRing k] (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 8) : C.IsSplitOfRank 8

GPR 22.19, rank eight: over a PID, a reduced constant-rank-eight composition algebra is split. The rank-three twisting module is projective, hence finite free over the PID.

theorem ConicAlgebra.IsReduced.isSplit_of_projective_constantRank_free_on_factors {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.IsReduced) (hfree : IsElementaryIdempotent.ProjectiveConstantRankFreeOnFactors k) : C.IsSplit

Full converse of GPR 22.16, in a factor-stable formulation of its freeness hypothesis. If finite projective constant-rank modules over the idempotent factors of k are free, every reduced composition algebra over k is split. Together with IsSplit.isReduced, this gives both directions of GPR 22.16 over arbitrary commutative rings satisfying that hypothesis.

theorem ConicAlgebra.IsReduced.isSplit_of_projectiveConstantRankFree {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.IsReduced) (hfree : IsElementaryIdempotent.ProjectiveConstantRankFree k) : C.IsSplit

GPR 22.16, converse, under GPR's own hypothesis. If every finitely generated projective k-module of constant rank is free, every reduced composition algebra over k is split. The hypothesis passes to the idempotent factors of the rank decomposition (IsElementaryIdempotent.ProjectiveConstantRankFree.onFactors).

theorem ConicAlgebra.IsReduced.isSplit_of_isLGRing {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.IsReduced) (hLG : IsLGRing k) : C.IsSplit

GPR 22.16, reduced ⇒ split over an LG ring. Each rank component has constant rank by the rank decomposition. Its base is again LG because it is an idempotent factor; ranks four and eight are therefore untwisted by freeness of constant-rank projective modules.

theorem ConicAlgebra.isGPRIsotropic_norm_of_isometryEquiv_dualProd {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {M : Type u_1} [AddCommGroup M] [Module k M] (e : QuadraticMap.IsometryEquiv (QuadraticForm.dualProd k M) C.norm) : QuadraticMap.IsGPRIsotropic C.norm

A hyperbolic norm is isotropic (GPR 22.9, (iv) ⇒ (iii)). If n ≅ dualProd k M, write 1 = e₁ + e₂ across the two totally isotropic summands: the preimage (φ, m) of 1 has φ m = n(1) = 1, so m is unimodular and (0, m) is a unimodular null vector. No hypothesis on M is needed.

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_isGPRIsotropic_of_projectiveConstantRankFree {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 : ℕ} [Nontrivial k] (hfree : IsElementaryIdempotent.ProjectiveConstantRankFree k) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ QuadraticMap.IsGPRIsotropic C.norm

GPR 22.18, split ↔ isotropic, under GPR's hypothesis. If every finitely generated projective k-module of constant rank is free, a composition algebra of constant rank two, four, or eight is split exactly when its norm has a unimodular null vector. The reverse implication produces an elementary idempotent (GPR 22.9) and then untwists the reduced model with the freeness hypothesis (GPR 22.16).

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_exists_isometryEquiv_dualProd_of_projectiveConstantRankFree {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 : ℕ} [Nontrivial k] (hfree : IsElementaryIdempotent.ProjectiveConstantRankFree k) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ ∃ (M : Type (max u v)) (x : AddCommGroup M) (x_1 : Module k M) (_ : Module.Finite k M) (_ : Module.Projective k M), Nonempty (QuadraticMap.IsometryEquiv (QuadraticForm.dualProd k M) C.norm)

GPR 22.18, split ↔ hyperbolic, under GPR's hypothesis. If every finitely generated projective k-module of constant rank is free, a composition algebra of constant rank two, four, or eight is split exactly when its norm is hyperbolic, i.e. isometric to QuadraticForm.dualProd k M for a finitely generated projective M. Forwards, an elementary idempotent gives the Peirce presentation peirceHyperbolicIsometryEquiv (GPR 22.9, (i) ⇒ (iv)); backwards, a hyperbolic norm is isotropic (isGPRIsotropic_norm_of_isometryEquiv_dualProd).

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_exists_isometryEquiv_dualProd_of_isLGRing {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 : ℕ} [Nontrivial k] (hcomp : C.IsComposition) (hLG : IsLGRing k) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ ∃ (M : Type (max u v)) (x : AddCommGroup M) (x_1 : Module k M) (_ : Module.Finite k M) (_ : Module.Projective k M), Nonempty (QuadraticMap.IsometryEquiv (QuadraticForm.dualProd k M) C.norm)

GPR 22.18, split ↔ hyperbolic over an LG ring: the case of isSplitOfRank_iff_exists_isometryEquiv_dualProd_of_projectiveConstantRankFree where the freeness hypothesis is GPR 11.24.

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_isGPRIsotropic_of_isLGRing {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 : ℕ} [Nontrivial k] (hcomp : C.IsComposition) (hLG : IsLGRing k) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ QuadraticMap.IsGPRIsotropic C.norm

GPR 22.18, split ↔ isotropic over an LG ring. For a constant-rank composition algebra of rank two, four, or eight, splitness is equivalent to the existence of a unimodular null vector. The forward implication transports the elementary idempotent of the standard model; the reverse implication uses GPR 22.9 and the reduced classification of GPR 22.16.

theorem ConicAlgebra.IsComposition.isSplitOfRank_of_isometryEquiv_dualProd {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 : ℕ} [Nontrivial k] (hcomp : C.IsComposition) (hLG : IsLGRing k) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) {M : Type u_1} [AddCommGroup M] [Module k M] (e : QuadraticMap.IsometryEquiv (QuadraticForm.dualProd k M) C.norm) : C.IsSplitOfRank r

GPR 22.18, hyperbolic ⇒ split over an LG ring. A norm isometric to a hyperbolic form QuadraticForm.dualProd k M is isotropic (isGPRIsotropic_norm_of_isometryEquiv_dualProd), with no hypothesis on M; the split/isotropic equivalence finishes the argument.

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_not_hasTwoSidedInverses {r : ℕ} {K : Type u} [Field K] {B : Type v} [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} (hcomp : D.IsComposition) (hB : Module.rankAtStalk B = fun (x : PrimeSpectrum K) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : D.IsSplitOfRank r ↔ ¬D.HasTwoSidedInverses

GPR 22.18, split ↔ not division over a field. For a constant-rank composition algebra of rank two, four, or eight, splitness is equivalent to the failure of the property that every nonzero element has a two-sided inverse.

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_isGPRIsotropic_of_pid {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 : ℕ} [IsDomain k] [IsPrincipalIdealRing k] (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ QuadraticMap.IsGPRIsotropic C.norm

GPR 22.19, split ↔ GPR-isotropic over a PID. For a constant-rank composition algebra of rank two, four, or eight, a unimodular null vector is equivalent to splitness. Projective twisting modules are free over the PID, replacing the LG-ring freeness step in GPR 22.18.

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_not_anisotropic_of_pid {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 : ℕ} [IsDomain k] [IsPrincipalIdealRing k] (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ ¬QuadraticMap.Anisotropic C.norm

GPR 22.19, split ↔ a nonzero null vector over a PID. This is where GPR's unimodular-vector isotropy and mathlib's failure of anisotropy become equivalent, by GPR Exc. 12.38(c) (QuadraticMap.isGPRIsotropic_iff_not_anisotropic_of_pid).

theorem ConicAlgebra.IsComposition.isSplitOfRank_iff_not_noZeroDivisors_of_pid {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 : ℕ} [IsDomain k] [IsPrincipalIdealRing k] (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r = 2 ∨ r = 4 ∨ r = 8) : C.IsSplitOfRank r ↔ ¬NoZeroDivisors A

GPR 22.19, split ↔ zero divisors over a PID. Here "has zero divisors" is expressed canonically as the negation of mathlib's NoZeroDivisors predicate.