Layer 2c of the Hasse–Minkowski development: the Hasse–Minkowski invariant

Over a field k whose Hilbert symbol is the one attached to a number field, every nondegenerate quadratic form is isometric to a diagonal form w₀ X₀² + ⋯ + w_{n-1} X_{n-1}² with nonzero structure constants. The Hasse–Minkowski invariant of such a diagonal form is the product of all the pairwise Hilbert symbols

ε(w) = ∏_{i < j} (wᵢ, wⱼ)_k.

This file defines hasseMinkowskiInvAux on the diagonal data and proves the elementary evaluations of the invariant. These are exactly the statements of Serre's Cours d'arithmétique, Ch. IV, together with the small-rank computations used in the classification.

Main definitions

• hasseMinkowskiInvAux w: the invariant of the diagonal form with weights w : Fin n → kˣ.

Main results

• hasseMinkowskiInvAux_zero, hasseMinkowskiInvAux_one, hasseMinkowskiInvAux_two, hasseMinkowskiInvAux_three: the invariant in ranks 0 through 3.
• hasseMinkowskiInvAux_cons: prepending a rank-one weight multiplies the invariant by the product of the Hilbert symbols of the new weight against the old ones.
• hasseMinkowskiInvAux_prod_rank_one: with a bilinear Hilbert symbol, the same product collapses to a single Hilbert symbol with the product (discriminant) of the old weights.
• hasseMinkowskiInvAux_eq_one_or_neg_one: the invariant is 1 or -1.

Omitted

The well-definedness of the invariant, i.e. the statement that equivalent diagonal forms have the same invariant (hasseMinkowskiInvAux.eq_of_equivalent in the reference development), is not stated here: it depends on the theory of Hilbert symbols over local fields that is not yet available in this project. A form-level invariant hasseMinkowskiInv is therefore kept as a private definition that no theorem or consumer exposes. As a consequence the computational lemmas at the level of hasseMinkowskiInv (which all pass through well-definedness) are also omitted. In particular the reference development's hasseMinkowskiInv.weightedSumSquares, …_two, …_three, hasseMinkowskiInv.prod_rank_one and hasseMinkowskiInv.of_baseChange_weightedSumSquares are not reproduced: without eq_of_equivalent there is no way to identify the diagonalization chosen by Classical.choose with any concrete list of weights. The diagonal-level statements (hasseMinkowskiInvAux_*) proved here are exactly the part of the development that does not need that machinery.

The invariant of a diagonal form

noncomputable def HasseMinkowski.hasseMinkowskiInvAux {k : Type u_1} [Field k] {n : ℕ} (w : Fin n → kˣ) : ℤ

The Hasse–Minkowski invariant of the diagonal form with nonzero weights w : Fin n → kˣ, namely the product ∏_{i < j} (wᵢ, wⱼ)_k of the Hilbert symbols of all pairs of weights.

Equations

• HasseMinkowski.hasseMinkowskiInvAux w = ∏ p : Fin n × Fin n with p.1 < p.2, HasseMinkowski.hilbertSym ↑(w p.1) ↑(w p.2)

theorem HasseMinkowski.hasseMinkowskiInvAux_def {k : Type u_1} [Field k] {n : ℕ} (w : Fin n → kˣ) : hasseMinkowskiInvAux w = ∏ p : Fin n × Fin n with p.1 < p.2, hilbertSym ↑(w p.1) ↑(w p.2)

theorem HasseMinkowski.hasseMinkowskiInvAux_zero {k : Type u_1} [Field k] (w : Fin 0 → kˣ) : hasseMinkowskiInvAux w = 1

theorem HasseMinkowski.hasseMinkowskiInvAux_one {k : Type u_1} [Field k] (w : Fin 1 → kˣ) : hasseMinkowskiInvAux w = 1

theorem HasseMinkowski.hasseMinkowskiInvAux_two {k : Type u_1} [Field k] (w : Fin 2 → kˣ) : hasseMinkowskiInvAux w = hilbertSym ↑(w 0) ↑(w 1)

theorem HasseMinkowski.hasseMinkowskiInvAux_three {k : Type u_1} [Field k] (w : Fin 3 → kˣ) : hasseMinkowskiInvAux w = hilbertSym ↑(w 0) ↑(w 1) * hilbertSym ↑(w 0) ↑(w 2) * hilbertSym ↑(w 1) ↑(w 2)

The invariant only takes the values 1 and -1

theorem HasseMinkowski.hilbertSym_eq_one_or_neg_one_of_ne_zero {k : Type u_1} [Field k] {a b : k} (ha : a ≠ 0) (hb : b ≠ 0) : hilbertSym a b = 1 ∨ hilbertSym a b = -1

theorem HasseMinkowski.hasseMinkowskiInvAux_eq_one_or_neg_one {k : Type u_1} [Field k] {n : ℕ} (w : Fin n → kˣ) : hasseMinkowskiInvAux w = 1 ∨ hasseMinkowskiInvAux w = -1

Splitting off a rank-one factor

theorem HasseMinkowski.hasseMinkowskiInvAux_cons {k : Type u_1} [Field k] {n : ℕ} (a : kˣ) (w : Fin n → kˣ) : hasseMinkowskiInvAux (Fin.cons a w) = (∏ i : Fin n, hilbertSym ↑a ↑(w i)) * hasseMinkowskiInvAux w

theorem HasseMinkowski.hasseMinkowskiInvAux_prod_rank_one {k : Type u_1} [Field k] [HasBilinHilbertSym k] {n : ℕ} (a : kˣ) (w : Fin n → kˣ) : hasseMinkowskiInvAux (Fin.cons a w) = hilbertSym (↑a) (∏ i : Fin n, ↑(w i)) * hasseMinkowskiInvAux w

The invariant of a nondegenerate form