The quaternary case of the Hasse–Minkowski theorem

Let Q be a regular quadratic form of dimension four over a number field K. This file transfers local isotropy of Q to the subforms of dimension three, and deduces the Hasse–Minkowski theorem for Q from the Hasse–Minkowski theorem for ternary forms.

If the discriminant of Q is a square, then at every place the localization of Q has square discriminant, so a form of dimension at least three represented by that localization is isotropic as soon as Q is (O'Meara 42:12). Hence a form of dimension at least three locally represented by Q, for instance the restriction of Q to a ternary subspace, is locally isotropic exactly when Q is. If moreover Q is locally isotropic, the ternary theorem makes such a subform, and hence Q, isotropic over K.

If the discriminant of Q is the class of d, then over any extension L of K containing a square root of d the scalar extension of Q has square discriminant, and it is locally isotropic when Q is, place by place through the completion tower. So every form of dimension at least three locally represented by Q ⊗ L is locally isotropic. For L = K(√d) with d a nonsquare, the square-discriminant case makes Q ⊗ L isotropic, and quaternary descent (QuadraticForm.anisotropic_baseChange_iff_quaternary) brings isotropy of Q ⊗ L back to Q.

The ternary theorem enters as a hypothesis, stated for diagonal forms.

Main results

• QuadraticForm.LocallyRepresents.isLocallyIsotropic_iff_quaternary: for Q regular quaternary of square discriminant, a form of dimension at least three locally represented by Q is locally isotropic exactly when Q is.
• QuadraticForm.LocallyRepresents.isLocallyIsotropic_of_baseChange_quaternary: for Q regular quaternary and locally isotropic, with discriminant the class of d, every form of dimension at least three locally represented by the scalar extension of Q to a number field containing a square root of d is locally isotropic.
• QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary_of_discr_eq_zero: a locally isotropic regular quaternary form of square discriminant is isotropic, given the ternary theorem over K.
• QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary: a locally isotropic regular quaternary form is isotropic, given the ternary theorem over every number field.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 42:12, 58:7 and 66:1, the case of dimension four.

theorem QuadraticForm.LocallyRepresents.isLocallyIsotropic_iff_quaternary {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [Module K W] {Q : QuadraticForm K V} {R : QuadraticForm K W} (hRQ : R.LocallyRepresents Q) (hQ : QuadraticMap.Nondegenerate) (hrank : Module.finrank K V = 4) (hdiscr : (TauCeti.formClass Q hQ).discr = 0) (hR : 3 ≤ Module.finrank K W) : R.IsLocallyIsotropic ↔ Q.IsLocallyIsotropic

Let Q be a regular quaternary form over a number field with square discriminant. A form of dimension at least three locally represented by Q is locally isotropic exactly when Q is.

theorem QuadraticForm.LocallyRepresents.isLocallyIsotropic_of_baseChange_quaternary {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {L : Type u_1} [Field L] [NumberField L] [Algebra K L] {Q : QuadraticForm K V} {W : Type u_2} [AddCommGroup W] [Module L W] {R : QuadraticForm L W} (hRQ : R.LocallyRepresents (QuadraticForm.baseChange L Q)) (hR : 3 ≤ Module.finrank L W) (hQloc : Q.IsLocallyIsotropic) (hQ : QuadraticMap.Nondegenerate) (hrank : Module.finrank K V = 4) (d : Kˣ) (hd : (TauCeti.formClass Q hQ).discr = TauCeti.squareClass d) (s : L) (hs : s * s = (algebraMap K L) ↑d) : R.IsLocallyIsotropic

Let Q be a regular quaternary form over a number field K which is isotropic at every finite and real place, and whose discriminant is the class of d. Let L be an extension of K containing a square root s of d. Then every form of dimension at least three locally represented by the scalar extension of Q to L is isotropic at every finite and real place of L.

theorem QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary_of_discr_eq_zero {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hrank : Module.finrank K V = 4) (hdiscr : (TauCeti.formClass Q hQ).discr = 0) (hloc : Q.IsLocallyIsotropic) (hternary : ∀ (p : TauCeti.RegularFormPresentation K), p.fst = 3 → (TauCeti.presentedForm p).IsLocallyIsotropic → ¬QuadraticMap.Anisotropic (TauCeti.presentedForm p)) : ¬QuadraticMap.Anisotropic Q

The quaternary case of the Hasse–Minkowski theorem, square discriminant. Let Q be a regular quaternary form over a number field K whose discriminant is a square and which is isotropic at every finite and real place. If every regular diagonal ternary form over K that is isotropic at every finite and real place is isotropic over K, then Q is isotropic over K.

theorem QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hrank : Module.finrank K V = 4) (hloc : Q.IsLocallyIsotropic) (hternary : ∀ (L : Type u) [inst : Field L] [inst_1 : NumberField L] (p : TauCeti.RegularFormPresentation L), p.fst = 3 → (TauCeti.presentedForm p).IsLocallyIsotropic → ¬QuadraticMap.Anisotropic (TauCeti.presentedForm p)) : ¬QuadraticMap.Anisotropic Q

The quaternary case of the Hasse–Minkowski theorem. Let Q be a regular quaternary form over a number field K which is isotropic at every finite and real place. If, over every number field, every regular diagonal ternary form that is isotropic at every finite and real place is isotropic, then Q is isotropic over K.

The ternary hypothesis is quantified over number fields because it is needed not only over K but also over the quadratic field K(√d), for d a nonsquare representative of the discriminant of Q.