Local Hilbert symbols at the completions of ℚ

This file collects the place-by-place facts about the Hilbert symbol (·,·)_k for k = ℚ_[p] (and, later, ℝ). The first item is the bilinearity of the symbol in its first argument, HasBilinHilbertSym ℚ_[p], which makes the generic rank criteria of RankCriteria.lean available at every p-adic place.

The two-adic case is imported from HilbertSymbol/Two.lean; for odd p the result is hilbertSym_padic_odd_mul_left.

Bilinearity of the p-adic Hilbert symbol

instance HasseMinkowski.instHasBilinHilbertSymPadic (p : ℕ) [Fact (Nat.Prime p)] : HasBilinHilbertSym ℚ_[p]

The Hilbert symbol on the p-adic numbers is bilinear in its first argument.

For p = 2 this is instHasBilinHilbertSym from HilbertSymbol/Two.lean; for odd p it is hilbertSym_padic_odd_mul_left.

The rank-two representation criterion

theorem HasseMinkowski.weightedSumSquares_two_represents_iff_ternary {k : Type u_1} [Field k] {a b x : k} [Invertible 2] (ha : a ≠ 0) (hb : b ≠ 0) (hx : x ≠ 0) : (QuadraticMap.weightedSumSquares k ![a, b]).represents x ↔ (QuadraticMap.weightedSumSquares k ![a, b, -x]).Isotropic

A nonzero vector of the plane ⟨a, b⟩ represents x exactly when the ternary form ⟨a, b, -x⟩ is isotropic.

This is the bridge between representability by a rank-two form and the ternary isotropy criterion of RankCriteria.lean. The hard case is when the isotropic vector of ⟨a, b, -x⟩ has last coordinate 0: then ⟨a, b⟩ is itself isotropic, and since it is nondegenerate it represents every value.

theorem HasseMinkowski.represents_weightedSumSquares_two_iff {k : Type u_1} [Field k] {a b x : k} [HasBilinHilbertSym k] [Invertible 2] (ha : a ≠ 0) (hb : b ≠ 0) (hx : x ≠ 0) : (QuadraticMap.weightedSumSquares k ![a, b]).represents x ↔ hilbertSym x (-(a * b)) = hilbertSym a b

Nontriviality of x ↦ (x, c) for a nonsquare c

For a nonsquare c ≠ 0 the character x ↦ (x, c)_k is nontrivial. Over ℝ this is immediate from hilbertSym_real_eq; over ℚ_[p] it is read off Serre's closed formulas, using the decomposition c = p ^ α · u.

theorem HasseMinkowski.exists_hilbertSym_eq_neg_one_real {c : ℝ} (hc : c < 0) : ∃ (x : ℝ), x ≠ 0 ∧ hilbertSym x c = -1

Nontriviality of the local Hilbert symbol character

theorem HasseMinkowski.exists_hilbertSym_eq_neg_one_padic (p : ℕ) [Fact (Nat.Prime p)] {c : ℚ_[p]} (hc : c ≠ 0) (hcsq : ¬IsSquare c) : ∃ (x : ℚ_[p]), x ≠ 0 ∧ hilbertSym x c = -1

Two prescribed Hilbert symbols (WP2.4) and the pair of non-squares (WP2.5)

theorem HasseMinkowski.exists_not_isSquare_and_not_isSquare_mul (p : ℕ) [Fact (Nat.Prime p)] {c : ℚ_[p]} (hc : c ≠ 0) : ∃ (c₂ : ℚ_[p]), ¬IsSquare c₂ ∧ ¬IsSquare (c * c₂)

theorem HasseMinkowski.exists_hilbertSym_two_prescribed {k : Type u_1} [Field k] [HasBilinHilbertSym k] {c₁ c₂ : k} (h1 : c₁ ≠ 0) (h2 : c₂ ≠ 0) (hc1 : ¬IsSquare c₁) (hc2 : ¬IsSquare c₂) (hc12 : ¬IsSquare (c₁ * c₂)) (hnd : ∀ (c : k), c ≠ 0 → ¬IsSquare c → ∃ (x : k), x ≠ 0 ∧ hilbertSym x c = -1) {e₁ e₂ : ℤ} (he1 : e₁ = 1 ∨ e₁ = -1) (he2 : e₂ = 1 ∨ e₂ = -1) : ∃ (x : k), x ≠ 0 ∧ hilbertSym x c₁ = e₁ ∧ hilbertSym x c₂ = e₂

Rank-3 representation and the five-variable isotropy theorem (WP2.6)

theorem HasseMinkowski.isotropic_weightedSumSquares_five (p : ℕ) [Fact (Nat.Prime p)] (w : Fin 5 → ℚ_[p]) (hw : ∀ (i : Fin 5), w i ≠ 0) : (QuadraticMap.weightedSumSquares ℚ_[p] w).Isotropic

theorem HasseMinkowski.isotropic_weightedSumSquares_of_five_le {ι : Type u_1} [Fintype ι] (p : ℕ) [Fact (Nat.Prime p)] {w : ι → ℚ_[p]} (hw : ∀ (i : ι), w i ≠ 0) (h : 5 ≤ Fintype.card ι) : (QuadraticMap.weightedSumSquares ℚ_[p] w).Isotropic