def HilbertSymbol.IsSolvable (F : Type u_1) [Field F] (a b : Fˣ) : Prop

The equation $ax^2 + by^2 = 1$ has a solution $(x, y) \in F^2$.

def HilbertSymbol.RepresentsZero (F : Type u_1) [Field F] (a b : Fˣ) : Prop

The quadratic form $z^2 - ax^2 - by^2$ represents zero non-trivially over $F$, i.e., $z^2 = ax^2 + by^2$ has a solution with $(x, y, z) \neq (0, 0, 0)$.

def HilbertSymbol.IsNormFromSqrtExt (F : Type u_1) [Field F] (a b : Fˣ) : Prop

The unit $a \in F^\times$ is a norm from the quadratic extension $F(\sqrt{b})$, i.e., there exist $z, y \in F$ with $z^2 - b y^2 = a$.

def HilbertSymbol.HasPrimitiveSolution {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : Prop

The equation $ax^2 + by^2 = z^2$ admits a primitive $p$-adic integer solution, i.e., one with $x, y, z \in \mathbb{Z}_p$ where at least one of them is a unit.

noncomputable def hilbertSymbol (F : Type u_1) [Field F] (a b : Fˣ) : ℤ

The Hilbert symbol $(a, b)_F \in \{\pm 1\}$ for units of a field $F$: takes the value $1$ if $ax^2 + by^2 = 1$ has a solution in $F$, and $-1$ otherwise. This is Definition 10.1 of the textbook (in its general form for a field $F$).

@[simp]

theorem hilbertSymbol.eq_one_iff {F : Type u_2} [Field F] {a b : Fˣ} : hilbertSymbol F a b = 1 ↔ HilbertSymbol.IsSolvable F a b

$(a, b)_F = 1$ iff the equation $ax^2 + by^2 = 1$ is solvable in $F$.

theorem hilbertSymbol.eq_neg_one_iff {F : Type u_2} [Field F] {a b : Fˣ} : hilbertSymbol F a b = -1 ↔ ¬HilbertSymbol.IsSolvable F a b

$(a, b)_F = -1$ iff the equation $ax^2 + by^2 = 1$ is unsolvable in $F$.

theorem hilbertSymbol.eq_one_or_neg_one {F : Type u_2} [Field F] (a b : Fˣ) : hilbertSymbol F a b = 1 ∨ hilbertSymbol F a b = -1

The Hilbert symbol always takes the value $\pm 1$.

theorem hilbertSymbol.sq {F : Type u_2} [Field F] (a b : Fˣ) : hilbertSymbol F a b ^ 2 = 1

$(a, b)_F^2 = 1$ since the Hilbert symbol is $\pm 1$.

theorem hilbertSymbol.ne_zero {F : Type u_2} [Field F] (a b : Fˣ) : hilbertSymbol F a b ≠ 0

The Hilbert symbol is never zero.

noncomputable def padicHilbertSymbol (p : ℕ) [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : ℤ

The $p$-adic Hilbert symbol $(a, b)_p$, defined as the Hilbert symbol over the $p$-adic numbers $\mathbb{Q}_p$.

@[simp]

theorem padicHilbertSymbol.eq_one_iff {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} : padicHilbertSymbol p a b = 1 ↔ ∃ (x : ℚ_[p]) (y : ℚ_[p]), ↑a * x ^ 2 + ↑b * y ^ 2 = 1

$(a, b)_p = 1$ iff the equation $ax^2 + by^2 = 1$ is solvable in $\mathbb{Q}_p$.

theorem padicHilbertSymbol.eq_neg_one_iff {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} : padicHilbertSymbol p a b = -1 ↔ ¬∃ (x : ℚ_[p]) (y : ℚ_[p]), ↑a * x ^ 2 + ↑b * y ^ 2 = 1

$(a, b)_p = -1$ iff the equation $ax^2 + by^2 = 1$ is unsolvable in $\mathbb{Q}_p$.

theorem padicHilbertSymbol.eq_one_or_neg_one {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : padicHilbertSymbol p a b = 1 ∨ padicHilbertSymbol p a b = -1

The $p$-adic Hilbert symbol takes values in $\{\pm 1\}$.

theorem padicHilbertSymbol.sq {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : padicHilbertSymbol p a b ^ 2 = 1

$(a, b)_p^2 = 1$.

theorem padicHilbertSymbol.ne_zero {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : padicHilbertSymbol p a b ≠ 0

The $p$-adic Hilbert symbol is never zero.

noncomputable def realHilbertSymbol (a b : ℝˣ) : ℤ

The real Hilbert symbol $(a, b)_\infty$, defined as the Hilbert symbol over $\mathbb{R}$.

@[simp]

theorem realHilbertSymbol.eq_one_iff {a b : ℝˣ} : realHilbertSymbol a b = 1 ↔ ∃ (x : ℝ) (y : ℝ), ↑a * x ^ 2 + ↑b * y ^ 2 = 1

$(a, b)_\infty = 1$ iff the equation $ax^2 + by^2 = 1$ is solvable in $\mathbb{R}$.

theorem realHilbertSymbol.eq_neg_one_iff {a b : ℝˣ} : realHilbertSymbol a b = -1 ↔ ¬∃ (x : ℝ) (y : ℝ), ↑a * x ^ 2 + ↑b * y ^ 2 = 1

$(a, b)_\infty = -1$ iff the equation $ax^2 + by^2 = 1$ is unsolvable in $\mathbb{R}$.

theorem realHilbertSymbol.eq_one_or_neg_one (a b : ℝˣ) : realHilbertSymbol a b = 1 ∨ realHilbertSymbol a b = -1

The real Hilbert symbol takes values in $\{\pm 1\}$.

theorem realHilbertSymbol.sq (a b : ℝˣ) : realHilbertSymbol a b ^ 2 = 1

$(a, b)_\infty^2 = 1$.

theorem realHilbertSymbol.ne_zero (a b : ℝˣ) : realHilbertSymbol a b ≠ 0

The real Hilbert symbol is never zero.

theorem realHilbertSymbol.isSolvable_of_pos_left {a b : ℝˣ} (ha : 0 < ↑a) : HilbertSymbol.IsSolvable ℝ a b

If $a > 0$, then $ax^2 + by^2 = 1$ is solvable over $\mathbb{R}$ (take $x = 1/\sqrt{a}$, $y = 0$).

theorem realHilbertSymbol.isSolvable_of_pos_right {a b : ℝˣ} (hb : 0 < ↑b) : HilbertSymbol.IsSolvable ℝ a b

If $b > 0$, then $ax^2 + by^2 = 1$ is solvable over $\mathbb{R}$ (take $x = 0$, $y = 1/\sqrt{b}$).

theorem realHilbertSymbol.not_isSolvable_of_both_neg {a b : ℝˣ} (ha : ↑a < 0) (hb : ↑b < 0) : ¬HilbertSymbol.IsSolvable ℝ a b

If both $a < 0$ and $b < 0$, then $ax^2 + by^2 \le 0 < 1$, so the equation $ax^2 + by^2 = 1$ has no real solution.

theorem realHilbertSymbol.eq_neg_one_iff_both_neg (a b : ℝˣ) : realHilbertSymbol a b = -1 ↔ ↑a < 0 ∧ ↑b < 0

(Textbook Theorem 10.4, real case) The real Hilbert symbol satisfies $(a, b)_\infty = -1$ if and only if both $a$ and $b$ are negative.

theorem HilbertSymbol.IsSolvable.representsZero {F : Type u_2} [Field F] [CharZero F] {a b : Fˣ} (h : IsSolvable F a b) : RepresentsZero F a b

Solvability of $ax^2 + by^2 = 1$ implies non-trivial representation of zero by $z^2 - ax^2 - by^2$ (take $z = 1$).

theorem HilbertSymbol.y_ne_zero_of_binary_zero {F : Type u_2} [Field F] {a b : Fˣ} {x₀ y₀ : F} (hx₀ : x₀ ≠ 0) (h0 : ↑a * x₀ ^ 2 + ↑b * y₀ ^ 2 = 0) : y₀ ≠ 0

Helper lemma: if $ax_0^2 + by_0^2 = 0$ and $x_0 \neq 0$, then $y_0 \neq 0$ (since otherwise $ax_0^2 = 0$, contradicting $a \neq 0$ and $x_0 \neq 0$).

theorem HilbertSymbol.binary_form_represents_all {F : Type u_2} [Field F] [CharZero F] {a b : Fˣ} {x₀ y₀ : F} (hx₀ : x₀ ≠ 0) (h0 : ↑a * x₀ ^ 2 + ↑b * y₀ ^ 2 = 0) (c : F) : ∃ (x : F) (y : F), ↑a * x ^ 2 + ↑b * y ^ 2 = c

Helper lemma: if the binary form $ax^2 + by^2$ represents zero non-trivially, then it represents every element $c \in F$.

theorem HilbertSymbol.RepresentsZero.isSolvable {F : Type u_2} [Field F] [CharZero F] {a b : Fˣ} (h : RepresentsZero F a b) : IsSolvable F a b

If $z^2 - ax^2 - by^2$ represents zero non-trivially, then $ax^2 + by^2 = 1$ is solvable.

theorem HilbertSymbol.isSolvable_iff_representsZero {F : Type u_2} [Field F] [CharZero F] {a b : Fˣ} : IsSolvable F a b ↔ RepresentsZero F a b

(Textbook Lemma 10.2, parts (1) ↔ (2)) Solvability of $ax^2 + by^2 = 1$ over $F$ is equivalent to non-trivial representation of zero by $z^2 - ax^2 - by^2$ over $F$.

theorem HilbertSymbol.IsNormFromSqrtExt.representsZero {F : Type u_2} [Field F] [CharZero F] {a b : Fˣ} (h : IsNormFromSqrtExt F a b) : RepresentsZero F a b

If $a$ is a norm from $F(\sqrt{b})$, i.e., $z^2 - by^2 = a$ has a solution, then $z^2 - ax^2 - by^2$ represents zero non-trivially (take $x = 1$).

theorem HilbertSymbol.RepresentsZero.isNormFromSqrtExt {F : Type u_2} [Field F] [CharZero F] {a b : Fˣ} (h : RepresentsZero F a b) : IsNormFromSqrtExt F a b

If $z^2 - ax^2 - by^2$ represents zero non-trivially, then $a$ is a norm from the quadratic extension $F(\sqrt{b})$.

theorem HilbertSymbol.representsZero_iff_isNormFromSqrtExt {F : Type u_2} [Field F] [CharZero F] {a b : Fˣ} : RepresentsZero F a b ↔ IsNormFromSqrtExt F a b

(Textbook Lemma 10.2, parts (2) ↔ (3)) Non-trivial representation of zero by $z^2 - ax^2 - by^2$ over $F$ is equivalent to $a$ being a norm from $F(\sqrt{b})$.

noncomputable def HilbertSymbol.toZpDiv {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]} (h : ‖a‖ ≤ ‖b‖) : ℤ_[p]

Helper: when $\|a\| \le \|b\|$, the quotient $a/b$ lies in $\mathbb{Z}_p$ (has $p$-adic norm $\le 1$).

@[simp]

theorem HilbertSymbol.toZpDiv_coe {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]} (h : ‖a‖ ≤ ‖b‖) : ↑(toZpDiv h) = a / b

The underlying $\mathbb{Q}_p$-value of toZpDiv h is $a/b$.

theorem HilbertSymbol.ne_zero_of_norm_le {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]} (ha : a ≠ 0) (h : ‖a‖ ≤ ‖b‖) : b ≠ 0

If $a \neq 0$ and $\|a\| \le \|b\|$, then $b \neq 0$.

theorem HilbertSymbol.exists_max_norm {p : ℕ} [Fact (Nat.Prime p)] {x y z : ℚ_[p]} (hne : x ≠ 0 ∨ y ≠ 0 ∨ z ≠ 0) : ‖y‖ ≤ ‖x‖ ∧ ‖z‖ ≤ ‖x‖ ∧ x ≠ 0 ∨ ‖x‖ ≤ ‖y‖ ∧ ‖z‖ ≤ ‖y‖ ∧ y ≠ 0 ∨ ‖x‖ ≤ ‖z‖ ∧ ‖y‖ ≤ ‖z‖ ∧ z ≠ 0

Among three elements of $\mathbb{Q}_p$ not all zero, one of them has maximum $p$-adic norm (and is non-zero); used to extract a primitive representative.

theorem HilbertSymbol.primitive_of_x_max {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} {x y z : ℚ_[p]} (hx : x ≠ 0) (hyx : ‖y‖ ≤ ‖x‖) (hzx : ‖z‖ ≤ ‖x‖) (heq : z ^ 2 = ↑a * x ^ 2 + ↑b * y ^ 2) : HasPrimitiveSolution a b

Constructs a primitive $p$-adic integer solution when $x$ has maximum norm (rescaling by dividing through by $x$).

theorem HilbertSymbol.primitive_of_y_max {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} {x y z : ℚ_[p]} (hy : y ≠ 0) (hxy : ‖x‖ ≤ ‖y‖) (hzy : ‖z‖ ≤ ‖y‖) (heq : z ^ 2 = ↑a * x ^ 2 + ↑b * y ^ 2) : HasPrimitiveSolution a b

Constructs a primitive $p$-adic integer solution when $y$ has maximum norm.

theorem HilbertSymbol.primitive_of_z_max {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} {x y z : ℚ_[p]} (hz : z ≠ 0) (hxz : ‖x‖ ≤ ‖z‖) (hyz : ‖y‖ ≤ ‖z‖) (heq : z ^ 2 = ↑a * x ^ 2 + ↑b * y ^ 2) : HasPrimitiveSolution a b

Constructs a primitive $p$-adic integer solution when $z$ has maximum norm.

theorem HilbertSymbol.RepresentsZero.hasPrimitiveSolution {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} (h : RepresentsZero ℚ_[p] a b) : HasPrimitiveSolution a b

Over $\mathbb{Q}_p$, non-trivial representation of zero by $z^2 - ax^2 - by^2$ implies the existence of a primitive $p$-adic integer solution.

theorem HilbertSymbol.HasPrimitiveSolution.representsZero {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} (h : HasPrimitiveSolution a b) : RepresentsZero ℚ_[p] a b

A primitive $p$-adic integer solution immediately gives non-trivial representation of zero over $\mathbb{Q}_p$.

theorem HilbertSymbol.representsZero_iff_hasPrimitiveSolution {p : ℕ} [Fact (Nat.Prime p)] {a b : ℚ_[p]ˣ} : RepresentsZero ℚ_[p] a b ↔ HasPrimitiveSolution a b

(Textbook Lemma 10.2, parts (2) ↔ (4)) Over $\mathbb{Q}_p$, non-trivial representation of zero is equivalent to existence of a primitive $p$-adic integer solution.

theorem HilbertSymbol.lemma_10_2 {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : IsSolvable ℚ_[p] a b ↔ RepresentsZero ℚ_[p] a b

(Textbook Lemma 10.2, parts (1) ↔ (2) over $\mathbb{Q}_p$) Solvability of $ax^2 + by^2 = 1$ over $\mathbb{Q}_p$ is equivalent to representation of zero.

theorem HilbertSymbol.isSolvable_iff_hasPrimitiveSolution {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : IsSolvable ℚ_[p] a b ↔ HasPrimitiveSolution a b

(Textbook Lemma 10.2, parts (1) ↔ (4)) Solvability of $ax^2 + by^2 = 1$ over $\mathbb{Q}_p$ is equivalent to existence of a primitive $p$-adic integer solution.

theorem HilbertSymbol.isSolvable_iff_isNormFromSqrtExt {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : IsSolvable ℚ_[p] a b ↔ IsNormFromSqrtExt ℚ_[p] a b

(Textbook Lemma 10.2, parts (1) ↔ (3)) Solvability of $ax^2 + by^2 = 1$ over $\mathbb{Q}_p$ is equivalent to $a$ being a norm from $\mathbb{Q}_p(\sqrt{b})$.

theorem HilbertSymbol.hasPrimitiveSolution_iff_isNormFromSqrtExt {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : HasPrimitiveSolution a b ↔ IsNormFromSqrtExt ℚ_[p] a b

(Textbook Lemma 10.2, parts (3) ↔ (4)) Over $\mathbb{Q}_p$, existence of a primitive solution is equivalent to $a$ being a norm from $\mathbb{Q}_p(\sqrt{b})$.

theorem HilbertSymbol.hilbert_eq_one_iff_representsZero {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : padicHilbertSymbol p a b = 1 ↔ RepresentsZero ℚ_[p] a b

The $p$-adic Hilbert symbol is $1$ iff $z^2 - ax^2 - by^2$ represents zero non-trivially.

theorem HilbertSymbol.hilbert_eq_one_iff_hasPrimitiveSolution {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : padicHilbertSymbol p a b = 1 ↔ HasPrimitiveSolution a b

The $p$-adic Hilbert symbol is $1$ iff there exists a primitive $p$-adic integer solution.

theorem HilbertSymbol.hilbert_eq_one_iff_isNormFromSqrtExt {p : ℕ} [Fact (Nat.Prime p)] (a b : ℚ_[p]ˣ) : padicHilbertSymbol p a b = 1 ↔ IsNormFromSqrtExt ℚ_[p] a b

The $p$-adic Hilbert symbol is $1$ iff $a$ is a norm from $\mathbb{Q}_p(\sqrt{b})$.

theorem hilbertSymbol.hilbert_neg_self {F : Type u_2} [Field F] [CharZero F] (c : Fˣ) : hilbertSymbol F (-c) c = 1

(Textbook Corollary 10.3, part 1) For any unit $c \in F^\times$, $(-c, c)_F = 1$, since $(-c) \cdot ((c^{-1}-1)/2)^2 + c \cdot ((1+c^{-1})/2)^2 = 1$.

theorem hilbertSymbol.isNormFromSqrtExt_mul {F : Type u_2} [Field F] {a b c : Fˣ} (ha : HilbertSymbol.IsNormFromSqrtExt F a c) (hb : HilbertSymbol.IsNormFromSqrtExt F b c) : HilbertSymbol.IsNormFromSqrtExt F (a * b) c

The set of norms from $F(\sqrt{c})$ is closed under multiplication.

theorem hilbertSymbol.isSolvable_mul_of_isSolvable {F : Type u_2} [Field F] [CharZero F] {a b c : Fˣ} (ha : HilbertSymbol.IsSolvable F a c) (hb : HilbertSymbol.IsSolvable F b c) : HilbertSymbol.IsSolvable F (a * b) c

If both $ax^2 + cy^2 = 1$ and $bx^2 + cy^2 = 1$ are solvable, then so is $(ab)x^2 + cy^2 = 1$. This is the multiplicativity in the first argument when the symbol equals $1$.

theorem hilbertSymbol.isSolvable_inv_of_isSolvable {F : Type u_2} [Field F] {a c : Fˣ} (h : HilbertSymbol.IsSolvable F a c) : HilbertSymbol.IsSolvable F a⁻¹ c

If $ax^2 + cy^2 = 1$ is solvable, then so is $a^{-1}x^2 + cy^2 = 1$ (using the substitution $x \mapsto ax$).

theorem hilbertSymbol.hilbert_mul_of_eq_one {F : Type u_2} [Field F] [CharZero F] (a b c : Fˣ) (h : hilbertSymbol F a c = 1) : hilbertSymbol F a c * hilbertSymbol F b c = hilbertSymbol F (a * b) c

Bilinearity in the first argument when $(a, c)_F = 1$: in that case, $(a, c)_F \cdot (b, c)_F = (ab, c)_F$.

theorem hilbertSymbol.hilbert_self_eq_neg_one {F : Type u_2} [Field F] [CharZero F] (c : Fˣ) : hilbertSymbol F c c = hilbertSymbol F (-1) c

(Textbook Corollary 10.3, part 2) For any unit $c \in F^\times$, $(c, c)_F = (-1, c)_F$.

noncomputable def HilbertSymbol.unitZpToQp {p : ℕ} [Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) : ℚ_[p]ˣ

Inclusion of $p$-adic integer units into $p$-adic field units: $\mathbb{Z}_p^\times \hookrightarrow \mathbb{Q}_p^\times$.

theorem HilbertSymbol.unitZpToQp_coe {p : ℕ} [Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) : ↑(unitZpToQp u) = ↑↑u

The image of unitZpToQp u in $\mathbb{Q}_p$ agrees with the inclusion of $u$.

theorem HilbertSymbol.chevalley_warning_hensel_lift (p : ℕ) [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (u v : ℤ_[p]ˣ) : ∃ (x₀ : ℤ_[p]) (y₀ : ℤ_[p]) (z₀ : ℤ_[p]ˣ), ↑z₀ ^ 2 = ↑u * x₀ ^ 2 + ↑v * y₀ ^ 2

(Helper, key step of Lemma 10.5) For odd prime $p$ and $p$-adic integer units $u, v \in \mathbb{Z}_p^\times$, there exist $x_0, y_0 \in \mathbb{Z}_p$ and a unit $z_0 \in \mathbb{Z}_p^\times$ such that $z_0^2 = u x_0^2 + v y_0^2$. The proof uses Chevalley–Warning to find a solution modulo $p$, then Hensel's lemma to lift it.

theorem HilbertSymbol.hilbert_symbol_units_eq_one_of_odd (p : ℕ) [Fact (Nat.Prime p)] (hp_odd : p ≠ 2) (u v : ℤ_[p]ˣ) : padicHilbertSymbol p (unitZpToQp u) (unitZpToQp v) = 1

(Textbook Lemma 10.5) For an odd prime $p$ and any two $p$-adic integer units $u, v \in \mathbb{Z}_p^\times$, the Hilbert symbol $(u, v)_p = 1$.