2607.20408v1 / Repro/QuadraticCharacters.lean

all files

import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

/-!
# Jacobi-symbol Dirichlet characters for the reproduction

Mathlib has the Jacobi symbol and Dirichlet L-functions, but does not currently
bundle the Jacobi symbol for a general odd modulus as a Dirichlet character.  This
file supplies that bridge for positive moduli greater than one.
-/

open NumberTheorySymbols

namespace ExtremeValues

/-- The Jacobi symbol `n ↦ J(n | q)`, bundled as an integer-valued Dirichlet character. -/
def jacobiCharacterInt (q : ℕ) (hq : 1 < q) : DirichletCharacter ℤ q where
  toFun a := J((a.val : ℤ) | q)
  map_one' := by
    rw [ZMod.val_one'' hq.ne']
    exact jacobiSym.one_left q
  map_mul' a b := by
    rw [ZMod.val_mul]
    rw [show (((a.val * b.val) % q : ℕ) : ℤ) =
        ((a.val * b.val : ℕ) : ℤ) % (q : ℤ) by exact Int.natCast_emod _ _]
    rw [← jacobiSym.mod_left ((a.val * b.val : ℕ) : ℤ) q]
    exact jacobiSym.mul_left a.val b.val q
  map_nonunit' a ha := by
    letI : NeZero q := ⟨by omega⟩
    rw [jacobiSym.eq_zero_iff_not_coprime]
    intro hgcd
    apply ha
    rw [← ZMod.natCast_zmod_val a, ZMod.isUnit_iff_coprime,
      Nat.coprime_iff_gcd_eq_one]
    rw [Int.gcd_def, Int.natAbs_natCast, Int.natAbs_natCast] at hgcd
    exact hgcd

/-- The complex-valued character used to define its Dirichlet L-function. -/
def jacobiCharacter (q : ℕ) (hq : 1 < q) : DirichletCharacter ℂ q :=
  (jacobiCharacterInt q hq).ringHomComp (Int.castRingHom ℂ)

/-- The analytically continued Dirichlet L-function of the Jacobi character. -/
noncomputable def jacobiLFunction (q : ℕ) (hq : 1 < q) : ℂ → ℂ :=
  letI : NeZero q := ⟨Nat.ne_of_gt (zero_lt_one.trans hq)⟩
  DirichletCharacter.LFunction (jacobiCharacter q hq)

@[simp]
theorem jacobiCharacterInt_apply_nat (q n : ℕ) (hq : 1 < q) :
    jacobiCharacterInt q hq n = J(n | q) := by
  change J(((n : ZMod q).val : ℕ) | q) = J(n | q)
  rw [ZMod.val_natCast]
  rw [show (((n % q : ℕ) : ℤ)) = (n : ℤ) % (q : ℤ) by exact Int.natCast_emod _ _]
  exact (jacobiSym.mod_left n q).symm

@[simp]
theorem jacobiCharacter_apply_nat (q n : ℕ) (hq : 1 < q) :
    jacobiCharacter q hq n = (J(n | q) : ℂ) := by
  simp [jacobiCharacter, jacobiCharacterInt_apply_nat]

/-- The bundled character really is quadratic: all its values are `0`, `1`, or `-1`. -/
theorem jacobiCharacter_isQuadratic (q : ℕ) (hq : 1 < q) :
    (jacobiCharacter q hq).IsQuadratic := by
  apply MulChar.IsQuadratic.comp (χ := jacobiCharacterInt q hq)
  · intro a
    exact jacobiSym.trichotomy a.val q

/--
For a positive modulus congruent to `1 mod 4`, quadratic reciprocity identifies
the character value with the naive symbol `(q/n)` at odd positive `n`.
-/
theorem jacobiCharacter_eq_symbol_of_one_mod_four
    {q n : ℕ} (hq : 1 < q) (hq4 : q % 4 = 1) (hn : Odd n) :
    jacobiCharacter q hq n = (J(q | n) : ℂ) := by
  rw [jacobiCharacter_apply_nat]
  norm_cast
  exact jacobiSym.quadratic_reciprocity_one_mod_four' hn hq4

end ExtremeValues