The class of a ramified prime is 2-torsion

For a degree-two number field K, the unique prime 𝔭 of 𝓞 K above a ramified rational prime p satisfies 𝔭² = p 𝓞 K, the extension of the principal ideal (p), so its class [𝔭] in Cl(𝓞 K) squares to 1: it is an explicit element of the 2-torsion Cl(𝓞 K)[2], the object measured by card_elementaryTwoQuotient_eq_card_twoTorsion. The generator p of that principal ideal is a positive rational integer, hence totally positive, so the same computation bounds the order of [𝔭]⁺ in the narrow class group Cl⁺(K).

Any ring automorphism of 𝓞 K fixes 𝔭 (map_eq_self_of_mem_ramifiedPrimes); applied to quadratic conjugation this says 𝔭 is an ambiguous ideal, so the ramified primes furnish individual explicit ambiguous 2-torsion classes. Determining all of Cl(𝓞 K)[2] (the ambiguous-class-number / 2-rank theorem of genus theory, which for real fields carries a unit-index correction relating these strongly ambiguous classes to the ambiguous ones) is left to later work.

A ramified prime also exhausts the class group when the Minkowski bound is small enough: if that bound is below 3 and 2 is ramified, then every ideal class is trivial or the class of the prime above 2, so Cl(𝓞 K) has at most two elements.

See D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws, for the classical genus theory this result underlies.

Main results

• NumberField.classGroupMk0_sq_eq_one_of_mem_ramifiedPrimes: the class of a ramified prime is 2-torsion.
• NumberField.NarrowClassGroup.mk0_sq_eq_one_of_mem_ramifiedPrimes: so is its narrow class.
• TauCeti.NumberField.class_eq_one_or_eq_classGroupMk0_primeAboveTwo_of_minkowskiBound_lt_three: with Minkowski bound below 3 and 2 ramified, every ideal class is trivial or the class of a prime above 2.

theorem NumberField.classGroupMk0_sq_eq_one_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] (hK : Module.finrank ℚ K = 2) {p : ℕ} (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : ClassGroup.mk0 ⟨𝔭, ⋯⟩ ^ 2 = 1

The class of a ramified prime is 2-torsion. In a degree-two number field, the prime 𝔭 above a ramified rational prime p satisfies 𝔭² = p 𝓞 K, the extension of the principal ideal (p), so its class in Cl(𝓞 K) squares to 1: [𝔭] is an explicit element of the 2-torsion Cl(𝓞 K)[2].

theorem NumberField.NarrowClassGroup.mk0_sq_eq_one_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] (hK : Module.finrank ℚ K = 2) {p : ℕ} (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : mk0 ⟨𝔭, ⋯⟩ ^ 2 = 1

The narrow class of a ramified prime is 2-torsion. In a degree-two number field, the prime 𝔭 above a ramified rational prime p satisfies 𝔭² = p 𝓞 K, and the rational integer p is positive, hence totally positive; so the narrow class of 𝔭 squares to 1 in Cl⁺(K).

theorem TauCeti.NumberField.class_eq_one_or_eq_classGroupMk0_primeAboveTwo_of_minkowskiBound_lt_three {K : Type u_1} [Field K] [NumberField K] (hfin : Module.finrank ℚ K = 2) (hram : 2 ∈ NumberField.ramifiedPrimes K) (hM : (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|) < 3) (P : Ideal (NumberField.RingOfIntegers K)) [P.IsPrime] [P.LiesOver (Ideal.span {2})] (C : ClassGroup (NumberField.RingOfIntegers K)) : C = 1 ∨ C = ClassGroup.mk0 ⟨P, ⋯⟩

With Minkowski bound below 3 and 2 ramified in a quadratic field, every ideal class is trivial or the class of a prime P above 2.