The principal genus theorem

Let K = ℚ(√d) with d squarefree and let D = ∏ P ∈ s, P be the prime-discriminant factorization of the fundamental discriminant of d, so that t = #s is the number of rational primes ramifying in K. The t genus characters χ_P assemble into a ZMod 2-linear map

Φ : Cl⁺(K) / Cl⁺(K)² → (P ∈ s) → {±1}

(genusCharFunElementaryTwoQuotientFamilyLinearMap). Two facts about Φ are already available: its image contains every sign vector whose coordinates sum to zero (exists_genusCharFunElementaryTwoQuotientFamilyLinearMap_eq, the Dirichlet-theorem input), and the source has dimension exactly t - 1 (narrowTwoRank_eq_ncard_ramifiedPrimes_sub_one). Since the sum-zero hyperplane has the same dimension t - 1, no room is left over: Φ is injective and its image is exactly that hyperplane.

Injectivity is the principal genus theorem: a narrow ideal class on which every genus character is trivial — a class in the principal genus — is a square. Together with the description of the image it says that the genus characters are a complete and independent system of invariants for narrow ideal classes modulo squares.

See D. A. Cox, Primes of the Form x² + ny², §3.B (Theorem 3.15 and its corollaries), and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

Main results

• TauCeti.Multiquadratic.mem_range_genusCharFunElementaryTwoQuotientFamilyLinearMap_iff: the sign vectors realized by the genus characters are exactly those of coordinate sum zero.
• TauCeti.Multiquadratic.genusCharFunElementaryTwoQuotientFamilyLinearMap_injective: the genus characters separate the classes of Cl⁺(K)/Cl⁺(K)².
• TauCeti.Multiquadratic.isSquare_iff_forall_genusCharFunNarrowClassGroupHom_eq_one: the principal genus theorem, a narrow ideal class is a square exactly when all its genus characters are trivial.

The image and the kernel of the genus-character family

theorem TauCeti.Multiquadratic.mem_range_genusCharFunElementaryTwoQuotientFamilyLinearMap_iff {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 ℤˣ) : v ∈ (genusCharFunElementaryTwoQuotientFamilyLinearMap hs heven hprod hmin hgen hsf).range ↔ ∑ P : ↥s, v P = 0

The genus characters realize exactly the sign vectors of product one. For K = ℚ(√d) with d squarefree and ∏ P ∈ s, P = fundamentalDiscriminant d a prime-discriminant factorization, a sign vector indexed by s is a value of the family of singleton genus characters on Cl⁺(K)/Cl⁺(K)² exactly when its coordinates sum to zero — that is, exactly when the product of its signs is 1.

The inclusion "⊇" is the Dirichlet-theorem input exists_genusCharFunElementaryTwoQuotientFamilyLinearMap_eq; the inclusion "⊆" holds because Cl⁺(K)/Cl⁺(K)² has dimension #s - 1, leaving no room beyond the hyperplane.

theorem TauCeti.Multiquadratic.genusCharFunElementaryTwoQuotientFamilyLinearMap_injective {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) : Function.Injective ⇑(genusCharFunElementaryTwoQuotientFamilyLinearMap hs heven hprod hmin hgen hsf)

The genus characters separate narrow classes modulo squares. The ZMod 2-linear family of singleton genus characters is injective on Cl⁺(K)/Cl⁺(K)². Equivalently, the #s genus characters span the full dual of Cl⁺(K)/Cl⁺(K)².

The principal genus theorem

theorem TauCeti.Multiquadratic.isSquare_iff_forall_genusCharFunNarrowClassGroupHom_eq_one {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) (A : NumberField.NarrowClassGroup K) : IsSquare A ↔ ∀ (P : ℤ) (hP : P ∈ s), (genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf ⋯) A = 1

The principal genus theorem. Let K = ℚ(√d) with d squarefree and let ∏ P ∈ s, P = fundamentalDiscriminant d be the prime-discriminant factorization of its discriminant. A narrow ideal class of K is a square exactly when every genus character is trivial on it; that is, the principal genus is the group of squares.

This is the classical statement that the genus characters cut out Cl⁺(K)² inside Cl⁺(K).