Primitive Dirichlet characters from prime-discriminant products

genusChar bundles the existing integer-valued genusCharFun as a Dirichlet character at the absolute value of the product of its prime discriminants. When at most one factor is even, this character is primitive. Thus the quadratic character of a fundamental discriminant D has conductor |D|, the character-theoretic input for identifying the least cyclotomic level of its quadratic field.

The construction is the whole-family case of genusCharAtLevel, which lifts the primitive prime-discriminant characters to the common level |∏ P ∈ s, P| and multiplies those indexed by a subset: genusChar s hs is genusCharAtLevel s hs Finset.univ. Distinct factors, with at most one even factor, have coprime absolute values, so their conductors multiply (conductor_genusCharAtLevel), which is what makes the whole product primitive. The empty factorization gives the trivial character at level one.

The character description follows K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6, and D. A. Cox, Primes of the Form x² + ny², §3.B.

noncomputable def TauCeti.Multiquadratic.genusChar (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : DirichletCharacter ℤ (∏ P ∈ s, P).natAbs

The product of the prime-discriminant characters, at the absolute value of the product of the discriminants. Its value on integers is genusCharFun.

@[simp]

theorem TauCeti.Multiquadratic.genusCharAtLevel_univ (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : genusCharAtLevel s hs s.attach = genusChar s hs

The character indexed by the whole family is the genus character of that family.

theorem TauCeti.Multiquadratic.genusChar_def (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : genusChar s hs = ∏ P : ↥s, primeDiscriminantCharAtLevel s hs P

The expression for genusChar in terms of prime-discriminant characters at a common level.

@[simp]

theorem TauCeti.Multiquadratic.genusChar_apply_int (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (n : ℤ) : (genusChar s hs) ↑n = genusCharFun s n

The bundled genus character agrees with the existing character function on every integer, including integers not coprime to the level.

theorem TauCeti.Multiquadratic.isPrimitive_genusChar {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) : (genusChar s hs).IsPrimitive

A product of distinct prime-discriminant characters with at most one even factor is primitive: its conductor is the absolute value of the product of the discriminants.