The Cayley–Dickson tower exhausts a composition algebra (GPR 19.17)

Over an LG ring, a composition algebra C of constant rank r > 1 is obtained from a rank-two composition algebra by iterated Cayley–Dickson doubling. At every noninitial rung there are a unital subalgebra B with regular restricted norm, of constant rank r / 2, and a v ⊥ B with n(v) ∈ kˣ, such that

Cay(B, -n(v)) → C, u + wj ↦ u + wv,

is bijective, unital, multiplicative and an isometry. B is then again a composition algebra, of half the rank, so the statement applies to it in turn and the whole tower descends to the rank-two subalgebra of GPR 19.16(b). If 2 is a unit, the rank-one scalar subalgebra may be used as the initial rung instead. These are the two clauses of GPR 19.17.

The three ingredients, and where each comes from

1. Start (GPR 19.16(b), Composition/RankTwoSubalgebra.lean): rank > 1 produces a regular rank-two subalgebra k[u]. The tower starts here and not at k · 1, whose restricted norm ⟨1⟩ is regular only when 2 ∈ kˣ; under that extra hypothesis the tower starts at k.
2. Step (GPR 19.16(a), Composition/Doubling.lean): a regular subalgebra whose orthogonal complement has full support is doubled inside C.
3. Regularity of the new rung (GPR 19.11, Composition/RankDichotomy.lean): the image is a composition algebra of constant rank 2s, and 2s ≠ 1 because it is even, so its norm is regular and step 2 applies again. Without this the induction could not feed its own output back in — regularity of q₁ ⊥ q₂ does not follow from regularity of q₁, only non-singularity does (GN (C.8.3)).

The rank bookkeeping

This is what the file supplies, and it is what "C is exhausted" turns into:

• ConicAlgebra.rankAtStalk_cay : the rank doubles, pointwise on Spec k — the projective version of ConicAlgebra.Cay.finrank_cay, which needs a basis.
• ConicAlgebra.rankAtStalk_add_polarOrthogonal : a regular subalgebra is a direct summand, so rk C = rk B + rk Bᗮ. Its two consequences are the two ends of the induction — ConicAlgebra.rankAtStalk_le_of_isGPRRegular bounds each rung by r, so doubling terminates, and ConicAlgebra.mem_of_isGPRRegular_of_rankAtStalk_eq says a regular subalgebra of full rank is everything, which is what turns the last doubling into a surjection.
• ConicAlgebra.hasFullSupport_polarOrthogonal_of_rankAtStalk_lt : constant rank s < r gives the full-support hypothesis that GPR 19.16(a) consumes, via Module.finrank_baseChange_of_rankAtStalk_eq.

⚠ [Nontrivial k] is a genuine hypothesis of the induction, not decoration: over the zero ring Spec k is empty, every rank statement is vacuous, and the bound 2s ≤ r that makes the tower terminate cannot be read off from any prime. (The conclusion still holds there, since every module is trivial, but by a different argument.)

⚠ The subalgebra produced at each step is the image of ConicAlgebra.cayToAlgebra, packaged existentially by ConicAlgebra.exists_subalgebra_equiv_cay rather than as a definition: its closure under multiplication needs the orthogonality and invertibility hypotheses, and overview §2 keeps hypotheses off definitions.

Main results

• ConicAlgebra.IsComposition.rank_eq_two_or_exists_bijective_cayToAlgebra : the full rank-> 1 clause of GPR 19.17, with rank two as the initial rung.
• ConicAlgebra.IsComposition.exists_bijective_cayToAlgebra_of_invertible_two : the clause of GPR 19.17 starting the tower at the base ring when 2 is invertible.
• ConicAlgebra.IsComposition.exists_bijective_cayToAlgebra : the noninitial doubling step.
• ConicAlgebra.IsComposition.exists_isGPRRegular_rankAtStalk_two_mul : one rung of the tower.
• ConicAlgebra.exists_subalgebra_equiv_cay : the image B + Bv as a unital subalgebra.
• ConicAlgebra.isGPRRegular_restrict_and_rankAtStalk_of_equiv_cay : every internal doubled image of a regular constant-rank subalgebra is regular and has twice the rank.
• ConicAlgebra.mem_of_isGPRRegular_of_rankAtStalk_eq : the exhaustion criterion.
• ConicAlgebra.rankAtStalk_cay, ConicAlgebra.rankAtStalk_add_polarOrthogonal : the rank bookkeeping.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 19.11, 19.16, 19.17.
• [GN] Gille, Neher, Group schemes over LG-rings…, European J. Math. 11 (2025), art. 42, C.8.3.

theorem Module.finrank_baseChange_of_rankAtStalk_eq {k : Type u} [CommRing k] {M : Type v} [AddCommGroup M] [Module k M] [Module.Finite k M] [Projective k M] {r : ℕ} (hr : rankAtStalk M = fun (x : PrimeSpectrum k) => r) (F : Type u) [Field F] [Algebra k F] : finrank F (TensorProduct k F M) = r

Constant rank is dimension after base change to any field. Module.rankAtStalk is computed at primes of k; base change to a field F ∈ k-alg reads it off at the prime ⊥ of F, where the module is free.

def ConicAlgebra.toSubmoduleEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (B : NonAssocSubalgebra k A) : ↥B.toSubmodule ≃ₗ[k] ↥B

A unital subalgebra and its underlying submodule are the same module. The two coercions are definitionally equal but not syntactically so, and Module.rankAtStalk statements have to be moved between them: the orthogonal-complement API is stated for submodules, the conic API for subalgebras.

Equations

• ConicAlgebra.toSubmoduleEquiv B = { toFun := fun (x : ↥B.toSubmodule) => ⟨↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : ↥B) => ⟨↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem ConicAlgebra.rankAtStalk_toSubmodule {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (B : NonAssocSubalgebra k A) : Module.rankAtStalk ↥B.toSubmodule = Module.rankAtStalk ↥B

Module.rankAtStalk does not see the difference between a subalgebra and its submodule.

theorem ConicAlgebra.hasFullSupport_polarOrthogonal_of_rankAtStalk_lt {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (hreg : (C.restrict B).norm.IsGPRRegular) {r s : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hB : Module.rankAtStalk ↥B.toSubmodule = fun (x : PrimeSpectrum k) => s) (hlt : s < r) : Module.HasFullSupport k ↥(C.norm.polarOrthogonal B.toSubmodule)

The rank criterion for properness. A regular subalgebra whose constant rank is smaller than the constant rank of the ambient algebra has a complement of full support, which is the hypothesis GPR 19.16(a) consumes.

The image of the doubling map as a subalgebra

theorem ConicAlgebra.exists_subalgebra_equiv_cay {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} {B : NonAssocSubalgebra k A} {v : A} [IsAlternative A] (hBv : ∀ b ∈ B, QuadraticMap.polar (⇑C.norm) b v = 0) (hu : IsUnit (C.norm v)) (hinj : Function.Injective ⇑(C.cayToAlgebra B v)) : ∃ (D : NonAssocSubalgebra k A) (e : (C.restrict B).Cay (-C.norm v) ≃ₗ[k] ↥D), ∀ (p : (C.restrict B).Cay (-C.norm v)), ↑(e p) = (C.cayToAlgebra B v) p

B + Bv is a unital subalgebra, isomorphic to Cay(B, -n(v)).

The image of ConicAlgebra.cayToAlgebra is closed under multiplication precisely because that map is multiplicative (GPR 18.1), and it contains 1 because the map is unital. Packaged with the linear equivalence onto it, which is what carries the norm, the rank and the composition structure across.

Existential rather than a definition: the subalgebra structure needs the orthogonality and invertibility hypotheses, and overview §2 keeps hypotheses off definitions.

The rank doubles

ConicAlgebra.Cay.finrank_cay says this for free modules; the tower needs it pointwise on Spec k, since that is the form in which the rank of a subalgebra is controlled.

theorem ConicAlgebra.rankAtStalk_cay {k : Type u} [CommRing k] {B' : Type v} [NonAssocRing B'] [Module k B'] [Module.Finite k B'] [Module.Projective k B'] (C' : ConicAlgebra k B') (μ : k) : Module.rankAtStalk (C'.Cay μ) = 2 * Module.rankAtStalk B'

The rank of the double is twice the rank. The pointwise form of ConicAlgebra.Cay.finrank_cay, with no freeness hypothesis.

theorem ConicAlgebra.isGPRRegular_restrict_and_rankAtStalk_of_equiv_cay {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} {B : NonAssocSubalgebra k A} {v : A} (h : C.IsComposition) (hreg : (C.restrict B).norm.IsGPRRegular) (hBv : ∀ b ∈ B, QuadraticMap.polar (⇑C.norm) b v = 0) (hu : IsUnit (C.norm v)) (D : NonAssocSubalgebra k A) (e : (C.restrict B).Cay (-C.norm v) ≃ₗ[k] ↥D) (he : ∀ (p : (C.restrict B).Cay (-C.norm v)), ↑(e p) = (C.cayToAlgebra B v) p) {s : ℕ} (hB : Module.rankAtStalk ↥B.toSubmodule = fun (x : PrimeSpectrum k) => s) : (C.restrict D).norm.IsGPRRegular ∧ Module.rankAtStalk ↥D.toSubmodule = fun (x : PrimeSpectrum k) => 2 * s

Regularity and rank of an internal doubled image. Suppose D is the image of the internal doubling map on a regular subalgebra B of constant rank s. Then the restricted norm on D is regular and D has constant rank 2s.

The norm pulled back to the external double is the Cayley–Dickson norm. It is non-singular by GN (C.8.3), so the image is a composition algebra; its even rank then rules out the exceptional rank-one case in GPR 19.11.

A regular subalgebra of full rank is everything

theorem ConicAlgebra.rankAtStalk_add_polarOrthogonal {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (hreg : (C.restrict B).norm.IsGPRRegular) : Module.rankAtStalk A = Module.rankAtStalk ↥B.toSubmodule + Module.rankAtStalk ↥(C.norm.polarOrthogonal B.toSubmodule)

The ranks add up. A subalgebra with regular restricted norm is a direct summand — that is QuadraticForm.orthogonalDecomposition — so its rank and the rank of its orthogonal complement add up to the rank of the ambient algebra, pointwise on Spec k.

theorem ConicAlgebra.rankAtStalk_le_of_isGPRRegular {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (hreg : (C.restrict B).norm.IsGPRRegular) (p : PrimeSpectrum k) : Module.rankAtStalk (↥B.toSubmodule) p ≤ Module.rankAtStalk A p

A subalgebra with regular restricted norm has rank at most that of the ambient algebra. This is what bounds the tower: each rung doubles the rank, and no rung can outgrow C.

theorem ConicAlgebra.mem_of_isGPRRegular_of_rankAtStalk_eq {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {B : NonAssocSubalgebra k A} (hreg : (C.restrict B).norm.IsGPRRegular) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hB : Module.rankAtStalk ↥B.toSubmodule = fun (x : PrimeSpectrum k) => r) (x : A) : x ∈ B

The exhaustion criterion. A subalgebra whose restricted norm is regular is a direct summand, so if its rank agrees with the rank of the ambient algebra everywhere on Spec k, the complement has rank zero and hence vanishes: the subalgebra is the whole algebra.

This is the rank bookkeeping that turns "C is exhausted" into a statement about Bᗮ.

One rung of the tower

theorem ConicAlgebra.IsComposition.exists_isGPRRegular_rankAtStalk_two_mul {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} {B : NonAssocSubalgebra k A} (hLG : IsLGRing k) (h : C.IsComposition) (hreg : (C.restrict B).norm.IsGPRRegular) {r s : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hB : Module.rankAtStalk ↥B.toSubmodule = fun (x : PrimeSpectrum k) => s) (hlt : s < r) : ∃ (D : NonAssocSubalgebra k A) (v : A), IsUnit (C.norm v) ∧ (∀ b ∈ B, QuadraticMap.polar (⇑C.norm) b v = 0) ∧ (C.restrict D).norm.IsGPRRegular ∧ (Module.rankAtStalk ↥D.toSubmodule = fun (x : PrimeSpectrum k) => 2 * s) ∧ (2 * s = r → Function.Bijective ⇑(C.cayToAlgebra B v))

The doubling step. Over an LG ring, a regular subalgebra of a composition algebra whose constant rank s is smaller than the constant rank r of the ambient algebra is contained in a regular subalgebra of constant rank 2s — the image of Cay(B, -n(v)) — and when 2s = r that image is the whole algebra.

Regularity of the new subalgebra is not proved from regularity of the doubled quadratic form, which would need q₁ ⊥ q₂ regular from q₁ regular. It comes from GPR 19.11 (ConicAlgebra.IsComposition.isGPRRegular_of_rankAtStalk_ne_one): the image is a composition algebra of constant rank 2s, and 2s ≠ 1 because it is even. This is the step that GPR 19.11 unblocks, and it is what lets the induction feed its own output back in.

Iterating: GPR 19.17

theorem ConicAlgebra.IsComposition.exists_bijective_cayToAlgebra {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} [Nontrivial k] (hLG : IsLGRing k) (h : C.IsComposition) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : 2 < r) : ∃ (B : NonAssocSubalgebra k A) (v : A) (s : ℕ), 2 * s = r ∧ (Module.rankAtStalk ↥B.toSubmodule = fun (x : PrimeSpectrum k) => s) ∧ IsUnit (C.norm v) ∧ (C.restrict B).norm.IsGPRRegular ∧ Function.Bijective ⇑(C.cayToAlgebra B v) ∧ (C.cayToAlgebra B v) 1 = 1 ∧ (∀ (p q : (C.restrict B).Cay (-C.norm v)), (C.cayToAlgebra B v) (p * q) = (C.cayToAlgebra B v) p * (C.cayToAlgebra B v) q) ∧ ∀ (p : (C.restrict B).Cay (-C.norm v)), C.norm ((C.cayToAlgebra B v) p) = ((C.restrict B).cay (-C.norm v)).norm p

GPR 19.17: a composition algebra of rank greater than two arises by the Cayley–Dickson process. Over an LG ring, a composition algebra of constant rank r > 2 is the double of one of its own subalgebras: there are a subalgebra B with regular restricted norm and a v ∈ Bᗮ with n(v) ∈ kˣ for which

Cay(B, -n(v)) → C, u + wj ↦ u + wv,

is bijective. It is automatically unital, multiplicative and an isometry (ConicAlgebra.cayToAlgebra_one, ConicAlgebra.cayToAlgebra_mul, ConicAlgebra.norm_cayToAlgebra), so C is Cay(B, -n(v)). Since B is again a composition algebra — of half the rank, by ConicAlgebra.rankAtStalk_cay — iterating the statement descends the whole tower.

The tower starts at the rank-two subalgebra of GPR 19.16(b) and not at k · 1, whose restricted norm ⟨1⟩ is regular only when 2 ∈ kˣ. That is why the hypothesis is 2 < r rather than 1 < r: rank two is the base case of the process, not a step in it.

theorem ConicAlgebra.IsComposition.rank_eq_two_or_exists_bijective_cayToAlgebra {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} [Nontrivial k] (hLG : IsLGRing k) (h : C.IsComposition) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : 1 < r) : r = 2 ∨ ∃ (B : NonAssocSubalgebra k A) (v : A) (s : ℕ), 2 * s = r ∧ (Module.rankAtStalk ↥B.toSubmodule = fun (x : PrimeSpectrum k) => s) ∧ IsUnit (C.norm v) ∧ (C.restrict B).norm.IsGPRRegular ∧ Function.Bijective ⇑(C.cayToAlgebra B v) ∧ (C.cayToAlgebra B v) 1 = 1 ∧ (∀ (p q : (C.restrict B).Cay (-C.norm v)), (C.cayToAlgebra B v) (p * q) = (C.cayToAlgebra B v) p * (C.cayToAlgebra B v) q) ∧ ∀ (p : (C.restrict B).Cay (-C.norm v)), C.norm ((C.cayToAlgebra B v) p) = ((C.restrict B).cay (-C.norm v)).norm p

Full GPR 19.17, starting in rank two. A composition algebra of constant rank greater than one over an LG ring is either already of rank two, or is a Cayley–Dickson double of a regular composition subalgebra of half its rank. Reapplying the second alternative to that subalgebra gives the finite tower starting in rank two asserted by the corollary.

noncomputable def ConicAlgebra.scalarAdjoinZeroLinearEquiv {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) : k ≃ₗ[k] ↥(C.adjoinElement 0)

The scalar subalgebra k · 1 = k[0], as a free rank-one module.

Equations

• C.scalarAdjoinZeroLinearEquiv = { toFun := fun (r : k) => ⟨r • 1, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : ↥(C.adjoinElement 0)) => C.unitForm ↑x, left_inv := ⋯, right_inv := ⋯ }

theorem ConicAlgebra.IsComposition.exists_bijective_cayToAlgebra_of_invertible_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} [Nontrivial k] [Invertible 2] (hLG : IsLGRing k) (h : C.IsComposition) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : 1 < r) : ∃ (B : NonAssocSubalgebra k A) (v : A) (s : ℕ), 2 * s = r ∧ (Module.rankAtStalk ↥B.toSubmodule = fun (x : PrimeSpectrum k) => s) ∧ IsUnit (C.norm v) ∧ (C.restrict B).norm.IsGPRRegular ∧ Function.Bijective ⇑(C.cayToAlgebra B v)

The second clause of GPR 19.17. If 2 is invertible, the Cayley–Dickson tower may be started at the base ring itself. The scalar subalgebra has rank one and its norm is the regular form ⟨1⟩; the same doubling induction as above then reaches the ambient algebra.