10.5. How the reciprocity input is to be proved🔗

The intended source for Theorem 10.2.1 is the classical Furtwaengler–Kummer reciprocity argument, in the form developed by Ireland–Rosen. The already completed part of that source proves the integer-denominator Eisenstein reciprocity theorem.

Theorem10.5.1

uses 0used by 0✓L∃∀N

Ireland–Rosen integer reciprocity. Let \alpha\in\mathcal{O}_K be primary and prime to p, and let a\in\mathbb{Z} be nonzero, prime to p, and coprime to (\alpha). Then \left(\frac{\alpha}{(a)}\right)_p = \left(\frac{a}{(\alpha)}\right)_p .

Lean code for Theorem10.5.1●1 theorem

theoremdefined in BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/IrelandRosen/Theorem1/Part2.lean

complete

theorem BernoulliRegular.Furtwaengler.IrelandRosen.eisensteinReciprocity_theorem1.{u}
  (p : ℕ) [Fact (Nat.Prime p)] (hp_odd : Odd p) (K : Type u) [Field K]
  [NumberField K] [IsCyclotomicExtension {p} ℚ K]
  {α : NumberField.RingOfIntegers K} (a : ℤ)
  (hα_primary : BernoulliRegular.FLT37.IsPrimary p α)
  (hα_prime_to_p : BernoulliRegular.Furtwaengler.IsPrimeToP α)
  (ha : BernoulliRegular.Furtwaengler.IsCoprimeToPAndAlphaInt a α) :
  BernoulliRegular.Furtwaengler.pthSymbolAtInt_canonical α a =
    BernoulliRegular.Furtwaengler.pthSymbolAtIdeal_canonical
      ((algebraMap ℤ (NumberField.RingOfIntegers K)) a) (Ideal.span {α})

theorem BernoulliRegular.Furtwaengler.IrelandRosen.eisensteinReciprocity_theorem1.{u}
  (p : ℕ) [Fact (Nat.Prime p)]
  (hp_odd : Odd p) (K : Type u) [Field K]
  [NumberField K]
  [IsCyclotomicExtension {p} ℚ K]
  {α : NumberField.RingOfIntegers K}
  (a : ℤ)
  (hα_primary :
    BernoulliRegular.FLT37.IsPrimary p α)
  (hα_prime_to_p :
    BernoulliRegular.Furtwaengler.IsPrimeToP
      α)
  (ha :
    BernoulliRegular.Furtwaengler.IsCoprimeToPAndAlphaInt
      a α) :
  BernoulliRegular.Furtwaengler.pthSymbolAtInt_canonical
      α a =
    BernoulliRegular.Furtwaengler.pthSymbolAtIdeal_canonical
      ((algebraMap ℤ
          (NumberField.RingOfIntegers K))
        a)
      (Ideal.span {α})

Ireland--Rosen, Chapter 14, Section 2, Theorem 1, in the canonical
project residue-symbol notation.

Dictionary with the statement in Ireland--Rosen:
* `p`, `[Fact p.Prime]`, and `hp_odd` are the odd rational prime `p`.
* `K` with `[IsCyclotomicExtension {p} ℚ K]` is the cyclotomic field
  containing the `p`-th roots of unity; in Ireland--Rosen this is
  `ℚ(ζ_p)`.
* `α : 𝓞 K` is Ireland--Rosen's algebraic integer `α`.
* `hα_primary` is the primary hypothesis on `α`.
* `hα_prime_to_p` says `α` is nonzero and prime to the rational prime `p`.
* `a : ℤ` is Ireland--Rosen's rational integer denominator.
* `ha` says `a ≠ 0` and the ideal `(a)` is prime both to `(α)` and to `(p)`.

The conclusion is the equality `(α / a)_p = (a / α)_p`; the right-hand side is
written in project notation as the canonical ideal symbol with numerator
`a : 𝓞 K` and denominator the principal ideal `(α)`.

Proof for Theorem 10.5.1

uses 0

The proof follows the Gauss–Jacobi sum construction. For every prime ideal P\nmid p, one constructs an element \Phi(P) whose principal ideal is controlled by the Stickelberger element: (\Phi(P))=P^\theta. This is proved without assuming that P has residue degree one. The construction also supplies the semiprimary normalization, the conjugation-norm identity, and the Frobenius residue-symbol identity for \Phi(P).

For a general principal ideal (\alpha), take the product over the prime factorization of (\alpha): \Phi(\alpha)= \prod_{P\mid(\alpha)}\Phi(P)^{v_P((\alpha))}. The Stickelberger identities multiply to give (\Phi(\alpha))=(\alpha^\theta). Hence \Phi(\alpha)=\varepsilon\,\alpha^\theta for a unit \varepsilon. The primary-unit lemma says that when \alpha is primary, this unit contributes only a sign, and a sign has trivial p-th-power residue symbol because p is odd.

Combining the product identity, the primary-unit cancellation, and the denominator norm calculation gives the ideal-norm reciprocity formula. Taking the denominator ideal to be (a) gives the displayed integer reciprocity law.

To finish the reflection route one still has to pass from this integer-denominator theorem to the full one-sided principal reciprocity statement of Theorem 10.2.1. The missing step is not a new reflection theorem; it is the remaining principal-denominator reciprocity argument that allows a general coprime principal denominator (\beta) in place of a rational integer denominator (a), with the local-primary hypothesis on the numerator preserved throughout.