Rank-4 Hasse–Minkowski over ℚ

A diagonal rank-four form ⟨a₁,a₂,a₃,a₄⟩ splits as an orthogonal sum ⟨a₁,a₂⟩ ⊥ ⟨a₃,a₄⟩; over a field in which 2 is invertible we may reindex the four coordinates as two pairs. When the form is isotropic at a place v, this gives a nonzero x_v represented by both ⟨a₁,a₂⟩ and ⟨−a₃,−a₄⟩ (WP4.1). Feeding the resulting local data into Serre's existence theorem produces a single rational x with the same local behaviour, and then isotropic_of_rank_three' shows each half represents x over ℚ (WP4.2). Diagonalizing an arbitrary nondegenerate rank-four form gives the general theorem (WP4.3).

WP4.1 — local splitting of a rank-four diagonal form

The four coordinates (x₀,x₁,x₂,x₃) are regrouped as ((x₀,x₁),(x₂,x₃)), and the weighted sum of squares ⟨a₁,a₂,a₃,a₄⟩ becomes the orthogonal sum ⟨a₁,a₂⟩ ⊥ ⟨a₃,a₄⟩. Since ⟨a₃,a₄⟩ = −⟨−a₃,−a₄⟩, isotropy of the orthogonal sum and nondegeneracy of both halves produce a common nonzero value.

theorem HasseMinkowski.local_splitting {k : Type u_1} [Field k] [Invertible 2] {a₁ a₂ a₃ a₄ : k} (h₁ : a₁ ≠ 0) (h₂ : a₂ ≠ 0) (h₃ : a₃ ≠ 0) (h₄ : a₄ ≠ 0) (h : (QuadraticMap.weightedSumSquares k ![a₁, a₂, a₃, a₄]).Isotropic) : ∃ (x : k), x ≠ 0 ∧ (QuadraticMap.weightedSumSquares k ![a₁, a₂]).represents x ∧ (QuadraticMap.weightedSumSquares k ![-a₃, -a₄]).represents x

WP4.2 — diagonal rank-four Hasse–Minkowski

theorem HasseMinkowski.rankFourDiagonalHM : RankFourDiagonalHM

WP4.3 — rank-four Hasse–Minkowski for an arbitrary form

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