Rank-three Hasse–Minkowski over `ℚ` (Legendre descent) #

This file reduces the rank-three Hasse–Minkowski principle over ℚ to a single, clearly isolated local–global statement about the Hilbert symbol, the Hasse norm theorem for quadratic extensions. Writing σ = -wq 2 * wq 0 and τ = -wq 2 * wq 1 for the two Hilbert-symbol arguments that the ternary criterion produces, the argument is:

diagonalize a nondegenerate rank-three form as ⟨w₀, w₁, w₂⟩ with wᵢ : ℚˣ (equivalent_weightedSumSquares_units_of_nondegenerate');
the rank-three isotropy criterion weightedSumSquares_isotropic_iff_hilbertSym_eq_one identifies isotropy of ⟨w₀, w₁, w₂⟩ with (σ, τ)_ℚ = 1;
base-changing the local isotropy data produces (σ, τ)_v = 1 at every place v (the finite places ℚ_[p] and the archimedean place ℝ);
the local–global statement HilbertSymLocalGlobal then yields (σ, τ)_ℚ = 1.

Step 4, HilbertSymLocalGlobal, is the Hasse norm theorem for quadratic extensions of ℚ (equivalently, Hasse–Minkowski for the conic z² = σ x² + τ y²); it is the rank-three local–global principle and is proved by elementary Legendre descent in HasseMinkowski/Legendre.lean (hilbertSymLocalGlobal), which also derives the unconditional isotropic_of_rank_three'. It is kept here as an explicit hypothesis so the reduction below is independent of the descent proof. Every declaration below is sorry-free.

Main results #

HilbertSymLocalGlobal: the missing local–global input.
isotropic_of_rank_three: the rank-three case, conditional on HilbertSymLocalGlobal.

The isolated local–global input for the Hilbert symbol #

source

def HasseMinkowski.HilbertSymLocalGlobal :

Prop

Legendre's theorem. A global Hilbert symbol (A, B)_ℚ is trivial as soon as its base changes (A, B)_v are trivial at every place v of ℚ (every prime p and the archimedean place ℝ).

This is the Hasse norm theorem for the quadratic extension ℚ(√B) (or √A) and the rank-three local–global principle; it is proved by elementary descent (CRT plus the norm criterion) in HasseMinkowski/Legendre.lean (hilbertSymLocalGlobal). It is kept as a def/Prop here so that the rank-three reduction does not depend on that proof.

Equations

One or more equations did not get rendered due to their size.

Instances For

Reindexing `Fin 3` weights #

The rank-three theorem #

source

theorem HasseMinkowski.isotropic_of_rank_three {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] (hloc : HilbertSymLocalGlobal) (Q : QuadraticForm ℚ V) (hr : Module.finrank ℚ V = 3) (hQ : QuadraticMap.Nondegenerate) (hQ' : EverywhereLocallyIsotropic Q) :

Isotropic Q

C.0 assessment: why the product-formula route is circular #

Under the hypotheses of HilbertSymLocalGlobal every local factor (A,B)_v is already 1, so the product formula hilbertReciprocity reduces to the tautology 1 * 1 = 1 and carries no information about the global symbol (A,B)_ℚ (see hilbertProd_eq_one_of_local_eq_one). The target is instead exactly the rank-three local–global principle for the diagonal ternary form ⟨-A,-B,1⟩, i.e. Legendre's theorem / the Hasse norm theorem for quadratic extensions of ℚ; the equivalence hilbertSymLocalGlobal_iff_rankThreeDiagonal below pins this down precisely. That principle is now proved by Legendre descent in HasseMinkowski/Legendre.lean; it is recorded here as a hypothesis so that this file does not depend on that proof.

source

def HasseMinkowski.RankThreeDiagonalLocalGlobal :

Prop

The rank-three local–global principle for diagonal ternary forms of the shape ⟨-A,-B,1⟩ over ℚ (equivalently, solvability of the conic z² = A x² + B y²): local isotropy over every completion implies global isotropy. This is Legendre's theorem.

Equations