Hilbert symbol

DefinitionSolvability of \(ax^2 + by^2 = 1\)#✓fully proved

For a field \(F\) and nonzero elements \(a, b \in F\), the equation \(ax^2 + by^2 = 1\) is solvable over \(F\) if there exist \(x, y \in F\) with \(ax^2 + by^2 = 1\).

def IsSolvable (a b : Fˣ) : Prop :=
  ∃ x y : F, (a : F) * x ^ 2 + (b : F) * y ^ 2 = 1

Used by 6

Used byWhen the \(p\)-adic Hilbert symbol is \(-1\) · Real Hilbert symbol equal to \(-1\) · When the \(p\)-adic Hilbert symbol is \(1\) · Real Hilbert symbol equal to \(1\) · The Hilbert symbol of a field is \(\pm 1\) · Hilbert symbol of a field

DefinitionHilbert symbol of a field#✓fully proved

For a field \(F\) and nonzero elements \(a, b \in F\), the Hilbert symbol \((a, b)_F\) is the integer \(1\) if there exist \(x, y \in F\) with \(ax^2 + by^2 = 1\), and \(-1\) otherwise.

noncomputable def hilbertSymbol (F : Type*) [Field F] (a b : Fˣ) : ℤ :=
  if HilbertSymbol.IsSolvable F a b then 1 else -1

Uses 1 · Used by 7

Statement usesSolvability of \(ax^2 + by^2 = 1\)

Used byWhen the \(p\)-adic Hilbert symbol is \(-1\) · Real Hilbert symbol equal to \(-1\) · When the \(p\)-adic Hilbert symbol is \(1\) · Real Hilbert symbol equal to \(1\) · The Hilbert symbol of a field is \(\pm 1\) · The \(p\)-adic Hilbert symbol · Real Hilbert symbol

TheoremThe Hilbert symbol of a field is \(\pm 1\)#✓fully proved

For every field \(F\) and all nonzero \(a, b \in F\), the Hilbert symbol \((a, b)_F\) of \(a\) and \(b\) over \(F\) equals \(1\) or \(-1\).

theorem eq_one_or_neg_one (a b : Fˣ) :
    hilbertSymbol F a b = 1 ∨ hilbertSymbol F a b = -1

Uses 2 · Used by 2

Statement usesHilbert symbol of a field

Proof usesSolvability of \(ax^2 + by^2 = 1\)

Used byThe \(p\)-adic Hilbert symbol is \(\pm 1\) · The real Hilbert symbol is \(\pm 1\)

DefinitionThe \(p\)-adic Hilbert symbol#✓fully proved

For a prime \(p\) and nonzero \(a, b \in \mathbb{Q}_p\), the \(p\)-adic Hilbert symbol \((a, b)_p\) is the integer \(1\) if there exist \(x, y \in \mathbb{Q}_p\) with \(ax^2 + by^2 = 1\), and \(-1\) otherwise.

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

Uses 1 · Used by 4

Statement usesHilbert symbol of a field

Used byWhen the \(p\)-adic Hilbert symbol is \(-1\) · When the \(p\)-adic Hilbert symbol is \(1\) · The \(p\)-adic Hilbert symbol is \(\pm 1\) · The Hilbert symbol of two \(p\)-adic units is trivial for odd \(p\)

TheoremWhen the \(p\)-adic Hilbert symbol is \(1\)#✓fully proved

For a prime \(p\) and nonzero \(a, b \in \mathbb{Q}_p\), the \(p\)-adic Hilbert symbol \((a, b)_p\) equals \(1\) if and only if there exist \(x, y \in \mathbb{Q}_p\) with \(ax^2 + by^2 = 1\).

@[simp]
theorem eq_one_iff {a b : ℚ_[p]ˣ} :
    padicHilbertSymbol p a b = 1 ↔
      ∃ x y : ℚ_[p], (a : ℚ_[p]) * x ^ 2 + (b : ℚ_[p]) * y ^ 2 = 1

Uses 3 · Used by 1

Statement usesThe \(p\)-adic Hilbert symbol

Proof usesSolvability of \(ax^2 + by^2 = 1\) · Hilbert symbol of a field

Used byThe Hilbert symbol of two \(p\)-adic units is trivial for odd \(p\)

TheoremWhen the \(p\)-adic Hilbert symbol is \(-1\)#✓fully proved

For a prime \(p\) and nonzero \(a, b \in \mathbb{Q}_p\), the \(p\)-adic Hilbert symbol \((a, b)_p\) equals \(-1\) if and only if there are no \(x, y \in \mathbb{Q}_p\) with \(ax^2 + by^2 = 1\).

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

Uses 3

Statement usesThe \(p\)-adic Hilbert symbol

Proof usesSolvability of \(ax^2 + by^2 = 1\) · Hilbert symbol of a field

TheoremThe \(p\)-adic Hilbert symbol is \(\pm 1\)#✓fully proved

For a prime \(p\) and all nonzero \(a, b \in \mathbb{Q}_p\), the \(p\)-adic Hilbert symbol \((a, b)_p\) equals \(1\) or \(-1\).

theorem eq_one_or_neg_one (a b : ℚ_[p]ˣ) :
    padicHilbertSymbol p a b = 1 ∨ padicHilbertSymbol p a b = -1

Uses 2

Statement usesThe \(p\)-adic Hilbert symbol

Proof usesThe Hilbert symbol of a field is \(\pm 1\)

TheoremUnit diagonal forms in at least three variables over \(\mathbb{Q}_p\) are isotropic for odd \(p\)#✓fully proved

Unit diagonal forms in at least three variables over \(\mathbb{Q}_p\) are isotropic for odd \(p\). Let \(p\) be an odd prime, let \(n > 2\), and let \(a_1, \dots, a_n\) be units of \(\mathbb{Z}_p\). Then there is a nonzero vector \((x_1, \dots, x_n) \in \mathbb{Q}_p^n\) with \(a_1 x_1^2 + \dots + a_n x_n^2 = 0\).

theorem diagonal_unit_isotropic (p : ℕ) [Fact p.Prime] (hp_odd : p ≠ 2)
    {n : ℕ} (hn : 2 < n) (a : Fin n → ℤ_[p]ˣ) :
    ∃ x : Fin n → ℚ_[p], x ≠ 0 ∧ ∑ i, ((a i : ℤ_[p]) : ℚ_[p]) * (x i) ^ 2 = 0

Sources

• ArithmeticGeometry:75.

DefinitionReal Hilbert symbol#✓fully proved

For nonzero real numbers \(a\) and \(b\), the real Hilbert symbol of \(a\) and \(b\) is the integer \(1\) if there are real numbers \(x, y\) with \(a x^2 + b y^2 = 1\), and the integer \(-1\) otherwise.

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

Uses 1 · Used by 4

Statement usesHilbert symbol of a field

Used byReal Hilbert symbol equal to \(-1\) · Sign rule for the real Hilbert symbol · Real Hilbert symbol equal to \(1\) · The real Hilbert symbol is \(\pm 1\)

TheoremReal Hilbert symbol equal to \(1\)#✓fully proved

For nonzero real numbers \(a\) and \(b\), the real Hilbert symbol of \(a\) and \(b\) equals \(1\) if and only if there are real numbers \(x, y\) with \(a x^2 + b y^2 = 1\).

@[simp]
theorem eq_one_iff {a b : ℝˣ} :
    realHilbertSymbol a b = 1 ↔
      ∃ x y : ℝ, (a : ℝ) * x ^ 2 + (b : ℝ) * y ^ 2 = 1

Uses 3

Statement usesReal Hilbert symbol

Proof usesSolvability of \(ax^2 + by^2 = 1\) · Hilbert symbol of a field

TheoremReal Hilbert symbol equal to \(-1\)#✓fully proved

For nonzero real numbers \(a\) and \(b\), the real Hilbert symbol of \(a\) and \(b\) equals \(-1\) if and only if there are no real numbers \(x, y\) with \(a x^2 + b y^2 = 1\).

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

Uses 3 · Used by 1

Statement usesReal Hilbert symbol

Proof usesSolvability of \(ax^2 + by^2 = 1\) · Hilbert symbol of a field

Used bySign rule for the real Hilbert symbol

TheoremSign rule for the real Hilbert symbol#✓fully proved

For nonzero real numbers \(a\) and \(b\), the real Hilbert symbol of \(a\) and \(b\) equals \(-1\) if and only if \(a < 0\) and \(b < 0\).

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

Uses 2

Statement usesReal Hilbert symbol

Proof usesReal Hilbert symbol equal to \(-1\)

TheoremThe real Hilbert symbol is \(\pm 1\)#✓fully proved

For nonzero real numbers \(a\) and \(b\), the real Hilbert symbol of \(a\) and \(b\) equals \(1\) or \(-1\).

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

Uses 2

Statement usesReal Hilbert symbol

Proof usesThe Hilbert symbol of a field is \(\pm 1\)

DefinitionInclusion of \(p\)-adic integer units#✓fully proved

For a prime \(p\), this is the map from the units of \(\mathbb{Z}_p\) to the units of \(\mathbb{Q}_p\) induced by the inclusion \(\mathbb{Z}_p \subseteq \mathbb{Q}_p\).

noncomputable def unitZpToQp {p : ℕ} [Fact (Nat.Prime p)]
    (u : ℤ_[p]ˣ) : ℚ_[p]ˣ :=
  Units.map (PadicInt.Coe.ringHom (p := p)).toMonoidHom u

Used by 2

Used byThe Hilbert symbol of two \(p\)-adic units is trivial for odd \(p\) · Value of the inclusion of \(p\)-adic integer units

LemmaValue of the inclusion of \(p\)-adic integer units#✓fully proved

For a prime \(p\) and a unit \(u\) of \(\mathbb{Z}_p\), the image of \(u\) under the inclusion of the units of \(\mathbb{Z}_p\) into the units of \(\mathbb{Q}_p\), viewed as an element of \(\mathbb{Q}_p\), equals \(u\) viewed as an element of \(\mathbb{Q}_p\).

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

Uses 1 · Used by 1

Statement usesInclusion of \(p\)-adic integer units

Used byThe Hilbert symbol of two \(p\)-adic units is trivial for odd \(p\)

TheoremFor odd \(p\), a binary unit form over \(\mathbb{Z}_p\) represents a unit square#✓fully proved

Let \(p\) be an odd prime and let \(u, v\) be units of \(\mathbb{Z}_p\). Then there are \(x_0, y_0 \in \mathbb{Z}_p\) and a unit \(z_0\) of \(\mathbb{Z}_p\) with \(z_0^2 = u x_0^2 + v y_0^2\).

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

Sources

• Lemma 10.5, key step.

Used by 1

Used byThe Hilbert symbol of two \(p\)-adic units is trivial for odd \(p\)

TheoremThe Hilbert symbol of two \(p\)-adic units is trivial for odd \(p\)#✓fully proved

Let \(p\) be an odd prime and let \(u, v\) be units of \(\mathbb{Z}_p\). Then the \(p\)-adic Hilbert symbol of \(u\) and \(v\), viewed as units of \(\mathbb{Q}_p\), equals \(1\).

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

Sources

• Lemma 10.5.

Uses 5

Statement usesInclusion of \(p\)-adic integer units · The \(p\)-adic Hilbert symbol

Proof usesFor odd \(p\), a binary unit form over \(\mathbb{Z}_p\) represents a unit square · Value of the inclusion of \(p\)-adic integer units · When the \(p\)-adic Hilbert symbol is \(1\)

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.