Primitive Dirichlet characters of prime discriminants

A prime discriminant P determines a real quadratic Dirichlet character of level |P|, the Kronecker character TauCeti.kroneckerChar of P. This file names it primeDiscriminantChar P hP, identifies its values with the function primeDiscriminantCharFun P, and proves that its conductor is exactly |P|.

For the three even prime discriminants this is Mathlib's ZMod.χ₄, ZMod.χ₈, or ZMod.χ₈'. For an odd prime discriminant p*, it is the quadratic character of ZMod p, equivalently the Legendre symbol (· / p). Primitivity at an odd prime level follows from nontriviality. At levels 4 and 8, the values at 1 and respectively 3 or 5 show that the character cannot descend to a proper divisor of its level.

These primitive characters are the character-theoretic input for the conductor-minimality part of the quadratic Kronecker--Weber theorem: Mathlib's cyclotomic Galois correspondence detects a subfield by the conductors of its associated Dirichlet characters.

The description is classical; see K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6.

Main definitions and results

• TauCeti.Multiquadratic.primeDiscriminantChar: the Dirichlet character of level |P| attached to the prime discriminant P.
• TauCeti.Multiquadratic.primeDiscriminantChar_apply_int: its value on an integer is primeDiscriminantCharFun P.
• TauCeti.Multiquadratic.isQuadratic_primeDiscriminantChar: it takes only the values 0, 1, -1.
• TauCeti.Multiquadratic.isPrimitive_primeDiscriminantChar: its conductor is |P|.

def TauCeti.Multiquadratic.primeDiscriminantChar (P : ℤ) (hP : IsPrimeDiscriminant P) : DirichletCharacter ℤ P.natAbs

The real quadratic Dirichlet character attached to a prime discriminant. It is the Kronecker character (P / ·) of level |P|. At -4, 8, and -8 this is respectively ZMod.χ₄, ZMod.χ₈, and ZMod.χ₈'; at an odd prime discriminant p* it is the quadratic character modulo p.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantChar_apply_int (P : ℤ) (hP : IsPrimeDiscriminant P) (n : ℤ) : (primeDiscriminantChar P hP) ↑n = primeDiscriminantCharFun P n

The bundled character evaluates to the unbundled prime-discriminant character on integers.

theorem TauCeti.Multiquadratic.primeDiscriminantChar_ne_one (P : ℤ) (hP : IsPrimeDiscriminant P) : primeDiscriminantChar P hP ≠ 1

The character attached to a prime discriminant is nontrivial.

theorem TauCeti.Multiquadratic.isQuadratic_primeDiscriminantChar (P : ℤ) (hP : IsPrimeDiscriminant P) : MulChar.IsQuadratic (primeDiscriminantChar P hP)

The Dirichlet character attached to a prime discriminant is quadratic.

theorem TauCeti.Multiquadratic.isPrimitive_primeDiscriminantChar (P : ℤ) (hP : IsPrimeDiscriminant P) : (primeDiscriminantChar P hP).IsPrimitive

The Dirichlet character of a prime discriminant is primitive. Its conductor is exactly the absolute value of the prime discriminant.