Layer 2b of the Hasse–Minkowski development: ranks one and two

This file proves the Hasse–Minkowski principle in ranks one and two: a quadratic form over ℚ that becomes isotropic over every completion of ℚ is already isotropic over ℚ. Both proofs are direct adaptations of the classical arguments.

• Rank one. In dimension one a nonzero quadratic form is anisotropic over any field, so real isotropy forces the base-changed form to be zero; evaluating at 1 ⊗ m shows the original form vanishes on every vector.
• Rank two. By equivalent_weightedSumSquares_units_of_nondegenerate' a nondegenerate form is isometric to a weighted sum of squares w₀ y₀² + w₁ y₁² with nonzero rational weights. Real isotropy makes the ratio -w₀⁻¹ w₁ nonnegative, while each p-adic completion gives it an even p-adic valuation; the square criterion isSquare_of_nonneg_of_even_padicValRat then produces the isotropic vector ![x, 1].

Main results

• isotropic_of_rank_one, isotropic_of_rank_two.
• QuadraticMap.Equivalent.represents_iff: equivalent forms represent the same values.

Representation transfers along isometries

theorem QuadraticMap.Equivalent.represents_iff {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : Equivalent Q₁ Q₂) (a : R) : HasseMinkowski.represents Q₁ a ↔ HasseMinkowski.represents Q₂ a

Rank one

theorem HasseMinkowski.isotropic_of_rank_one {V : Type u_1} [AddCommGroup V] [Module ℚ V] (Q : QuadraticForm ℚ V) (hr : Module.finrank ℚ V = 1) (hQ' : EverywhereLocallyIsotropic Q) : Isotropic Q

Rank two

theorem HasseMinkowski.isotropic_of_rank_two {V : Type u_1} [AddCommGroup V] [Module ℚ V] [Module.Finite ℚ V] (Q : QuadraticForm ℚ V) (hr : Module.finrank ℚ V = 2) (hQ : QuadraticMap.Nondegenerate) (hQ' : EverywhereLocallyIsotropic Q) : Isotropic Q