Quadratic forms of rank at least three are isotropic at almost every finite place

Let Q be a quadratic form over a number field K on a space of dimension at least three. This file proves that Q is isotropic at all but finitely many finite places of K.

Isotropic global forms are isotropic at every place, so only anisotropic, hence regular, forms need an argument. Such a form has a diagonalization ⟨a₁, …, aₙ⟩ with nonzero coefficients. At every finite place v not above 2 at which every aᵢ is a v-adic unit, the binary form ⟨a₁, a₂⟩ represents the unit -a₃ over the ring of integers of the completion K_v, a Henselian local ring with finite residue field of odd characteristic; this gives an isotropic vector of Q over K_v. The remaining places are those dividing 2 or one of the finitely many nonzero coefficients. This argument uses neither local Hasse invariants nor a rank-by-rank local classification. In rank at least five a form is even isotropic at every finite place, by the local isotropy of regular forms of rank at least five.

The rank bound is necessary: the binary form ⟨1, 1⟩ over ℚ is anisotropic at every prime congruent to 3 modulo 4. The finiteness of the anisotropic places of a form of rank at least three is what allows the weak-approximation step of the Hasse–Minkowski theorem in rank at least five, where it is applied to the complement of a binary summand.

Main results

• QuadraticForm.not_anisotropic_atFinitePlace_weightedSumSquares: a diagonal form is isotropic at every finite place at which 2 and three of its coefficients are units.
• QuadraticForm.finite_setOfPred_anisotropic_atFinitePlace: a quadratic form on a space of dimension at least three is anisotropic at only finitely many finite places.
• QuadraticForm.not_anisotropic_atFinitePlace_of_five_le_finrank: a form of rank at least five over a number field is isotropic at every finite place.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 66:1, the finiteness of the exceptional set in the case of dimension at least five.
• J.-P. Serre, A Course in Arithmetic, Chapter IV, §3.2, the proof of the Hasse–Minkowski theorem in dimension at least five.

theorem QuadraticForm.not_anisotropic_atFinitePlace_weightedSumSquares {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] (a : ι → K) {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (h2 : (IsDedekindDomain.HeightOneSpectrum.valuation K v) 2 = 1) (hi : (IsDedekindDomain.HeightOneSpectrum.valuation K v) (a i) = 1) (hj : (IsDedekindDomain.HeightOneSpectrum.valuation K v) (a j) = 1) (hk : (IsDedekindDomain.HeightOneSpectrum.valuation K v) (a k) = 1) : ¬QuadraticMap.Anisotropic (atFinitePlace (QuadraticMap.weightedSumSquares K a) v)

Isotropy at a good place. A diagonal form over a number field is isotropic at every finite place v at which 2 and three of its coefficients have valuation one.

theorem QuadraticForm.finite_setOfPred_anisotropic_atFinitePlace {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hV : 3 ≤ Module.finrank K V) : {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) | QuadraticMap.Anisotropic (Q.atFinitePlace v)}.Finite

Almost-all isotropy. A quadratic form over a number field on a space of dimension at least three is isotropic at all but finitely many finite places.

theorem QuadraticForm.not_anisotropic_atFinitePlace_of_five_le_finrank {K : Type u_1} [Field K] [NumberField K] {V : Type u_2} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hV : 5 ≤ Module.finrank K V) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ¬QuadraticMap.Anisotropic (Q.atFinitePlace v)

A quadratic form of rank at least five over a number field is isotropic at every finite place.