Documentation

Atlas.ArithmeticGeometry.code.HilbertProductFormula

noncomputable def ratToRealUnits (a : ˣ) :

Inclusion of rational units into real units: $\mathbb{Q}^\times \to \mathbb{R}^\times$.

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

    Inclusion of rational units into $p$-adic units: $\mathbb{Q}^\times \to \mathbb{Q}_p^\times$.

    Instances For
      @[simp]
      theorem ratToRealUnits_val (a : ˣ) :
      (ratToRealUnits a) = a

      The image of ratToRealUnits a in $\mathbb{R}$ is just the inclusion of $a$.

      @[simp]
      theorem ratToQpUnits_val (p : ) [Fact (Nat.Prime p)] (a : ˣ) :
      (ratToQpUnits p a) = a

      The image of ratToQpUnits p a in $\mathbb{Q}_p$ is just the inclusion of $a$.

      The inclusion $\mathbb{Q}^\times \to \mathbb{R}^\times$ is multiplicative.

      theorem ratToQpUnits_mul (p : ) [Fact (Nat.Prime p)] (a b : ˣ) :

      The inclusion $\mathbb{Q}^\times \to \mathbb{Q}_p^\times$ is multiplicative.

      The image of $-1 \in \mathbb{Q}^\times$ in $\mathbb{Q}_p^\times$ is $-1$ (coming from $\mathbb{Z}_p^\times$).

      noncomputable def hilbertAtInfty (a b : ˣ) :

      The Hilbert symbol $(a, b)_\infty$ at the infinite (archimedean) place, computed by viewing $a, b \in \mathbb{Q}^\times$ as elements of $\mathbb{R}^\times$.

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

        The Hilbert symbol $(a, b)_p$ at the prime $p$, computed by viewing $a, b \in \mathbb{Q}^\times$ as elements of $\mathbb{Q}_p^\times$.

        Instances For
          theorem hilbertAtPrime_neg_one_neg_one_odd (p : ) [Fact (Nat.Prime p)] (hp : p 2) :
          hilbertAtPrime p (-1) (-1) = 1

          At an odd prime $p$, the Hilbert symbol $(-1, -1)_p = 1$, since $-1$ is a $p$-adic unit and by Lemma 10.5 the symbol on units is $1$ for odd primes.

          The image of $-1$ in $\mathbb{Q}_2^\times$ agrees with the padicUnit_one representation of $-1 \in \mathbb{Z}_2^\times$.

          At the prime $2$, the Hilbert symbol $(-1, -1)_2 = -1$: the equation $-x^2 - y^2 = 1$ has no solution over $\mathbb{Q}_2$.

          At the archimedean place, the Hilbert symbol $(-1, -1)_\infty = -1$: the equation $-x^2 - y^2 = 1$ is unsolvable over $\mathbb{R}$.

          theorem ratToQpUnits_eq_unitZpToQp_of_not_dvd (p : ) [Fact (Nat.Prime p)] (a : ˣ) (hnum : ¬p (↑a).num.natAbs) (hden : ¬p (↑a).den) :

          If a rational $a$ has $p \nmid \text{num}(a)$ and $p \nmid \text{den}(a)$, then $a$ is a $p$-adic unit, i.e., comes from $\mathbb{Z}_p^\times$.

          The image of $2 \in \mathbb{Q}^\times$ inside $\mathbb{Q}_2^\times$ agrees with twoQp.

          The image of $q \in \mathbb{Q}^\times$ inside $\mathbb{Q}_q^\times$ agrees with qpPrime q.

          The rational $2$, viewed in $\mathbb{Q}_p^\times$ for an odd prime $p$, is a $p$-adic unit.

          theorem ratToQpUnits_prime_at_two (q : ) (hq : Nat.Prime q) (hq_odd : q 2) :

          An odd prime $q$, viewed in $\mathbb{Q}_2^\times$, is a $2$-adic unit.

          (Textbook Corollary 10.10) For any $a, b \in \mathbb{Q}^\times$, the set of primes $p$ where $(a, b)_p \neq 1$ is finite. This is the finiteness condition that makes the global Hilbert product well-defined.

          noncomputable def globalHilbertProduct (a b : ˣ) :

          The global Hilbert product over all places: $\prod_v (a, b)_v$ where $v$ ranges over $\{\infty\} \cup \{p : p \text{ prime}\}$. By the product formula (Theorem 10.11), this always equals $1$. The product over primes is a finprod (well-defined by hilbert_product_formula_finite_support).

          Instances For

            (Textbook Theorem 10.11, case $a = b = -1$) The product formula holds for $(-1, -1)$: $\prod_v (-1, -1)_v = 1$. The two contributions are $(-1, -1)_\infty = -1$ (from $\mathbb{R}$) and $(-1, -1)_2 = -1$, with all other primes contributing $1$.

            theorem hilbert_product_neg_one_odd_prime_aux (q : ) (hq : Nat.Prime q) (hq_odd : q 2) :
            globalHilbertProduct (-1) (Units.mk0 q ) = 1

            (Auxiliary step for Theorem 10.11) For an odd prime $q$, the product formula holds for $(-1, q)$. Only the $2$-adic and $q$-adic places contribute non-trivially, and these contributions cancel because $\chi_4(q) = \left(\frac{-1}{q}\right)$ by quadratic reciprocity.

            Bilinearity in the first argument at the infinite place: $(ab, c)_\infty = (a, c)_\infty \cdot (b, c)_\infty$.

            theorem hilbertAtPrime_mul_left (p : ) [Fact (Nat.Prime p)] (a b c : ˣ) :

            Bilinearity in the first argument at the prime $p$: $(ab, c)_p = (a, c)_p \cdot (b, c)_p$.

            Symmetry of the Hilbert symbol at the infinite place: $(a, b)_\infty = (b, a)_\infty$.

            theorem hilbertAtPrime_comm (p : ) [Fact (Nat.Prime p)] (a b : ˣ) :

            Symmetry of the Hilbert symbol at a prime: $(a, b)_p = (b, a)_p$.

            Bilinearity of the global Hilbert product in the first argument: $\prod_v (ab, c)_v = \prod_v (a, c)_v \cdot \prod_v (b, c)_v$.

            Symmetry of the global Hilbert product: $\prod_v (a, b)_v = \prod_v (b, a)_v$.

            Bilinearity of the global Hilbert product in the second argument: $\prod_v (a, bc)_v = \prod_v (a, b)_v \cdot \prod_v (a, c)_v$.

            The global Hilbert product always takes the value $1$ or $-1$, as a product of $\pm 1$ values from a finite set of non-trivial contributions.

            The global Hilbert product is trivial in the first argument when $a = 1$: $\prod_v (1, b)_v = 1$ (since $1 \cdot x^2 + by^2 = 1$ always has solution $(1, 0)$).

            theorem globalHilbertProduct_generators (h1 : globalHilbertProduct (-1) (-1) = 1) (h2 : ∀ (q : ) (hq : Nat.Prime q), globalHilbertProduct (-1) (Units.mk0 q ) = 1) (h3 : ∀ (q : ) (hq : Nat.Prime q), have q' := Units.mk0 q ; globalHilbertProduct q' q' = 1) (h4 : ∀ (q : ) (hq : Nat.Prime q), q 2globalHilbertProduct (Units.mk0 2 ) (Units.mk0 q ) = 1) (h5 : ∀ (a b : ) (ha : Nat.Prime a) (hb : Nat.Prime b), a 2b 2a bglobalHilbertProduct (Units.mk0 a ) (Units.mk0 b ) = 1) (p q : ) (hp : Nat.Prime p) (hq : Nat.Prime q) :
            globalHilbertProduct (Units.mk0 p ) (Units.mk0 q ) = 1

            If the global Hilbert product equals $1$ on the generators of $\mathbb{Q}^\times$ (namely $-1$, and primes $p$ paired against each other), then it equals $1$ on any pair of primes $(p, q)$.

            The global Hilbert product is invariant under taking inverses in the first argument: $\prod_v (a^{-1}, b)_v = \prod_v (a, b)_v$ (follows from bilinearity and $\pm 1$ values).

            theorem globalHilbertProduct_pos_nat (b : ˣ) (h2 : ∀ (q : ) (hq : Nat.Prime q), globalHilbertProduct (-1) (Units.mk0 q ) = 1) (hgen : ∀ (q : ) (hq : Nat.Prime q), globalHilbertProduct (Units.mk0 q ) b = 1) (n : ) (hn : n 0) :

            If the global Hilbert product equals $1$ on $(-1, b)$ and on every $(q, b)$ for $q$ prime, then by multiplicativity it equals $1$ on every $(n, b)$ for $n$ a positive integer. Proved by strong induction on $n$ using prime factorization.

            theorem hilbert_product_formula_bilinearity_reduction (a b : ˣ) (h1 : globalHilbertProduct (-1) (-1) = 1) (h2 : ∀ (q : ) (hq : Nat.Prime q), globalHilbertProduct (-1) (Units.mk0 q ) = 1) (h3 : ∀ (q : ) (hq : Nat.Prime q), have q' := Units.mk0 q ; globalHilbertProduct q' q' = 1) (h4 : ∀ (q : ) (hq : Nat.Prime q), q 2globalHilbertProduct (Units.mk0 2 ) (Units.mk0 q ) = 1) (h5 : ∀ (a b : ) (ha : Nat.Prime a) (hb : Nat.Prime b), a 2b 2a bglobalHilbertProduct (Units.mk0 a ) (Units.mk0 b ) = 1) :

            Reduces the global product formula to the case of generators. By bilinearity, the formula holds for all $a, b \in \mathbb{Q}^\times$ if it holds on the generators of $\mathbb{Q}^\times / (\mathbb{Q}^\times)^2$: namely $(-1, -1)$, $(-1, q)$, $(q, q)$, $(2, q)$, and $(p, q)$ for distinct odd primes $p, q$.

            (Theorem 10.11, case $a = -1$, $b = q$ prime) For any prime $q$, $\prod_v (-1, q)_v = 1$. The proof splits into the cases $q = 2$ (trivial) and $q$ odd (uses quadratic reciprocity via hilbert_product_neg_one_odd_prime_aux).

            theorem hilbert_product_prime_self (q : ) (hq : Nat.Prime q) :
            have q' := Units.mk0 q ; globalHilbertProduct q' q' = 1

            (Theorem 10.11, case $a = b = q$ prime) For any prime $q$, $\prod_v (q, q)_v = 1$. Reduces to $\prod_v (-1, q)_v = 1$ via Corollary 10.3 ($(c, c)_F = (-1, c)_F$).

            theorem hilbertAtPrime_two_q_eq_one_of_ne (q : ) (hq : Nat.Prime q) (hq_odd : q 2) (p : ) [Fact (Nat.Prime p)] (hp2 : p 2) (hpq : p q) :
            hilbertAtPrime p (Units.mk0 2 ) (Units.mk0 q ) = 1

            At an odd prime $p$ with $p \neq q$ (odd), both $2$ and $q$ are $p$-adic units, so $(2, q)_p = 1$ by Lemma 10.5.

            theorem hilbertAtInfty_two_q (q : ) (hq : Nat.Prime q) :
            hilbertAtInfty (Units.mk0 2 ) (Units.mk0 q ) = 1

            At the archimedean place, $(2, q)_\infty = 1$ for any prime $q$, since $2 > 0$.

            theorem hilbertAtPrime_two_q_at_q (q : ) (hq : Nat.Prime q) (hq_odd : q 2) (u : ℤ_[q]ˣ) :

            At the prime $q$ (odd), if $2 = u$ in $\mathbb{Z}_q^\times$, then by Lemma 10.8 $(2, q)_q = (q, u)_q = \left(\frac{u}{q}\right) = \left(\frac{2}{q}\right)$.

            At the prime $2$, the Hilbert symbol $(2, q)_2$ is computed by the $2$-adic formula (Theorem 10.9): one writes $2 = 2^1 \cdot 1$ and $q = 2^0 \cdot v$ for a $2$-adic unit $v$.

            The Legendre symbol $\left(\frac{2}{q}\right)$ equals $\chi_8(q)$, which is exactly what the $2$-adic Hilbert formula at $(1, q, 1, 0)$ computes. Hence $\left(\frac{2}{q}\right) \cdot \text{hilbert2Adic}(\ldots) = 1$.

            theorem hilbertAtPrime_two_q_product (q : ) (hq : Nat.Prime q) (hq_odd : q 2) :
            hilbertAtPrime q (Units.mk0 2 ) (Units.mk0 q ) * hilbertAtPrime 2 (Units.mk0 2 ) (Units.mk0 q ) = 1

            The product $(2, q)_q \cdot (2, q)_2 = 1$, the key cancellation in the proof that the global product $\prod_v (2, q)_v = 1$.

            theorem hilbert_product_two_odd_prime (q : ) (hq : Nat.Prime q) (hq_odd : q 2) :

            (Theorem 10.11, case $a = 2$, $b = q$ odd prime) For any odd prime $q$, $\prod_v (2, q)_v = 1$. Only $(2, q)_2$ and $(2, q)_q$ are non-trivial, and they cancel via the second supplementary law of quadratic reciprocity.

            theorem hilbert_qr_cancellation {a b : } (ha : Nat.Prime a) (hb : Nat.Prime b) (ha_odd : a 2) (hb_odd : b 2) (hab : a b) [instA : Fact (Nat.Prime a)] [instB : Fact (Nat.Prime b)] (u_a2 u_b2 : ℤ_[2]ˣ) (hu_a2 : ratToQpUnits 2 (Units.mk0 a ) = HilbertSymbol.unitZpToQp u_a2) (hu_b2 : ratToQpUnits 2 (Units.mk0 b ) = HilbertSymbol.unitZpToQp u_b2) (ub_a : ℤ_[a]ˣ) (hub_a : ratToQpUnits a (Units.mk0 b ) = HilbertSymbol.unitZpToQp ub_a) (ua_b : ℤ_[b]ˣ) (hua_b : ratToQpUnits b (Units.mk0 a ) = HilbertSymbol.unitZpToQp ua_b) :

            (The quadratic reciprocity cancellation) For distinct odd primes $a, b$, the product $\text{hilbert2Adic}(\bar a, \bar b, 0, 0) \cdot \left(\frac{b}{a}\right) \cdot \left(\frac{a}{b}\right) = 1$. This is the heart of the proof of the global product formula for $(a, b)$ with both $a$ and $b$ distinct odd primes, and is equivalent to the law of quadratic reciprocity.

            theorem hilbert_product_distinct_odd_primes (a b : ) (ha : Nat.Prime a) (hb : Nat.Prime b) (ha_odd : a 2) (hb_odd : b 2) (hab : a b) :
            globalHilbertProduct (Units.mk0 a ) (Units.mk0 b ) = 1

            (Theorem 10.11, case $a, b$ distinct odd primes) For distinct odd primes $a, b$, $\prod_v (a, b)_v = 1$. Only the primes $2$, $a$, and $b$ contribute; the product of these three local symbols equals $1$ by hilbert_qr_cancellation (quadratic reciprocity).

            (Textbook Theorem 10.11, Hilbert's Product Formula) For any two non-zero rationals $a, b \in \mathbb{Q}^\times$, the product of the local Hilbert symbols over all places is $1$: $$\prod_v (a, b)_v = 1$$ where the product ranges over $v = \infty$ and all prime places $v = p$. This is one of the deepest theorems of elementary number theory and is equivalent to the law of quadratic reciprocity.