Documentation

TauCeti.NumberTheory.Multiquadratic.Legendre.PrimeDiscriminant.Dirichlet.Basic

Primes with prescribed prime-discriminant characters #

Let P₁, …, P_t be distinct prime discriminants, at most one of them even, and let a sign ε_i = ±1 be assigned to each. Then there are infinitely many primes q at which the characters attached to the P_i take exactly the prescribed values, χ_{P_i}(q) = ε_i for every i. More generally, arbitrary signs can be prescribed at some natural number whenever the family does not contain all three even prime discriminants. This is the arithmetic input that makes the genus characters of a quadratic field independent: the lower bound t - 1 on the 2-rank of the narrow class group of ℚ(√d) comes from realising every sign pattern of product 1 by the class of a prime ideal of degree one, and this file supplies the rational prime under that ideal.

Three facts combine. Each character χ_P is nontrivial, so it takes the value -1 somewhere; the moduli |P_i| of distinct prime discriminants are pairwise coprime, so the Chinese remainder theorem produces one residue class with all the prescribed values at once; and Dirichlet's theorem on primes in arithmetic progressions (Nat.forall_exists_prime_gt_and_zmodEq) places a prime, larger than any given bound, in that class.

The statement is classical; see D. A. Cox, Primes of the Form x² + ny², §3.B (the proof of Theorem 3.15), and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

The nontriviality of a single character (exists_primeDiscriminantCharFun_eq) and the coprimality of distinct prime discriminants (isCoprime_primeDiscriminant_of_ne_of_not_both_even) are supplied by TauCeti.NumberTheory.Multiquadratic.Legendre.PrimeDiscriminant.Character and TauCeti.NumberTheory.Multiquadratic.Prime.Discriminants.

Main results #

Prescribing several characters at once #

source
theorem TauCeti.Multiquadratic.exists_forall_primeDiscriminantCharFun_eq_of_not_all_three_even {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hnoall : ¬(-4 ∈ s ∧ 8 ∈ s ∧ -8 ∈ s)) (ε : ℤ → ℤˣ) :
∃ (a : ℕ), ∀ P ∈ s, primeDiscriminantCharFun P ↑a = ↑(ε P)

Prescribing a square-class independent family of prime-discriminant characters. If s does not contain all three even prime discriminants, then every assignment of signs to s is attained simultaneously by the characters attached to its members.

source
theorem TauCeti.Multiquadratic.exists_forall_primeDiscriminantCharFun_eq {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) (ε : ℤ → ℤˣ) :
∃ (a : ℕ), ∀ P ∈ s, primeDiscriminantCharFun P ↑a = ↑(ε P)

Prescribing the characters of finitely many prime discriminants. Let s be a finite set of prime discriminants, at most one of them even, and let ε assign a sign to each. Then some natural number a has χ_P(a) = ε P for every P ∈ s.

source
theorem TauCeti.Multiquadratic.exists_prime_gt_forall_primeDiscriminantCharFun_eq {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) (ε : ℤ → ℤˣ) (N : ℕ) :
∃ (q : ℕ), N < q ∧ Nat.Prime q ∧ q ≠ 2 ∧ ∀ P ∈ s, primeDiscriminantCharFun P ↑q = ↑(ε P)

Dirichlet's theorem for prime-discriminant characters. Let s be a finite set of prime discriminants, at most one of them even, let ε assign a sign to each, and let N be any bound. Then some odd prime q > N has χ_P(q) = ε P for every P ∈ s. In particular there are infinitely many such primes.