The rank of a composition algebra is 1, 2, 4 or 8 (GPR 19.18)

A composition algebra of constant rank over a nontrivial commutative ring is the base ring in rank 1; commutative associative with nontrivial conjugation in rank 2; associative and noncommutative in rank 4; or alternative and nonassociative in rank 8. In particular its rank is 1, 2, 4, or 8. The positive identities descend from localizations, while the negative ones are detected over a residue field.

⚠ No LG hypothesis. The tower that proves the field case runs over a field, and every field is an LG ring, so nothing here assumes IsLGRing k.

The two halves

The rank is a power of two. That is GPR 19.17 (Composition/Tower.lean): a composition algebra of dimension r > 2 is a Cayley–Dickson double of a composition subalgebra of dimension r / 2. Iterating halves the dimension until it reaches 2.

The tower stops at eight. That is the converse half of GPR 18.14(c) (Conic/CayleyDicksonAlternative.lean), and it is what the descent below is for. Reading the chain downwards from a hypothetical algebra of dimension 16:

• it is alternative — every composition algebra over a field is (GPR 19.3) — and it is a double, so its eight-dimensional half is associative (ConicAlgebra.mul_assoc_of_isAlternative_cay);
• an associative double forces its own half to be commutative (ConicAlgebra.exists_mul_mul_ne_mul_mul_cay, contrapositive), so the four-dimensional rung is commutative;
• a commutative double forces the conjugation of its half to be the identity (ConicAlgebra.exists_mul_ne_mul_cay, contrapositive), so the two-dimensional rung has conj x = x;
• but a composition algebra with trivial conjugation has dimension at most one (ConicAlgebra.IsComposition.finrank_le_one_of_conj_eq_id) — contradiction.

Only the first bullet is new; the middle two are the explicit witnesses already in Conic/CayleyDicksonAssociative.lean, used in the contrapositive direction they were built for.

The bottom of the descent

finrank_le_one_of_conj_eq_id is where the two characteristics part company. conj x = x reads 2x = t(x) · 1. When 2 ≠ 0 every element is therefore a scalar multiple of 1, and the dimension is at most one outright. When 2 = 0 it reads t(x) · 1 = 0, so t ≡ 0 because 1 ≠ 0; then n(1, y) = t(y) = 0 for every y, so 1 is a nonzero vector in the kernel of the polar form, the norm is not regular, and GPR 19.11 (Composition/RankDichotomy.lean) leaves only dimension one. The characteristic-two branch is the one that needs 19.11, and it is the reason this file depends on it.

Implementation notes

Each rung is identified with the next by ConicAlgebra.cayToAlgebra, a LinearMap that happens to be bijective and multiplicative but is not a bundled algebra map, so alternativity, associativity and commutativity are moved across by hand (isAlternative_of_injective and friends). Injectivity alone suffices in every case.

The induction runs over the carrier type as well as the dimension, since each rung is a subalgebra of the previous one and so a different type.

Main results

• ConicAlgebra.IsComposition.rankAtStalk_classification : full GPR 19.18, including the structure in each of the four ranks.
• ConicAlgebra.IsComposition.rankAtStalk_eq_one_or_two_or_four_or_eight : its rank-only part.
• ConicAlgebra.IsComposition.finrank_eq_one_or_two_or_four_or_eight : the same over a field.
• ConicAlgebra.mul_comm_of_rankAtStalk_eq_two, ConicAlgebra.mul_assoc_of_rankAtStalk_eq_two : a finitely generated projective conic algebra of constant rank two over any commutative ring is commutative and associative (GPR 16.4); no composition hypothesis is needed.
• ConicAlgebra.IsComposition.finrank_le_four_of_mul_assoc, ConicAlgebra.IsComposition.finrank_le_two_of_mul_comm, ConicAlgebra.IsComposition.finrank_le_one_of_conj_eq_id : the three steps of the descent.
• ConicAlgebra.not_isComposition_of_finrank_notMem : the contrapositive. Applied to the sixteen-dimensional double of an octonion algebra it says the sedenions are not a composition algebra (GPR 19.23).

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 16.4, 18.14(c), 19.3, 19.11, 19.17, 19.18.

Transporting multiplicative properties along an injective multiplicative map

Each rung of the Cayley–Dickson tower is identified with an algebra by a bijection that is multiplicative but is not an algebra homomorphism of any bundled kind (ConicAlgebra.cayToAlgebra is a LinearMap), so the properties have to be moved by hand. Injectivity alone suffices in every case — surjectivity is never used.

theorem isAlternative_of_injective {X : Type v} {Y : Type w} [Mul X] [Mul Y] (f : X → Y) (hf : Function.Injective f) (hmul : ∀ (p q : X), f (p * q) = f p * f q) [IsAlternative Y] : IsAlternative X

Alternativity pulls back along an injective multiplicative map.

theorem mul_assoc_of_injective {X : Type v} {Y : Type w} [Mul X] [Mul Y] (f : X → Y) (hf : Function.Injective f) (hmul : ∀ (p q : X), f (p * q) = f p * f q) (h : ∀ (a b c : Y), a * b * c = a * (b * c)) (a b c : X) : a * b * c = a * (b * c)

Associativity pulls back along an injective multiplicative map.

theorem mul_comm_of_injective {X : Type v} {Y : Type w} [Mul X] [Mul Y] (f : X → Y) (hf : Function.Injective f) (hmul : ∀ (p q : X), f (p * q) = f p * f q) (h : ∀ (a b : Y), a * b = b * a) (a b : X) : a * b = b * a

Commutativity pulls back along an injective multiplicative map.

instance NonAssocSubalgebra.isAlternative {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsAlternative A] (B : NonAssocSubalgebra k A) : IsAlternative ↥B

A unital subalgebra of an alternative algebra is alternative: both laws are checked on elements of the ambient algebra.

theorem Module.finrank_of_rankAtStalk_eq {F : Type u} [Field F] {X : Type v} [AddCommGroup X] [Module F X] {s : ℕ} (h : rankAtStalk X = fun (x : PrimeSpectrum F) => s) : finrank F X = s

Over a field, Module.rankAtStalk is the dimension.

theorem Module.rankAtStalk_eq_of_finrank_eq {F : Type u} [Field F] {X : Type v} [AddCommGroup X] [Module F X] {s : ℕ} (h : finrank F X = s) : rankAtStalk X = fun (x : PrimeSpectrum F) => s

Over a field, the dimension is Module.rankAtStalk.

instance ConicAlgebra.finite_nonAssocSubalgebra {F : Type u} {A : Type v} [Field F] [NonAssocRing A] [Module F A] [Module.Finite F A] (B : NonAssocSubalgebra F A) : Module.Finite F ↥B

Over a field a unital subalgebra of a finite-dimensional algebra is finite-dimensional. The corresponding statement for its underlying submodule is found by instance search; this moves it across ConicAlgebra.toSubmoduleEquiv, which instance search will not do on its own.

theorem ConicAlgebra.IsComposition.exists_isComposition_finrank_of_two_lt {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) {r : ℕ} (hr : Module.finrank F A = r) (h2 : 2 < r) : ∃ (B : NonAssocSubalgebra F A) (v : A) (s : ℕ), 2 * s = r ∧ Module.finrank F ↥B = s ∧ (C.restrict B).IsComposition ∧ Function.Injective ⇑(C.cayToAlgebra B v) ∧ ∀ (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

GPR 19.17 over a field, in dimensions. A composition algebra of dimension r > 2 over a field is a Cayley–Dickson double of a composition subalgebra of dimension r / 2.

This is ConicAlgebra.IsComposition.exists_bijective_cayToAlgebra with Module.rankAtStalk traded for Module.finrank — over a field the two agree — and with the subalgebra packaged as a composition algebra in its own right, which is what lets the statement be applied to it again.

The bottom of the tower: trivial conjugation forces dimension one

theorem ConicAlgebra.nontrivial_of_conicAlgebra {F : Type u} {A : Type v} [Field F] [NonAssocRing A] [Module F A] (C : ConicAlgebra F A) : Nontrivial A

A conic algebra over a nontrivial base is nonzero, because n(1) = 1.

theorem ConicAlgebra.IsComposition.finrank_le_one_of_conj_eq_id {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) (hconj : ∀ (x : A), C.conj x = x) : Module.finrank F A ≤ 1

The last step of the descent. A composition algebra over a field whose conjugation is the identity has dimension at most one.

The two characteristics are genuinely different. When 2 ≠ 0, conj x = x reads 2x = t(x) · 1, so every element is a scalar multiple of 1 outright. When 2 = 0 it reads t(x) · 1 = 0, hence t ≡ 0 since 1 ≠ 0; then n(1, y) = t(y) = 0 for every y, so 1 is a nonzero vector in the kernel of the polar form, the norm is not regular, and GPR 19.11 leaves only dimension one.

Climbing back up: commutative, then associative

theorem ConicAlgebra.IsComposition.finrank_le_two_of_mul_comm {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) (hcomm : ∀ (a b : A), a * b = b * a) : Module.finrank F A ≤ 2

A commutative composition algebra over a field has dimension at most two. If it were larger it would be a double Cay(B, μ), and a commutative double forces the conjugation of B to be the identity (ConicAlgebra.exists_mul_ne_mul_cay, contrapositive), which caps B at dimension one and so the algebra itself at dimension two.

theorem ConicAlgebra.IsComposition.finrank_le_four_of_mul_assoc {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) (hassoc : ∀ (a b c : A), a * b * c = a * (b * c)) : Module.finrank F A ≤ 4

An associative composition algebra over a field has dimension at most four. The same descent one rung higher: an associative double forces its input to be commutative (ConicAlgebra.exists_mul_mul_ne_mul_mul_cay, contrapositive), which caps the input at dimension two. This is what rules out an associative rank-eight algebra, and hence a ninth rung.

GPR 19.18 over a field

theorem ConicAlgebra.IsComposition.finrank_eq_one_or_two_or_four_or_eight {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) : Module.finrank F A = 1 ∨ Module.finrank F A = 2 ∨ Module.finrank F A = 4 ∨ Module.finrank F A = 8

GPR 19.18 over a field. A composition algebra over a field has dimension 1, 2, 4 or 8.

The tower of GPR 19.17 halves the dimension at every step, so it is a power of two; what stops it at eight is the converse half of GPR 18.14(c). A ninth rung would make the eight-dimensional one associative (ConicAlgebra.mul_assoc_of_isAlternative_cay, applied to the alternativity that every composition algebra over a field has), and ConicAlgebra.IsComposition.finrank_le_four_of_mul_assoc says no associative composition algebra gets past dimension four.

GPR 19.18 over a commutative ring

The rank is a fibrewise invariant, so the general case is the field case read off at a single residue field. In particular no LG hypothesis is needed: the tower that proves the field case runs over a field, and every field is an LG ring.

theorem ConicAlgebra.IsComposition.mul_assoc_of_isLGRing_of_rankAtStalk_eq_four {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] (h : C.IsComposition) (hLG : IsLGRing k) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (x y z : A) : x * y * z = x * (y * z)

Over an LG ring, a rank-four composition algebra is associative. It is a double of its rank-two associative commutative subalgebra, so GPR 18.14(b) applies.

theorem ConicAlgebra.eq_of_forall_localization_maximal {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (x y : A) (hxy : ∀ (P : Ideal k) [inst : P.IsMaximal], 1 ⊗ₜ[k] x = 1 ⊗ₜ[k] y) : x = y

Equality in a module can be checked after localizing at every maximal ideal, using tensor product models for the localized modules.

theorem ConicAlgebra.mul_comm_of_rankAtStalk_eq_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) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 2) (x y : A) : x * y = y * x

A finitely generated projective conic algebra of constant rank two over an arbitrary commutative ring is commutative (GPR 16.4); for composition algebras this is the positive part of GPR 19.18(b). It is checked at each localization at a maximal ideal, where the algebra is k[u] (ConicAlgebra.mul_comm_of_isLGRing_of_rankAtStalk_eq_two).

theorem ConicAlgebra.mul_assoc_of_rankAtStalk_eq_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) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 2) (x y z : A) : x * y * z = x * (y * z)

A finitely generated projective conic algebra of constant rank two over an arbitrary commutative ring is associative (GPR 16.4); for composition algebras this is the positive part of GPR 19.18(b). It is checked at each localization at a maximal ideal, where the algebra is k[u] (ConicAlgebra.mul_assoc_of_isLGRing_of_rankAtStalk_eq_two).

theorem ConicAlgebra.IsComposition.mul_assoc_of_rankAtStalk_eq_four {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.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (x y z : A) : x * y * z = x * (y * z)

A constant-rank-four composition algebra over an arbitrary commutative ring is associative. This is the positive part of GPR 19.18(c).

theorem ConicAlgebra.IsComposition.exists_conj_ne_of_rankAtStalk_eq_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] (h : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 2) : ∃ (x : A), C.conj x ≠ x

A constant-rank-two composition algebra over a nonzero ring has nontrivial conjugation.

theorem ConicAlgebra.IsComposition.not_mul_comm_of_rankAtStalk_eq_four {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] (h : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : ¬∀ (x y : A), x * y = y * x

A constant-rank-four composition algebra over a nonzero ring is not commutative.

theorem ConicAlgebra.IsComposition.not_mul_assoc_of_rankAtStalk_eq_eight {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] (h : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 8) : ¬∀ (x y z : A), x * y * z = x * (y * z)

A constant-rank-eight composition algebra over a nonzero ring is not associative.

theorem ConicAlgebra.exists_linearEquiv_map_one_map_mul_of_rankAtStalk_eq_one {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] [Nontrivial k] (C : ConicAlgebra k A) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 1) : ∃ (e : A ≃ₗ[k] k), e 1 = 1 ∧ ∀ (x y : A), e (x * y) = e x * e y

A constant-rank-one conic algebra is isomorphic, as a unital non-associative algebra, to its base ring. This is GPR 19.18(a) in the project's unbundled isomorphism convention.

theorem ConicAlgebra.IsComposition.rankAtStalk_eq_one_or_two_or_four_or_eight {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] (h : C.IsComposition) {r : ℕ} (hrank : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) : r = 1 ∨ r = 2 ∨ r = 4 ∨ r = 8

GPR 19.18. A composition algebra of constant rank over a nontrivial commutative ring has rank 1, 2, 4 or 8.

Base change to the residue field at any maximal ideal is a composition algebra over a field of the same dimension (ConicAlgebra.finrank_quotient_tensor_eq_rankAtStalk), so this is ConicAlgebra.IsComposition.finrank_eq_one_or_two_or_four_or_eight read at one point of Spec k.

theorem ConicAlgebra.IsComposition.rankAtStalk_classification {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] (h : C.IsComposition) {r : ℕ} (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) : (r = 1 ∧ ∃ (e : A ≃ₗ[k] k), e 1 = 1 ∧ ∀ (x y : A), e (x * y) = e x * e y) ∨ (r = 2 ∧ (∀ (x y : A), x * y = y * x) ∧ (∀ (x y z : A), x * y * z = x * (y * z)) ∧ ∃ (x : A), C.conj x ≠ x) ∨ (r = 4 ∧ (∀ (x y z : A), x * y * z = x * (y * z)) ∧ ¬∀ (x y : A), x * y = y * x) ∨ r = 8 ∧ IsAlternative A ∧ ¬∀ (x y z : A), x * y * z = x * (y * z)

Full GPR 19.18. Besides the rank restriction, this records the algebraic structure in each possible constant rank: rank one is the base ring; rank two is commutative associative with nontrivial conjugation; rank four is associative but not commutative; and rank eight is alternative but not associative.

theorem ConicAlgebra.not_isComposition_of_finrank_notMem {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) (h1 : Module.finrank F A ≠ 1) (h2 : Module.finrank F A ≠ 2) (h4 : Module.finrank F A ≠ 4) (h8 : Module.finrank F A ≠ 8) : ¬C.IsComposition

The dimension obstruction. A conic algebra over a field whose dimension is none of 1, 2, 4, 8 is not a composition algebra — no choice of conic norm on it permits composition.

Applied to the sixteen-dimensional double of an octonion algebra this says the sedenions are not a composition algebra (GPR 19.23), with no computation of an associator: the dimension alone rules it out.