The 2-rank of a quadratic class group

For a squarefree integer d let K = ℚ(√d) and let t be the number of rational primes that ramify in K. Genus theory computes the 2-rank of the narrow class group Cl⁺(K), the dimension over 𝔽₂ of Cl⁺(K)/Cl⁺(K)², to be exactly t - 1. This file proves that formula,

2-rank Cl⁺(K) = t - 1,

for a quadratic field of either signature: the upper bound is the ambiguous class number bound, and the lower bound is the independence of the genus characters. The ordinary bound 2-rank Cl(K) ≤ t - 1 follows because forgetting positivity is surjective (NumberField.NarrowClassGroup.classGroupTwoRank_le_twoRank). It is the class-group counterpart of the field-theoretic 2 ^ (t - 1) available for the candidate genus field, whose degree over the embedded copy of K is 2 ^ (t - 1) (finrank_candidateGenusField_over_candidateGenusFieldBase_eq_two_pow_ncard_ramifiedPrimes).

Two inputs combine. The 2-torsion of Cl⁺(K) is generated by the narrow classes of the ramified primes (NumberField.NarrowClassGroup.mem_closure_of_sq_eq_one, which rests on the Hilbert-90 descent to ambiguous ideals — narrowly, with no hypothesis on the signature), and the subgroup those classes generate has at most 2 ^ (t - 1) elements (natCard_closure_image_narrowMk0_le, where the - 1 comes from the narrow relation exists_nonempty_prod_narrowMk0_eq_one). Since the maximal elementary-2 quotient and the 2-torsion subgroup have the same cardinality, 2 ^ (2-rank) ≤ 2 ^ (t - 1).

The lower bound t - 1 ≤ 2-rank Cl⁺(K) comes from the genus characters. The t prime discriminants dividing the discriminant of K give t characters of Cl⁺(K) with values ±1 (genusCharFunNarrowClassGroupHom), hence a ZMod 2-linear map Cl⁺(K)/Cl⁺(K)² → (ZMod 2)^t. Every sign pattern of product 1 is attained, by the class of a degree-one prime ideal supplied by Dirichlet's theorem (exists_forall_genusCharFunNarrowClassGroupHom_singleton_eq), so the image contains a hyperplane and the 2-rank is at least t - 1.

For an imaginary quadratic field the narrow and ordinary class groups coincide, and the ordinary lower bound also follows from the independence of the ramified-prime classes (TauCeti.Multiquadratic.ncard_ramifiedPrimes_sub_one_le_twoRank); combining it with the upper bound gives the imaginary quadratic 2-rank formula for Cl(K). For a real quadratic field the ordinary 2-rank can be strictly smaller than t - 1 — ℚ(√3) has t = 2 and class number 1 — so there the formula is genuinely a statement about Cl⁺(K).

See F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2, which runs the same route: its Proposition 2.9 is the Hilbert-90 descent realising an ambiguous class by an ambiguous ideal, and its "first inequality" #Cl⁺/Cl⁺² ≤ 2^(t-1) is the bound proved here. D. A. Cox, Primes of the Form x² + ny², §6.A has the same statement for field discriminants, and §3.B the form-theoretic genus theory it descends from.

Main results

• TauCeti.Multiquadratic.narrowTwoRank_le_ncard_ramifiedPrimes_sub_one: the upper bound on the narrow 2-rank of a quadratic field.
• TauCeti.Multiquadratic.twoRank_le_ncard_ramifiedPrimes_sub_one: the same bound for the ordinary 2-rank.
• TauCeti.Multiquadratic.twoRank_eq_ncard_ramifiedPrimes_sub_one: the 2-rank of an imaginary quadratic class group is exactly t - 1.
• TauCeti.Multiquadratic.ncard_ramifiedPrimes_sub_one_le_narrowTwoRank: the lower bound on the narrow 2-rank of a quadratic field of either signature.
• TauCeti.Multiquadratic.narrowTwoRank_eq_ncard_ramifiedPrimes_sub_one: the narrow 2-rank of a quadratic field of either signature is exactly t - 1.
• TauCeti.Multiquadratic.twoRank_eq_ncard_ramifiedPrimes_sub_one_of_exists_norm_eq_neg_one: the ordinary 2-rank is also exactly t - 1 when some unit of 𝓞 K has norm -1.
• TauCeti.Multiquadratic.ncard_ramifiedPrimes_sub_two_le_twoRank and TauCeti.Multiquadratic.twoRank_eq_ncard_ramifiedPrimes_sub_one_or_sub_two: the ordinary 2-rank of any field of degree 2 over ℚ is t - 1 or t - 2.

theorem TauCeti.Multiquadratic.narrowTwoRank_le_ncard_ramifiedPrimes_sub_one {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 : 1 < d.natAbs) : NumberField.NarrowClassGroup.twoRank K ≤ (NumberField.ramifiedPrimes K).ncard - 1

The narrow ambiguous class number bound. For K = ℚ(√d) with d squarefree and 1 < |d|, the 2-rank of the narrow class group Cl⁺(K) is at most t - 1, where t is the number of rational primes ramifying in K. No hypothesis on the signature of K is needed.

The 2-torsion of Cl⁺(K) is generated by the narrow classes of the ramified primes, and those classes satisfy a relation, so they span at most 2 ^ (t - 1) classes. The hypothesis 1 < |d| excludes d = -1, where the radicand has no prime factor; see exists_nonempty_prod_narrowMk0_eq_one.

theorem TauCeti.Multiquadratic.twoRank_le_ncard_ramifiedPrimes_sub_one {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 : 1 < d.natAbs) : ClassGroup.twoRank (NumberField.RingOfIntegers K) ≤ (NumberField.ramifiedPrimes K).ncard - 1

The ambiguous class number bound. For K = ℚ(√d) with d squarefree and 1 < |d|, the 2-rank of Cl(𝓞 K) is at most t - 1, where t is the number of rational primes ramifying in K.

Forgetting total positivity is a surjection Cl⁺(K) → Cl(K), so the ordinary 2-rank is at most the narrow one, which narrowTwoRank_le_ncard_ramifiedPrimes_sub_one bounds by t - 1. For a real quadratic field the inequality can be strict: ℚ(√3) has t = 2 and class number 1.

theorem TauCeti.Multiquadratic.twoRank_eq_ncard_ramifiedPrimes_sub_one {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 < 0) : ClassGroup.twoRank (NumberField.RingOfIntegers K) = (NumberField.ramifiedPrimes K).ncard - 1

The 2-rank formula for an imaginary quadratic field. For K = ℚ(√d) with d < 0 squarefree, the 2-rank of Cl(𝓞 K) is exactly t - 1, where t is the number of rational primes ramifying in K.

The narrow lower bound

theorem TauCeti.Multiquadratic.card_sub_one_le_narrowTwoRank {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) : s.card - 1 ≤ NumberField.NarrowClassGroup.twoRank K

The genus characters bound the narrow 2-rank from below. Let K = ℚ(√d) with d squarefree and let ∏ P ∈ s, P = fundamentalDiscriminant d be the prime-discriminant factorization, t = #s. Then t - 1 ≤ 2-rank Cl⁺(K).

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

The genus-theoretic lower bound on the narrow 2-rank. For K = ℚ(√d) with d squarefree, the 2-rank of the narrow class group Cl⁺(K) is at least t - 1, where t is the number of rational primes ramifying in K. No hypothesis on the signature of K is needed.

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

The 2-rank formula for the narrow class group of a quadratic field. For K = ℚ(√d) with d squarefree, of either signature, the 2-rank of Cl⁺(K) is exactly t - 1, where t is the number of rational primes ramifying in K. For an imaginary K the narrow and ordinary class groups coincide, and this recovers twoRank_eq_ncard_ramifiedPrimes_sub_one; that identity is also how the Gaussian field d = -1, which the ambiguous class number bound excludes, is covered.

theorem TauCeti.Multiquadratic.twoRank_eq_ncard_ramifiedPrimes_sub_one_of_exists_norm_eq_neg_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hu : ∃ (u : (NumberField.RingOfIntegers K)ˣ), (Algebra.norm ℚ) ↑↑u = -1) : ClassGroup.twoRank (NumberField.RingOfIntegers K) = (NumberField.ramifiedPrimes K).ncard - 1

The 2-rank formula for a real quadratic field with a unit of norm -1. For K = ℚ(√d) with d squarefree, if some unit of 𝓞 K has norm -1 then the narrow and ordinary class groups coincide (NumberField.NarrowClassGroup.toClassGroup_injective_of_norm_eq_neg_one), so the ordinary 2-rank inherits the narrow value t - 1, with t the number of rational primes ramifying in K. A unit of norm -1 suffices to keep the real case from dropping; without one the ordinary rank can be smaller, as for ℚ(√3), which has t = 2 and class number 1.

The ordinary 2-rank of a quadratic field

theorem TauCeti.Multiquadratic.ncard_ramifiedPrimes_sub_two_le_twoRank {K : Type u_1} [Field K] [NumberField K] (hK : Module.finrank ℚ K = 2) : (NumberField.ramifiedPrimes K).ncard - 2 ≤ ClassGroup.twoRank (NumberField.RingOfIntegers K)

The ordinary 2-rank of a quadratic field falls at most one short of t - 1. For any field K of degree 2 over ℚ, t - 2 ≤ 2-rank Cl(𝓞 K), where t is the number of rational primes ramifying in K.

Writing K = ℚ(√d) with d squarefree (NumberField.exists_minpoly_eq_X_sq_sub_C_and_adjoin_eq_top), the narrow 2-rank is exactly t - 1 (narrowTwoRank_eq_ncard_ramifiedPrimes_sub_one) and forgetting positivity is a surjection Cl⁺(K) → Cl(K) whose kernel has at most two elements (NumberField.card_ker_toClassGroup_le_two), so the ordinary 2-rank drops by at most one (MonoidHom.twoRank_le_twoRank_add_of_card_ker_le_two_pow). For an imaginary field the kernel is trivial and no drop occurs; for a real field it can, as ℚ(√3) shows.

theorem TauCeti.Multiquadratic.twoRank_eq_ncard_ramifiedPrimes_sub_one_or_sub_two {K : Type u_1} [Field K] [NumberField K] (hK : Module.finrank ℚ K = 2) : ClassGroup.twoRank (NumberField.RingOfIntegers K) = (NumberField.ramifiedPrimes K).ncard - 1 ∨ ClassGroup.twoRank (NumberField.RingOfIntegers K) = (NumberField.ramifiedPrimes K).ncard - 2

The ordinary 2-rank of a quadratic field is t - 1 or t - 2. For any field K of degree 2 over ℚ, the 2-rank of Cl(𝓞 K) is one of the two values allowed by the narrow formula 2-rank Cl⁺(K) = t - 1, with t the number of ramified rational primes. Both values occur among real quadratic fields: ℚ(√3) has t = 2 and class number 1, so its 2-rank is 0 = t - 2, while ℚ(√10) has t = 2 and class number 2, so its 2-rank is 1 = t - 1. For an imaginary field the value is always t - 1 (twoRank_eq_ncard_ramifiedPrimes_sub_one).