Documentation

Atlas.ArithmeticGeometry.code.HasseMinkowskiProof

theorem exists_prime_not_square_padic (c : ˣ) (hc_pos : 0 < c) (hc_not_sq : ¬IsSquare c) :
∃ (p : ) (x : Fact (Nat.Prime p)), ¬IsSquare (ratToQpUnits p c)

If a positive rational $c \in \mathbb{Q}^\times$ is not a square in $\mathbb{Q}$, then there exists a prime $p$ such that $c$ is also not a square in $\mathbb{Q}_p$.

theorem exists_rat_local_witness (p : ) [Fact (Nat.Prime p)] (c : ˣ) (hc : ¬IsSquare (ratToQpUnits p c)) :
∃ (b : ˣ), padicHilbertSymbol p (ratToQpUnits p b) (ratToQpUnits p c) = -1

If $c$ is not a square in $\mathbb{Q}_p$, then there exists a rational witness $b \in \mathbb{Q}^\times$ such that the $p$-adic Hilbert symbol $(b, c)_p = -1$.

Solvability of the Hilbert equation $b x^2 + c y^2 = 1$ over $\mathbb{Q}$ implies its solvability over $\mathbb{Q}_p$, obtained by base change of the rational solution.

theorem rat_hilbert_one_implies_local (p : ) [Fact (Nat.Prime p)] (b c : ˣ) (h : hilbertSymbol b c = 1) :

If the rational Hilbert symbol $(b, c)_\mathbb{Q} = 1$, then the $p$-adic Hilbert symbol $(b, c)_p = 1$ for every prime $p$.

theorem hilbertSymbol.self_neg_self {F : Type u_1} [Field F] [NeZero 2] (x : Fˣ) :
hilbertSymbol F x (-x) = 1

For any field $F$ with $2 \neq 0$ and any unit $x$, the Hilbert symbol $(x, -x) = 1$, witnessed by the identity solution $x \cdot ((x^{-1}+1)/2)^2 + (-x) \cdot ((x^{-1}-1)/2)^2 = 1$.

The Hilbert equation $(a c^2) x^2 + b y^2 = 1$ is solvable iff $a x^2 + b y^2 = 1$ is, since multiplying $a$ by a square does not change the square class.

The Hilbert equation $a x^2 + (b c^2) y^2 = 1$ is solvable iff $a x^2 + b y^2 = 1$ is, by symmetry from IsSolvable_sq_mul_left.

theorem hilbertSymbol.sq_mul_left {F : Type u_1} [Field F] (a c b : Fˣ) :
hilbertSymbol F (a * c * c) b = hilbertSymbol F a b

The Hilbert symbol is invariant under scaling the first argument by a square: $(a c^2, b) = (a, b)$.

theorem hilbertSymbol.sq_mul_right {F : Type u_1} [Field F] (a b c : Fˣ) :
hilbertSymbol F a (b * c * c) = hilbertSymbol F a b

The Hilbert symbol is invariant under scaling the second argument by a square: $(a, b c^2) = (a, b)$.

theorem hilbertSymbol.div_div_eq_mul {F : Type u_1} [Field F] [HilbertBilinearField F] (a b t : Fˣ) :
hilbertSymbol F (a * t⁻¹) (b * t⁻¹) = hilbertSymbol F a b * hilbertSymbol F t (-(a * b))

The "division" identity for the Hilbert symbol over a field with bilinear Hilbert symbol: $(a/t, b/t) = (a, b) \cdot (t, -ab)$. A key step in relating binary form representation to the Hilbert symbol.

theorem hilbertSymbol.prod_pm_one_eq_one_iff {x y : } (hx : x = 1 x = -1) (hy : y = 1 y = -1) :
x * y = 1 x = y

For integers $x, y \in \{1, -1\}$, the product $x y = 1$ iff $x = y$.

def TernaryForm.RepresentsZero (F : Type u_1) [Field F] (a b c : Fˣ) :

The ternary form $a x^2 + b y^2 + c z^2$ with unit coefficients $a, b, c \in F^\times$ represents zero if there is a nontrivial solution $(x, y, z) \neq (0, 0, 0)$ with $a x^2 + b y^2 + c z^2 = 0$.

Instances For
    def BinaryForm.Represents (F : Type u_1) [Field F] (a b : Fˣ) (t : F) :

    The binary form $a x^2 + b y^2$ with unit coefficients $a, b \in F^\times$ represents $t \in F$ if there exist $x, y \in F$ such that $a x^2 + b y^2 = t$.

    Instances For

      Representation criterion via Hilbert symbols. Over a field with bilinear Hilbert symbol, the binary form $a x^2 + b y^2$ represents $t \in F^\times$ if and only if $(a, b) = (t, -ab)$ in $\{1, -1\}$.

      If the binary form $a x^2 + b y^2$ represents $-c$, then the ternary form $a x^2 + b y^2 + c z^2$ represents zero (with $z = 1$).

      If the ternary form $a x^2 + b y^2 + c z^2$ represents zero, then the binary form $a x^2 + b y^2$ represents $-c$: either dehomogenize by dividing by $z$ if $z \neq 0$, or use the "represents-all" property of an isotropic binary form.

      The ternary form $a x^2 + b y^2 + c z^2$ represents zero iff the binary form $a x^2 + b y^2$ represents $-c$.

      Corollary 11.4. The ternary form $a x^2 + b y^2 + c z^2$ represents zero over $F$ iff $(a, b) = (-c, -(ab))$ in $\{1, -1\}$.

      For a nonzero integer $a$, the set of primes $p$ for which $|a|_p \neq 1$ is finite (equivalently, only finitely many primes divide $a$).

      For a nonzero natural number $d$, the set of primes $p$ for which $|d|_p \neq 1$ is finite.

      For a nonzero rational $q$, the set of primes $p$ for which $|q|_p \neq 1$ is finite. That is, $q$ is a $p$-adic unit for all but finitely many primes.

      theorem finitely_many_bad_primes {n : } (w : Fin n) (hw : ∀ (i : Fin n), w i 0) :
      {p : | Nat.Prime p ∃ (i : Fin n), padicNorm p (w i) 1}.Finite

      For a finite tuple of nonzero rationals $w_0, \dots, w_{n-1}$, the set of "bad" primes (those at which some $w_i$ is not a unit) is finite.

      theorem padicNorm_eq_one_to_padic_norm {p : } [Fact (Nat.Prime p)] (q : ) (h : padicNorm p q = 1) :
      q = 1

      Bridge between rational and $p$-adic norms: if the rational $p$-adic norm $|q|_p = 1$, then the $p$-adic norm of $q$ viewed in $\mathbb{Q}_p$ also equals $1$.

      theorem diagonal_form_represents_zero_locally_cofinitely {n : } (hn : 2 < n) (w : Fin n) (hw : ∀ (i : Fin n), w i 0) :
      ∃ (S : Finset ), ∀ (p : ) (x : Nat.Prime p), pS∃ (x_2 : Fin nℚ_[p]), (∃ (i : Fin n), x_2 i 0) i : Fin n, (w i) * x_2 i ^ 2 = 0

      Corollary 11.2. A diagonal quadratic form $\sum_{i < n} w_i x_i^2$ with $n > 2$ variables and nonzero rational coefficients represents zero in $\mathbb{Q}_p$ for all but finitely many primes $p$. The exceptional set consists of $\{2\}$ together with primes dividing some coefficient.

      noncomputable def Corollary115.ratToRealUnits (a : ˣ) :

      The canonical map sending a rational unit $a \in \mathbb{Q}^\times$ to a real unit $a \in \mathbb{R}^\times$.

      Instances For
        noncomputable def Corollary115.ratToQpUnits (p : ) [Fact (Nat.Prime p)] (a : ˣ) :

        The canonical map sending a rational unit $a \in \mathbb{Q}^\times$ to a $p$-adic unit $a \in \mathbb{Q}_p^\times$.

        Instances For
          noncomputable def Corollary115.hilbertAtInfty (a b : ˣ) :

          The Hilbert symbol at the archimedean place: $(a, b)_\infty$ equals the real Hilbert symbol of $a, b$ regarded as units of $\mathbb{R}^\times$.

          Instances For
            noncomputable def Corollary115.hilbertAtPrime (p : ) [Fact (Nat.Prime p)] (a b : ˣ) :

            The Hilbert symbol at the finite place $p$: $(a, b)_p$ is the $p$-adic Hilbert symbol of $a, b$ regarded as units of $\mathbb{Q}_p^\times$.

            Instances For
              noncomputable def Corollary115.globalHilbertProduct (a b : ˣ) :

              The global Hilbert product $\prod_v (a, b)_v$, taken over all places of $\mathbb{Q}$: the archimedean place $\infty$ and all finite primes $p$.

              Instances For

                Hilbert reciprocity (product formula). For any $a, b \in \mathbb{Q}^\times$, the global product $\prod_v (a, b)_v = 1$.

                For any $a, b \in \mathbb{Q}^\times$, the local Hilbert symbol $(a, b)_p$ is equal to $1$ for all but finitely many primes $p$.

                inductive Place :

                The set of places of $\mathbb{Q}$: either the archimedean (infinite) place $\infty$ or a finite place $p$ given by a prime.

                Instances For
                  @[implicit_reducible]
                  def instDecidableEqPlace.decEq (x✝ x✝¹ : Place) :
                  Decidable (x✝ = x✝¹)
                  Instances For
                    noncomputable def hilbertAt (v : Place) (a b : ˣ) :

                    The Hilbert symbol $(a, b)_v$ at the place $v$ of $\mathbb{Q}$, taking values in $\{1, -1\}$.

                    Instances For
                      theorem hilbertAt_eq_one_or_neg_one (v : Place) (a b : ˣ) :
                      hilbertAt v a b = 1 hilbertAt v a b = -1

                      The Hilbert symbol at any place takes values in $\{1, -1\}$.

                      The global Hilbert product can be rewritten using the hilbertAt notation indexed by places: $\prod_v (a, b)_v = (a, b)_\infty \cdot \prod_p (a, b)_p$.

                      theorem hilbert_symbol_determined_by_all_but_one (a b c d : ˣ) (hprod1 : Corollary115.globalHilbertProduct a b = 1) (hprod2 : Corollary115.globalHilbertProduct c d = 1) (v₀ : Place) (h_agree : ∀ (v : Place), v v₀hilbertAt v a b = hilbertAt v c d) :
                      hilbertAt v₀ a b = hilbertAt v₀ c d

                      A consequence of Hilbert reciprocity. If two pairs $(a, b)$ and $(c, d)$ have matching local Hilbert symbols at all places except possibly one place $v_0$, then they also match at $v_0$. This follows from the product formula $\prod_v (a, b)_v = 1$.

                      theorem corollary_11_5 (a b c : ˣ) (v₀ : Place) (h : ∀ (v : Place), v v₀hilbertAt v a b = hilbertAt v (-c) (-(a * b))) :
                      hilbertAt v₀ a b = hilbertAt v₀ (-c) (-(a * b))

                      Corollary 11.5. If the local equality $(a, b)_v = (-c, -(ab))_v$ (the ternary representation-of-zero criterion) holds at every place except possibly $v_0$, then it also holds at $v_0$. Applied to deduce global representation of zero from local conditions.

                      @[implicit_reducible]
                      noncomputable instance invertibleTwoQ :

                      The element $2 \in \mathbb{Q}$ is invertible (needed for converting between quadratic forms and their associated symmetric matrices over $\mathbb{Q}$).

                      A symmetric matrix $M$ over $\mathbb{Q}$ defines a quadratic form $x \mapsto x^T M x$, and represents zero $p$-adically if there exists a nonzero vector $x \in \mathbb{Q}_p^n$ with $x^T M x = 0$.

                      Instances For

                        Diagonalization of nondegenerate quadratic forms over $\mathbb{Q}$. Any nondegenerate quadratic form $Q$ over $\mathbb{Q}$ in $n$ variables is equivalent (via a linear change of coordinates) to a diagonal weighted sum of squares $\sum w_i x_i^2$ with all $w_i \neq 0$.

                        theorem equiv_diagonal_represents_zero_implies_matrix_represents_zero {n : } (p : ) [Fact (Nat.Prime p)] (Q : QuadraticForm (Fin n)) (w : Fin n) (hequiv : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares w)) (hzero : ∃ (x : Fin nℚ_[p]), (∃ (i : Fin n), x i 0) i : Fin n, (w i) * x i ^ 2 = 0) :

                        Transport of $p$-adic isotropy along an equivalence: if $Q$ is rationally equivalent to the diagonal form $\sum w_i x_i^2$ and the latter represents zero $p$-adically, then the matrix $Q.\mathrm{toMatrix}'$ of $Q$ also represents zero $p$-adically.