GPR 19.16(b): rank greater than one gives a separable quadratic subalgebra

A composition algebra A of rank at least two contains an element u whose discriminant t(u)² - 4n(u) is a unit. By GPR 19.8 (Composition/QuadraticSubalgebra.lean) the subalgebra k[u] = k·1 + k·u is then free of rank two with regular norm — a separable quadratic subalgebra — which is where the Cayley–Dickson tower of GPR 19.17 starts.

Starting the tower at a rank-two subalgebra rather than at k·1 is not a convenience: in characteristic 2 the norm ⟨1⟩ of k·1 is non-singular but not regular, and ConicAlgebra.IsComposition.cay needs a regular input (Composition/CayleyDickson.lean). The content of this file is exactly that the obstruction can always be avoided.

The field case is proved first and is the whole mathematical content; the passage to an LG ring is the usual one, and reuses the machinery of the representation lemma (QuadraticForm/Representation.lean) verbatim.

Main results

• ConicAlgebra.IsComposition.exists_isUnit_elementDiscriminant : over a field.
• ConicAlgebra.IsComposition.exists_isRegularRankTwoComposition : the same, packaged as GPR 19.8(i) — a regular rank-two composition subalgebra.
• ConicAlgebra.discriminantForm : u ↦ t(u)² - 4n(u) as a quadratic form, so that GPR 11.8 can turn it into a polynomial and the LG axiom can be applied to it.
• ConicAlgebra.IsComposition.exists_isUnit_elementDiscriminant_of_isLGRing, ConicAlgebra.IsComposition.exists_isRegularRankTwoComposition_of_isLGRing, ConicAlgebra.IsComposition.exists_isRegularRankTwoComposition_of_rankAtStalk : GPR 19.16(b) over an LG ring, with the rank hypothesis stated at the residue fields (the form the proof consumes) and in terms of Module.rankAtStalk (the form callers will have).

Implementation notes

The two characteristics need different arguments over a field, and the characteristic-2 one is the reason the statement is about the discriminant rather than about the trace.

• 2 ≠ 0. If every discriminant vanishes then n vanishes on ker t, hence so does the polar form (ker t is a subspace, and polar n u 1 = t(u)), so ker t lies in the radical of n. Over a field the radical of a composition norm vanishes (ConicAlgebra.IsComposition.isGPRNondegenerate), so t is injective and the dimension is at most one.

• 2 = 0. Here t(u)² - 4n(u) = t(u)², so the hypothesis says exactly that the trace vanishes identically, and no information about n is available over the base field: t ≡ 0 is consistent with a nonzero radical-free norm (GPR 19.4, the purely inseparable example, is a conic algebra of this shape). The argument therefore moves to the algebraic closure — legitimate precisely because non-singularity is stable under base change (ConicAlgebra.IsComposition.baseChangeOfProjective), which is what that stability is for. There, two steps: the polar form vanishes identically (ConicAlgebra.IsMultiplicative.polar_eq_zero_of_trace_eq_zero, a short consequence of the second linearization of multiplicativity), and then every element x equals d • 1 for d a square root of n(x), because x + d • 1 lies in the radical. So the dimension is at most one there too, and dimension does not change under base change.

Note that the characteristic-2 argument uses no alternativity and no regularity beyond the vanishing of the radical over the algebraic closure; in particular it does not go through GPR 19.3.

Over an LG ring the discriminant is fed to the LG axiom as a polynomial. A need not be free, so — exactly as in QuadraticForm.exists_isUnit_apply_of_hasFullSupport — the discriminant form is pulled back along a presentation kⁿ ↠ A, where GPR 11.8 applies. The residue-field hypothesis of the axiom is discharged by the field case, since the base change of a composition algebra is a composition algebra (Composition/BaseChange.lean) and the rank is unchanged. Note that the representation lemma itself is not used: the discriminant form is not non-singular, so it is the LG axiom and not GPR 11.26 that does the work.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 19.8, 19.16(b).

theorem ConicAlgebra.finrank_le_one_of_forall_exists_smul {K : Type u_1} [Field K] {M : Type u_2} [AddCommGroup M] [Module K M] (a : M) (h : ∀ (x : M), ∃ (d : K), x = d • a) : Module.finrank K M ≤ 1

A module spanned by a single element has dimension at most one. Used both here and in Composition/Fields/SepClosed.lean, to produce an element outside K · 1.

theorem ConicAlgebra.IsMultiplicative.polar_eq_zero_of_trace_eq_zero {F : Type u} {A : Type v} [Field F] [NonAssocRing A] [Module F A] {C : ConicAlgebra F A} (h : C.IsMultiplicative) (h2 : 2 = 0) (ht : ∀ (x : A), C.trace x = 0) (x y : A) : QuadraticMap.polar (⇑C.norm) x y = 0

In characteristic 2 a traceless multiplicative conic norm has zero polar form.

Specialize the second linearization n(xz, yw) + n(xw, yz) = n(x, y) n(z, w) at z = x, w = y. The degree-two identity turns x² and y² into multiples of 1, so the first term is a multiple of n(1, 1) = t(1) = 0; the linearized degree-two identity turns yx into n(x, y)·1 + xy, so the second term is a combination of t(xy) = 0 and n(xy, xy) = 2n(xy) = 0. What is left is n(x, y)² = 0.

Neither alternativity nor regularity is used, and the hypothesis is on the trace, not on the algebra.

theorem ConicAlgebra.IsMultiplicative.exists_eq_smul_one_of_isAlgClosed {F : Type u} {A : Type v} [Field F] [NonAssocRing A] [Module F A] {C : ConicAlgebra F A} [IsAlgClosed F] (h : C.IsMultiplicative) (h2 : 2 = 0) (ht : ∀ (x : A), C.trace x = 0) (hrad : QuadraticMap.radical C.norm = ⊥) (x : A) : ∃ (d : F), x = d • 1

Over an algebraically closed field of characteristic 2, a traceless multiplicative conic algebra with vanishing radical is spanned by 1.

Every x has n(x) = d² for some d, and then n(x + d • 1) = n(x) + d² = 2n(x) = 0 while the polar form vanishes identically by ConicAlgebra.IsMultiplicative.polar_eq_zero_of_trace_eq_zero; so x + d • 1 lies in the radical, which is zero.

theorem ConicAlgebra.IsComposition.exists_isUnit_elementDiscriminant {F : Type u} {A : Type v} [Field F] [NonAssocRing A] [Module F A] [SMulCommClass F A A] [IsScalarTower F A A] {C : ConicAlgebra F A} [Module.Finite F A] [Module.Projective F A] (h : C.IsComposition) (hrank : 1 < Module.finrank F A) : ∃ (u : A), IsUnit (C.elementDiscriminant u)

The field case of GPR 19.16(b). A composition algebra of dimension at least two over a field contains an element of nonzero — hence invertible — discriminant, so by GPR 19.8 it contains a separable quadratic subalgebra.

The two characteristics are genuinely different arguments; see the module docstring.

theorem ConicAlgebra.IsComposition.exists_isRegularRankTwoComposition {F : Type u} {A : Type v} [Field F] [NonAssocRing A] [Module F A] [SMulCommClass F A A] [IsScalarTower F A A] {C : ConicAlgebra F A} [Module.Finite F A] [Module.Projective F A] (h : C.IsComposition) (hrank : 1 < Module.finrank F A) : ∃ (u : A), C.IsRegularRankTwoComposition u

The field case of GPR 19.16(b), packaged. A composition algebra of dimension at least two over a field contains a regular rank-two composition subalgebra k[u] (GPR 19.8(i)).

Globalization over an LG ring

def ConicAlgebra.discriminantForm {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) : QuadraticForm k A

The element discriminant t(u)² - 4n(u) of GPR 19.8, as a quadratic form on A.

The trace is linear and the norm is quadratic, so this is quadratic; packaging it as a QuadraticForm is what lets GPR 11.8 turn it into a polynomial and hence hand it to the LG axiom.

Equations

• C.discriminantForm = QuadraticMap.sq.comp C.trace - 4 • C.norm

@[simp]

theorem ConicAlgebra.discriminantForm_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) : C.discriminantForm u = C.elementDiscriminant u

theorem ConicAlgebra.discriminantForm_baseChangeOfProjective {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) (S : Type w) [CommRing S] [Algebra k S] : (baseChangeOfProjective S C).discriminantForm = QuadraticForm.baseChangeOfProjective S C.discriminantForm

The discriminant form commutes with base change: on 1 ⊗ₜ a both sides are the image of t(a)² - 4n(a), and a quadratic form on a base changed module is determined by those values.

theorem ConicAlgebra.finrank_quotient_tensor_eq_rankAtStalk {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] (𝔪 : Ideal k) [𝔪.IsMaximal] : Module.finrank (k ⧸ 𝔪) (TensorProduct k (k ⧸ 𝔪) A) = Module.rankAtStalk A { asIdeal := 𝔪, isPrime := ⋯ }

The dimension of the fibre (k ⧸ 𝔪) ⊗ A is mathlib's Module.rankAtStalk at 𝔪.

The two differ only in which model of the residue field they use: rankAtStalk goes through Ideal.ResidueField, the residue field of the localization, whereas the LG axiom speaks about k ⧸ 𝔪. For 𝔪 maximal these agree, and base change along the comparison map does not change the rank.

theorem ConicAlgebra.IsComposition.exists_isUnit_elementDiscriminant_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} (hLG : IsLGRing k) (h : C.IsComposition) (hrank : ∀ (𝔪 : Ideal k) [𝔪.IsMaximal], 1 < Module.finrank (k ⧸ 𝔪) (TensorProduct k (k ⧸ 𝔪) A)) : ∃ (u : A), IsUnit (C.elementDiscriminant u)

GPR 19.16(b). Over an LG ring, a composition algebra whose rank exceeds one at every residue field contains an element of invertible discriminant.

This is where the LG axiom is applied, and the shape is that of the representation lemma (QuadraticForm/Representation.lean): A need not be free, so pull the discriminant form back along a presentation kⁿ ↠ A, where GPR 11.8 writes it as a polynomial. Over each residue field the base changed algebra is again a composition algebra (ConicAlgebra.IsComposition.baseChangeOfProjective) of dimension at least two, so exists_isUnit_elementDiscriminant supplies the required unit value there, and π ⊗ κ stays surjective so the witness lifts to the free module. The LG axiom then descends a witness to k.

theorem ConicAlgebra.IsComposition.exists_isRegularRankTwoComposition_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} (hLG : IsLGRing k) (h : C.IsComposition) (hrank : ∀ (𝔪 : Ideal k) [𝔪.IsMaximal], 1 < Module.finrank (k ⧸ 𝔪) (TensorProduct k (k ⧸ 𝔪) A)) : ∃ (u : A), C.IsRegularRankTwoComposition u

GPR 19.16(b), packaged. Over an LG ring, a composition algebra of rank greater than one contains a regular rank-two composition subalgebra k[u] — the subalgebra the Cayley–Dickson tower starts from.

theorem ConicAlgebra.IsComposition.exists_isRegularRankTwoComposition_of_rankAtStalk {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} (hLG : IsLGRing k) (h : C.IsComposition) (hrank : ∀ (𝔭 : PrimeSpectrum k), 1 < Module.rankAtStalk A 𝔭) : ∃ (u : A), C.IsRegularRankTwoComposition u

GPR 19.16(b), in the project's standard rank language. Over an LG ring, a composition algebra of rank greater than one everywhere on Spec k contains a regular rank-two composition subalgebra. This is the form the Cayley–Dickson tower of GPR 19.17 will consume, where the rank is constant and greater than one.