Documentation

TauCeti.NumberTheory.Multiquadratic.Legendre.PrimeDiscriminant.Character

The character attached to a prime discriminant #

Genus theory attaches to a prime discriminant P the primitive real character modulo |P| cutting out the quadratic field ℚ(√P). Mathlib has no Kronecker symbol, so this file assembles that character from the pieces Mathlib does have: it is ZMod.χ₄, ZMod.χ₈ and ZMod.χ₈' at the three even prime discriminants -4, 8 and -8, and the Legendre symbol (· / p), written as a Jacobi symbol, at an odd prime discriminant p* = ±p.

primeDiscriminantCharFun_mul_right and primeDiscriminantCharFun_eq_one_or_eq_neg_one record that it is a ±1-valued completely multiplicative function on the integers coprime to P, and primeDiscriminantCharFun_mod_right' that its value depends only on the residue class modulo |P|. The rest of this directory studies the Legendre symbols legendreSym q P of prime discriminants at an odd prime q; primeDiscriminantCharFun_eq_legendreSym identifies the character with them, so the splitting laws proved there are statements about the character.

The genus characters of a fundamental discriminant — the products of these characters over the prime discriminants of a factorization D = P₁ ⋯ P_t — are built on this in TauCeti.NumberTheory.Multiquadratic.Quadratic.GenusCharacter.Basic. The material is classical; see D. A. Cox, Primes of the Form x² + ny², §3.B, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

Main definitions #

Main results #

The character attached to a prime discriminant #

source
def TauCeti.Multiquadratic.primeDiscriminantCharFun (P n : ℤ) :
ℤ

The real quadratic character attached to a prime discriminant P: the primitive character modulo |P| cutting out the quadratic field ℚ(√P). At the even prime discriminants -4, 8 and -8 it is ZMod.χ₄, ZMod.χ₈ and ZMod.χ₈'; at an odd prime discriminant p* it is the Legendre symbol (· / p), written as a Jacobi symbol. The value at an integer sharing a factor with P is 0.

The function is total: the prime-discriminant hypothesis is not bundled into it, but is carried by the API below, which supplies the facts specific to prime discriminants.

Equations
Instances For
    source
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_def (P n : ℤ) :
    primeDiscriminantCharFun P n = if P = -4 then ZMod.χ₄ ↑n else if P = 8 then ZMod.χ₈ ↑n else if P = -8 then ZMod.χ₈' ↑n else jacobiSym n P.natAbs

    The defining four-case description of the character attached to a prime discriminant.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_neg_four (n : ℤ) :
    primeDiscriminantCharFun (-4) n = ZMod.χ₄ ↑n

    The character of the prime discriminant -4 is ZMod.χ₄.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eight (n : ℤ) :
    primeDiscriminantCharFun 8 n = ZMod.χ₈ ↑n

    The character of the prime discriminant 8 is ZMod.χ₈.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_neg_eight (n : ℤ) :
    primeDiscriminantCharFun (-8) n = ZMod.χ₈' ↑n

    The character of the prime discriminant -8 is ZMod.χ₈'.

    source
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_jacobiSym_of_not_isEvenPrimeDiscriminant {P : ℤ} (hP : ¬IsEvenPrimeDiscriminant P) (n : ℤ) :
    primeDiscriminantCharFun P n = jacobiSym n P.natAbs

    Away from the three even prime discriminants the character is a Jacobi symbol.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_oddPrimeDiscriminant {p : ℕ} (hodd : Odd p) (n : ℤ) :
    primeDiscriminantCharFun (oddPrimeDiscriminant p) n = jacobiSym n p

    The character of the odd prime discriminant p* is the Legendre symbol (· / p). In particular it depends only on p, not on the sign normalization p* = (-1) ^ ((p - 1) / 2) * p.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_mul_right (P m n : ℤ) :
    primeDiscriminantCharFun P (m * n) = primeDiscriminantCharFun P m * primeDiscriminantCharFun P n

    The character attached to a prime discriminant is completely multiplicative.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_one (P : ℤ) :
    primeDiscriminantCharFun P 1 = 1

    The character attached to a prime discriminant takes the value 1 at 1.

    source
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_mod_right' {P m n : ℤ} (h : m % ↑P.natAbs = n % ↑P.natAbs) :
    primeDiscriminantCharFun P m = primeDiscriminantCharFun P n

    The character attached to P depends only on the residue class modulo |P|.

    source
    theorem TauCeti.Multiquadratic.isCoprime_evenPrimeDiscriminant_iff_not_two_dvd {P n : ℤ} (hP : IsEvenPrimeDiscriminant P) :
    IsCoprime n P ↔ ¬2 ∣ n

    An integer is coprime to an even prime discriminant exactly when it is odd: the only prime dividing -4, 8 or -8 is 2.

    source
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_one_or_eq_neg_one {P n : ℤ} (hP : IsPrimeDiscriminant P) (hcop : IsCoprime n P) :
    primeDiscriminantCharFun P n = 1 ∨ primeDiscriminantCharFun P n = -1

    The character attached to a prime discriminant takes the values ±1 on the integers coprime to it.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_zero_iff {P n : ℤ} (hP : IsPrimeDiscriminant P) :
    primeDiscriminantCharFun P n = 0 ↔ ¬IsCoprime n P

    The character attached to a prime discriminant vanishes exactly on the integers that are not coprime to it.

    source
    theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_legendreSym {P : ℤ} (hP : IsPrimeDiscriminant P) {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) :
    primeDiscriminantCharFun P ↑q = legendreSym q P

    The character attached to a prime discriminant P agrees at an odd prime q with the Legendre symbol legendreSym q P, the splitting symbol of P at q studied in TauCeti.NumberTheory.Multiquadratic.Legendre.PrimeDiscriminant.Basic and TauCeti.NumberTheory.Multiquadratic.Legendre.EvenPrimeDiscriminant.

    Nontriviality #

    source
    theorem TauCeti.Multiquadratic.exists_primeDiscriminantCharFun_eq_neg_one {P : ℤ} (hP : IsPrimeDiscriminant P) :
    ∃ (a : ℕ), primeDiscriminantCharFun P ↑a = -1

    The character of a prime discriminant is nontrivial. For every prime discriminant P, some natural number has character -1 at P.

    source
    theorem TauCeti.Multiquadratic.exists_primeDiscriminantCharFun_eq {P : ℤ} (hP : IsPrimeDiscriminant P) (ε : ℤˣ) :
    ∃ (a : ℕ), primeDiscriminantCharFun P ↑a = ↑ε

    The character attached to a prime discriminant takes each of the values ±1 at some natural number.