Independence of the genus characters of a quadratic field

Let K = ℚ(√d) with d squarefree, and let D = P₁ ⋯ P_t be the prime-discriminant factorization of its fundamental discriminant. The genus characters χ_{P_i} are characters of the narrow class group Cl⁺(K) (genusCharFunNarrowClassGroupHom), and their product over all i is trivial on every class. This file proves that this is the only relation among them: every assignment of signs ε_i = ±1 with ∏ ε_i = 1 is the vector of values (χ_{P_i}(A))_i at some narrow class A. In other words the map Cl⁺(K) → {±1}^t they define hits the whole product-one hyperplane, which has 2^(t-1) elements.

This is the lower bound half of the genus-theoretic 2-rank formula for the narrow class group, rank₂ Cl⁺(K) ≥ t - 1; the matching upper bound is TauCeti.Multiquadratic.narrowTwoRank_le_ncard_ramifiedPrimes_sub_one. See D. A. Cox, Primes of the Form x² + ny², §3.B and §6.A, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

Main results

• TauCeti.Multiquadratic.exists_forall_genusCharFunNarrowClassGroupHom_singleton_eq: every sign pattern of product 1 on the prime discriminants of D is the value vector of the singleton genus characters at some narrow class.
• TauCeti.Multiquadratic.exists_forall_genusCharFunNarrowClassGroupHom_subset_eq: the same class has the prescribed product of signs as the value of every subset-indexed genus character.
• TauCeti.Multiquadratic.exists_genusCharFunElementaryTwoQuotientFamilyLinearMap_eq: the same statement for the ZMod 2-linear family on Cl⁺(K)/Cl⁺(K)², where the product-one condition becomes the vanishing of the coordinate sum.

theorem TauCeti.Multiquadratic.exists_forall_genusCharFunNarrowClassGroupHom_singleton_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) (ε : ℤ → ℤˣ) (hε : ∏ P ∈ s, ε P = 1) : ∃ (A : NumberField.NarrowClassGroup K), ∀ (P : ℤ) (hP : P ∈ s), (genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf ⋯) A = ε P

Every sign pattern of product one is attained by a narrow class. Let K = ℚ(√d) with d squarefree, let ∏ P ∈ s, P = fundamentalDiscriminant d be the prime-discriminant factorization, and let ε assign a sign to each P ∈ s with ∏ P ∈ s, ε P = 1. Then some narrow class A has χ_P(A) = ε P for every P ∈ s.

theorem TauCeti.Multiquadratic.exists_forall_genusCharFunNarrowClassGroupHom_subset_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) (ε : ℤ → ℤˣ) (hε : ∏ P ∈ s, ε P = 1) : ∃ (A : NumberField.NarrowClassGroup K), ∀ (t : Finset ℤ) (hts : t ⊆ s), (genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf hts) A = ∏ P ∈ t, ε P

Every sign pattern of product one is attained, on all subset characters at once. Under the hypotheses of exists_forall_genusCharFunNarrowClassGroupHom_singleton_eq, some narrow class A has χ_t(A) = ∏ P ∈ t, ε P for every subset t ⊆ s simultaneously.

theorem TauCeti.Multiquadratic.exists_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) (v : ↥s → Additive ℤˣ) (hv : ∑ P : ↥s, v P = 0) : ∃ (x : NumberField.NarrowClassGroup.ElementaryTwoQuotient K), (genusCharFunElementaryTwoQuotientFamilyLinearMap hs heven hprod hmin hgen hsf) x = v

Every sign vector of coordinate sum zero is a value of the genus characters. The linear form of exists_forall_genusCharFunNarrowClassGroupHom_singleton_eq: writing the sign group additively, the family of singleton genus characters on Cl⁺(K)/Cl⁺(K)² takes every value whose coordinates sum to zero.