The ramified primes of an imaginary quadratic field span exactly 2 ^ (t - 1) classes

Let K = ℚ(√d) be an imaginary quadratic field, presented by θ : 𝓞 K with minpoly ℤ θ = X ^ 2 - d for a squarefree d < -1, and let t be the number of rational primes ramifying in K. The classes [𝔭_p] of the primes above the ramified primes are 2-torsion (NumberField.classGroupMk0_sq_eq_one_of_mem_ramifiedPrimes) and satisfy the relation ∏_{p ∣ d} [𝔭_p] = 1 (prod_classGroupMk0_eq_one), which bounds the subgroup they generate by 2 ^ (t - 1) elements (natCard_closure_image_classGroupMk0_le). This file supplies the matching lower bound, so that subgroup has exactly 2 ^ (t - 1) elements, and reads off the genus-theoretic lower bound 2-rank Cl(K) ≥ t - 1.

The content is that there is no relation beyond the known one. A relation is a subset S of the ramified primes with ∏_{p ∈ S} 𝔭_p principal; taking absolute norms, a generator z of that product has |N(z)| = ∏_{p ∈ S} p, and since d < 0 the norm form of K is positive definite, so N(z) = ∏_{p ∈ S} p on the nose. Writing n = |d|, the norm form is (A² + n B²)/4 in general and A² + n B² when d ≢ 1 (mod 4) (NumberField.exists_sq_sub_mul_sq_eq_four_mul_norm and NumberField.exists_sq_sub_mul_sq_eq_norm_of_mod_four_ne_one). The product m = ∏_{p ∈ S} p is a squarefree divisor of the discriminant, hence of n when d ≡ 1 (mod 4) (where disc K = d is odd) and of 2n otherwise (where disc K = 4d). Positive definiteness then leaves very little room: if the B-coordinate vanishes, m is a square and so m = 1; if it does not, then m ≥ n/4 resp. m ≥ n, and the few surviving ratios n/m are excluded one by one. The upshot is m = 1 or m = n, that is, S = ∅ or S is the set of prime factors of d.

Counting is then immediate: fix a prime factor q of d. If two subsets of the ramified primes avoiding q have the same product of classes, their symmetric difference is a relation, and it too avoids q; so it is not the set of prime factors of d, which contains q, leaving only the empty relation — that is, the two subsets are equal. Distinct such subsets therefore have distinct products of classes.

The radicand d = -1 is genuinely excluded, not merely for convenience: there t = 1 and the single ramified prime 2 has the principal prime (1 + i) above it, so the relation used here (which lives on the prime factors of d) is empty while the classes still collapse. The bound 2-rank ≥ t - 1 = 0 is vacuous in that case anyway.

For the ordinary class group of a real quadratic field the analogous statement is false — ℚ(√3) has t = 2 and class number 1 — which is why genus theory states the t - 1 formula for the narrow class group there; only the imaginary case, where narrow and ordinary agree, is treated here.

The classical source is D. A. Cox, Primes of the Form x² + ny², §6.A, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2, where this is the lower-bound half of the ambiguous class number formula.

Main results

In the namespace TauCeti.Multiquadratic:

• prod_eq_one_or_prod_eq_natAbs_of_isPrincipal_prod: a principal product of ramified primes has ∏_{p ∈ s} p equal to 1 or to |d|.
• eq_empty_or_eq_primeFactors_of_prod_classGroupMk0_eq_one: the class-group form — a trivial product of ramified-prime classes is indexed by ∅ or by the prime factors of d.
• two_pow_le_natCard_closure_image_classGroupMk0 and natCard_closure_image_classGroupMk0_eq: the classes of the ramified primes generate a subgroup of order exactly 2 ^ (t - 1).
• card_sub_one_le_twoRank and ncard_ramifiedPrimes_sub_one_le_twoRank: hence 2-rank Cl(𝓞 K) ≥ t - 1.

theorem TauCeti.Multiquadratic.prod_eq_one_or_prod_eq_natAbs_of_isPrincipal_prod {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd : d < -1) {s : Finset ℕ} (P : ℕ → Ideal (NumberField.RingOfIntegers K)) (hram : ∀ p ∈ s, p ∈ NumberField.ramifiedPrimes K) (hprime : ∀ p ∈ s, (P p).IsPrime) (hover : ∀ p ∈ s, (P p).LiesOver (Ideal.span {↑p})) (hprin : (∏ p ∈ s, P p).IsPrincipal) : ∏ p ∈ s, p = 1 ∨ ∏ p ∈ s, p = d.natAbs

The only principal products of ramified primes are the two obvious ones. Let K = ℚ(√d) be an imaginary quadratic field with d < -1 squarefree, and let s be a finite set of ramified rational primes with P p the prime of 𝓞 K above p ∈ s. If ∏_{p ∈ s} 𝔭_p is principal, then ∏_{p ∈ s} p is 1 (forcing s = ∅) or |d| (the known relation span_singleton_eq_prod_primeFactors, which comes from θ itself).

This is the arithmetic heart of the genus-theoretic 2-rank formula: the classes of the ramified primes satisfy no relation beyond the one already known. The proof takes absolute norms — a generator z of the product has |N(z)| = ∏_{p ∈ s} p — and then reads off the possibilities from the norm form of K, which is positive definite because d < 0. Whether the 2 in the discriminant is available as a ramified prime is exactly the d mod 4 split: for d ≡ 1 (mod 4) the norm form is (A² + |d|B²)/4 and ∏_{p ∈ s} p divides |d|, while otherwise the form is A² + |d|B² and the product divides 2|d|.

theorem TauCeti.Multiquadratic.eq_empty_or_eq_primeFactors_of_prod_classGroupMk0_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (Q : ℕ → ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd : d < -1) {s : Finset ℕ} (hram : ∀ p ∈ s, p ∈ NumberField.ramifiedPrimes K) (hprime : ∀ p ∈ s, (↑(Q p)).IsPrime) (hover : ∀ p ∈ s, (↑(Q p)).LiesOver (Ideal.span {↑p})) (h : ∏ p ∈ s, ClassGroup.mk0 (Q p) = 1) : s = ∅ ∨ s = d.natAbs.primeFactors

The classes of the ramified primes satisfy only the known relation. For K = ℚ(√d) with d < -1 squarefree and s a finite set of ramified rational primes, a trivial product ∏_{p ∈ s} [𝔭_p] = 1 of their classes forces s to be empty or to be the whole set of prime factors of d — the relation of prod_classGroupMk0_eq_one.

theorem TauCeti.Multiquadratic.two_pow_le_natCard_closure_image_classGroupMk0 {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (Q : ℕ → ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd : d < -1) {s : Finset ℕ} (hram : ∀ p ∈ s, p ∈ NumberField.ramifiedPrimes K) (hprime : ∀ p ∈ s, (↑(Q p)).IsPrime) (hover : ∀ p ∈ s, (↑(Q p)).LiesOver (Ideal.span {↑p})) (hs : d.natAbs.primeFactors ⊆ s) : 2 ^ (s.card - 1) ≤ Nat.card ↥(Subgroup.closure ((fun (p : ℕ) => ClassGroup.mk0 (Q p)) '' ↑s))

The ramified primes of an imaginary quadratic field span at least 2 ^ (t - 1) classes. Complementing natCard_closure_image_classGroupMk0_le: with s a finite set of ramified primes containing every prime factor of d < -1, the sub-products ∏_{p ∈ S} [𝔭_p] over subsets S of s avoiding one chosen prime factor q of d are pairwise distinct: if two of them agree, the symmetric difference of the two index sets is a relation avoiding q, so it is not the set of prime factors of d, and eq_empty_or_eq_primeFactors_of_prod_classGroupMk0_eq_one leaves only the empty relation, forcing the two index sets to be equal.

theorem TauCeti.Multiquadratic.natCard_closure_image_classGroupMk0_eq {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (Q : ℕ → ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd : d < -1) {s : Finset ℕ} (hram : ∀ p ∈ s, p ∈ NumberField.ramifiedPrimes K) (hprime : ∀ p ∈ s, (↑(Q p)).IsPrime) (hover : ∀ p ∈ s, (↑(Q p)).LiesOver (Ideal.span {↑p})) (hs : d.natAbs.primeFactors ⊆ s) : Nat.card ↥(Subgroup.closure ((fun (p : ℕ) => ClassGroup.mk0 (Q p)) '' ↑s)) = 2 ^ (s.card - 1)

The ramified primes of an imaginary quadratic field span exactly 2 ^ (t - 1) classes. For K = ℚ(√d) with d < -1 squarefree and s a finite set of ramified rational primes containing every prime factor of d, the subgroup of Cl(𝓞 K) generated by the classes of the primes above the members of s has exactly 2 ^ (#s - 1) elements: the upper bound is natCard_closure_image_classGroupMk0_le, and the lower bound is two_pow_le_natCard_closure_image_classGroupMk0.

theorem TauCeti.Multiquadratic.card_sub_one_le_twoRank {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (Q : ℕ → ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd : d < -1) {s : Finset ℕ} (hram : ∀ p ∈ s, p ∈ NumberField.ramifiedPrimes K) (hprime : ∀ p ∈ s, (↑(Q p)).IsPrime) (hover : ∀ p ∈ s, (↑(Q p)).LiesOver (Ideal.span {↑p})) (hs : d.natAbs.primeFactors ⊆ s) : s.card - 1 ≤ ClassGroup.twoRank (NumberField.RingOfIntegers K)

The genus-theoretic lower bound on the 2-rank. For K = ℚ(√d) with d < -1 squarefree and s a finite set of ramified rational primes containing every prime factor of d, the 2-rank of Cl(𝓞 K) is at least #s - 1: the classes of the ramified primes span a subgroup of exponent two and order 2 ^ (#s - 1).

theorem TauCeti.Multiquadratic.ncard_ramifiedPrimes_sub_one_le_twoRank {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd : d < -1) : (NumberField.ramifiedPrimes K).ncard - 1 ≤ ClassGroup.twoRank (NumberField.RingOfIntegers K)

The genus-theoretic lower bound 2-rank ≥ t - 1. For an imaginary quadratic field K = ℚ(√d) with d < -1 squarefree, the 2-rank of the class group is at least t - 1, where t = #{ramified primes}. Together with the matching upper bound this is the 2-rank formula of genus theory in the imaginary case; the field-theoretic counterpart, [K_gen : K] = 2 ^ (t - 1), is finrank_candidateGenusField_over_candidateGenusFieldBase_eq_two_pow_ncard_ramifiedPrimes.