Genus characters at a split prime

Let K = ℚ(√d) with d squarefree, and let D = ∏ P ∈ s, P be a factorization of its discriminant into prime discriminants. At an odd prime q the genus character of the whole factorization is the splitting symbol of K,

genusCharFun s q = legendreSym q d

(genusCharFun_natCast_eq_legendreSym). Two consequences follow. First, the quadratic splitting law reads: q splits in K exactly when its genus character is trivial. Second — the point of the file — a split prime carries the prescribed character values into the narrow class group: a prime 𝔮 of 𝓞 K above a split q has absolute norm q, so its narrow ideal class [𝔮] ∈ Cl⁺(K) satisfies

χ_P([𝔮]) = primeDiscriminantCharFun P q for every P ∈ s,

and the same values are taken by the ZMod 2-linear family on Cl⁺(K)/Cl⁺(K)². This is the mechanism by which a sign pattern prescribed at a rational prime is realized by a narrow ideal class.

The classical account is in D. A. Cox, Primes of the Form x² + ny², §3.B, and F. Lemmermeyer, Reciprocity Laws, §2.2. The splitting law itself, the genus characters, and their descent to the narrow class group are the preceding Tau Ceti modules.

Main results

• ncard_primesOver_eq_finrank_iff_genusCharFun_eq_one: q splits in K exactly when its genus character is trivial.
• exists_forall_genusCharFunNarrowClassGroupHom_eq: a narrow ideal class realizing the prime-discriminant character values of a split prime.
• exists_forall_genusCharFunElementaryTwoQuotientFamilyLinearMap_eq: the same values in the linear family on Cl⁺(K)/Cl⁺(K)².

theorem TauCeti.Multiquadratic.ncard_primesOver_eq_finrank_iff_genusCharFun_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : ((Ideal.span {↑q}).primesOver (NumberField.RingOfIntegers K)).ncard = Module.finrank ℚ K ↔ genusCharFun s ↑q = 1

The quadratic splitting law in genus-character form. An odd prime q splits in K = ℚ(√d) for squarefree d exactly when the genus character of the whole prime-discriminant factorization of disc K is trivial at q.

theorem TauCeti.Multiquadratic.exists_forall_genusCharFunNarrowClassGroupHom_eq {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) (hgc : genusCharFun s ↑q = 1) : ∃ (A : NumberField.NarrowClassGroup K), ∀ (P : ℤ) (hP : P ∈ s), ↑((genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf ⋯) A) = primeDiscriminantCharFun P ↑q

The narrow class of a split prime realizes the prescribed character values. Let D = ∏ P ∈ s, P be a prime-discriminant factorization of the discriminant of K = ℚ(√d) and let q be an odd prime with trivial genus character. Then q splits in K, and the narrow ideal class of a prime of 𝓞 K above q has, at each P ∈ s, exactly the value primeDiscriminantCharFun P q.

theorem TauCeti.Multiquadratic.exists_forall_genusCharFunElementaryTwoQuotientFamilyLinearMap_eq {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) (hgc : genusCharFun s ↑q = 1) : ∃ (x : NumberField.NarrowClassGroup.ElementaryTwoQuotient K), ∀ (P : ↥s), ↑(Additive.toMul ((genusCharFunElementaryTwoQuotientFamilyLinearMap hs heven hprod hmin hgen hsf) x P)) = primeDiscriminantCharFun ↑P ↑q

The linear family on Cl⁺(K)/Cl⁺(K)² realizes the character values of a split prime. The elementary-2 form of exists_forall_genusCharFunNarrowClassGroupHom_eq: the vector of prime-discriminant characters of a split prime q lies in the image of the linear family of singleton genus characters.