Classes of ambiguous ideals are generated by ramified primes

Let K be a quadratic number field with quadratic conjugation σ. An ideal I of 𝓞 K is ambiguous when σI = I. This file draws the class-group consequence of the structure theorem for ambiguous ideals: the class of an ambiguous ideal lies in the subgroup of Cl(𝓞 K) generated by the classes of the primes above the ramified rational primes.

The work is done by NumberField.exists_eq_span_singleton_mul_prod_of_map_eq_self, which writes an ambiguous ideal as m 𝓞 K · ∏_{p ∈ s} Q p with m a positive rational integer and s a finite set of ramified rational primes. The rational factor is principal, so it contributes the trivial class, and each remaining factor is one of the named generators.

Combined with the Hilbert-90 descent of Quadratic/Conjugation/Ambiguous/Basic.lean, which for a totally complex K represents every 2-torsion class by an ambiguous ideal, this says that Cl(𝓞 K)[2] is generated by the classes of the ramified primes. The relation ∏ 𝔭 = (θ) of TauCeti.Multiquadratic.span_singleton_eq_prod_primeFactors then removes one generator, bounding the 2-rank by t - 1 for an imaginary quadratic field.

The genus-theoretic bound itself (TauCeti.Multiquadratic.twoRank_le_ncard_ramifiedPrimes_sub_one) is proved for a quadratic field of either signature, so it runs through the narrow counterparts of these two statements — NumberField.NarrowClassGroup.mk0_mem_closure_of_map_eq_self and NumberField.NarrowClassGroup.mem_closure_of_sq_eq_one — which need no hypothesis on the signature. What is recorded here is the ordinary form of the generation statement.

See F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2, and D. A. Cox, Primes of the Form x² + ny², §6.A, for the classical ambiguous class number formula.

Main results

• NumberField.classGroupMk0_mem_closure_of_map_eq_self: the class of an ambiguous ideal is a product of classes of primes above ramified rational primes.
• NumberField.mem_closure_of_sq_eq_one: for a totally complex quadratic field, every 2-torsion ideal class is such a product.

theorem NumberField.classGroupMk0_mem_closure_of_map_eq_self {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} {Q : ℕ → ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hprime : ∀ p ∈ ramifiedPrimes K, (↑(Q p)).IsPrime) (hover : ∀ p ∈ ramifiedPrimes K, (↑(Q p)).LiesOver (Ideal.span {↑p})) {I : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))} (hI : Ideal.map (ringOfIntegersQuadraticConj hmin hgen) ↑I = ↑I) : ClassGroup.mk0 I ∈ Subgroup.closure ((fun (p : ℕ) => ClassGroup.mk0 (Q p)) '' ramifiedPrimes K)

The class of an ambiguous ideal is a product of classes of ramified primes. Let K be a quadratic number field with quadratic conjugation σ, and let Q p be a prime of 𝓞 K above each ramified rational prime p. If σI = I then the class of I lies in the subgroup of Cl(𝓞 K) generated by the classes [Q p] for ramified p.

This is the class-group shadow of exists_eq_span_singleton_mul_prod_of_map_eq_self: the rational factor of an ambiguous ideal is principal, so only the ramified primes survive.

theorem NumberField.mem_closure_of_sq_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} {Q : ℕ → ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))} [IsTotallyComplex K] (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hprime : ∀ p ∈ ramifiedPrimes K, (↑(Q p)).IsPrime) (hover : ∀ p ∈ ramifiedPrimes K, (↑(Q p)).LiesOver (Ideal.span {↑p})) {Cl : ClassGroup (RingOfIntegers K)} (hCl : Cl ^ 2 = 1) : Cl ∈ Subgroup.closure ((fun (p : ℕ) => ClassGroup.mk0 (Q p)) '' ramifiedPrimes K)

The 2-torsion of the class group of an imaginary quadratic field is generated by the ramified primes. A 2-torsion class of a totally complex quadratic field is the class of an ambiguous ideal (exists_map_ringOfIntegersQuadraticConj_eq_self_of_sq_eq_one, the Hilbert-90 descent step), and the class of an ambiguous ideal is a product of classes of ramified primes.

This generation result yields the genus-theoretic upper bound; it does not state the exact ambiguous class number formula, whose real quadratic form also includes a unit index. Total complexity is needed for the descent step, not for the generation lemma.