The Hasse–Minkowski induction step in rank at least five

Let Q be a regular quadratic form over a number field K of rank n ≥ 5 which is isotropic at every finite and real place. This file shows that Q is isotropic over K as soon as every locally isotropic regular form of rank n - 1 is isotropic over K. Together with the cases of rank two, three and four, this is the inductive structure of the Hasse–Minkowski theorem.

Main results

• QuadraticForm.not_anisotropic_prod_of_isLocallyIsotropic: if U ⊥ W is locally isotropic, with U regular on a nonzero space and W regular of rank at least three, and every locally isotropic form ⟨c⟩ ⊥ W is isotropic over K, then U ⊥ W is isotropic over K.
• QuadraticForm.not_anisotropic_of_isLocallyIsotropic_of_five_le_finrank: the induction step from rank n - 1 to rank n ≥ 5, with the induction hypothesis stated for diagonal forms.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1973), 66:1, the case of dimension at least five.
• J.-P. Serre, A Course in Arithmetic, Chapter IV, §3.2, Theorem 8, the case n ≥ 5.

theorem QuadraticForm.not_anisotropic_prod_of_isLocallyIsotropic {K : Type u_1} [Field K] [NumberField K] {X : Type u_2} {Y : Type u_3} [AddCommGroup X] [Module K X] [AddCommGroup Y] [Module K Y] [FiniteDimensional K X] [FiniteDimensional K Y] [Nontrivial X] {U : QuadraticForm K X} {W : QuadraticForm K Y} (hU : QuadraticMap.Nondegenerate) (hW : QuadraticMap.Nondegenerate) (hY : 3 ≤ Module.finrank K Y) (hUW : IsLocallyIsotropic (QuadraticMap.prod U W)) (ih : ∀ (c : K), c ≠ 0 → IsLocallyIsotropic ((c • QuadraticMap.sq).prod W) → ¬((c • QuadraticMap.sq).prod W).Anisotropic) : ¬(QuadraticMap.prod U W).Anisotropic

Let U be a regular quadratic form on a nonzero space and W a regular quadratic form of rank at least three over a number field, such that U ⊥ W is isotropic at every finite and real place. If every form ⟨c⟩ ⊥ W with c ≠ 0 that is isotropic at every finite and real place is isotropic over K, then U ⊥ W is isotropic over K.

theorem QuadraticForm.not_anisotropic_of_isLocallyIsotropic_of_five_le_finrank {K : Type u_1} [Field K] [NumberField K] {X : Type u_2} [AddCommGroup X] [Module K X] [FiniteDimensional K X] {Q : QuadraticForm K X} (hQ : QuadraticMap.Nondegenerate) (hX : 5 ≤ Module.finrank K X) (hloc : Q.IsLocallyIsotropic) (ih : ∀ (p : TauCeti.RegularFormPresentation K), p.fst + 1 = Module.finrank K X → (TauCeti.presentedForm p).IsLocallyIsotropic → ¬QuadraticMap.Anisotropic (TauCeti.presentedForm p)) : ¬QuadraticMap.Anisotropic Q

The Hasse–Minkowski induction step in rank at least five. Let Q be a regular quadratic form of rank n ≥ 5 over a number field that is isotropic at every finite and real place. If every diagonal regular form of rank n - 1 that is isotropic at every finite and real place is isotropic over K, then Q is isotropic over K.