The structure of an ambiguous ideal of a quadratic field

Let K be a quadratic number field with quadratic conjugation σ. An ideal I of 𝓞 K is ambiguous when σI = I. This file describes the nonzero ambiguous ideals completely: they are exactly the products

I = n 𝓞 K · ∏_{p ∈ s} 𝔭_p

of a positive rational integer with a product of distinct primes above ramified rational primes. The zero ideal is ambiguous as well, but it is not of this form, every such product being nonzero.

The proof is an induction on the absolute norm, peeling off at each step a conjugation-stable divisor of one of two shapes. Let 𝔭 be a maximal ideal containing I and p the rational prime below it.

• σ𝔭 = 𝔭 and p ramifies. Then 𝔭 is the only prime of 𝓞 K above p (NumberField.primesOver_eq_singleton_of_mem_ramifiedPrimes), so it is the chosen prime Q p.
• σ𝔭 = 𝔭 and p does not ramify. Then p is inert and 𝔭 = p 𝓞 K (NumberField.map_span_eq_of_notMem_ramifiedPrimes).
• σ𝔭 ≠ 𝔭. Then 𝔭 and σ𝔭 are distinct maximal ideals, hence coprime, and both divide I because I is ambiguous; so their product divides I, and that product is N(𝔭) 𝓞 K (NumberField.mul_map_ringOfIntegersQuadraticConj_eq_map_relNorm together with Ideal.relNorm_int).

Repeated ramified primes are absorbed into the rational factor through 𝔭_p ^ 2 = p 𝓞 K (NumberField.map_span_eq_sq_of_mem_ramifiedPrimes), which is what makes the exponents in the product squarefree.

Everything here is signature-free: the rational factor is generated by a positive natural number, hence by a totally positive element (exists_isTotallyPositive_and_eq_span_singleton_mul_prod_of_map_eq_self). So the description feeds the narrow class group Cl⁺(K) exactly as it feeds the ordinary one: the narrow class of an ambiguous ideal is a product of narrow classes of ramified primes (NumberField.NarrowClassGroup.mk0_mem_closure_of_map_eq_self), which is what gives the genus-theoretic upper bound 2-rank ≤ t - 1 of TauCeti.Multiquadratic.twoRank_le_ncard_ramifiedPrimes_sub_one, for a quadratic field of either signature. The ordinary form is NumberField.classGroupMk0_mem_closure_of_map_eq_self.

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 this description opens.

Main results

• NumberField.exists_eq_span_singleton_mul_prod_of_map_eq_self: a nonzero ambiguous ideal is a positive rational integer times a product of distinct primes above ramified rational primes.
• NumberField.map_eq_self_of_eq_span_singleton_mul_prod: the converse, that every such product is ambiguous.
• NumberField.map_eq_self_iff_exists_eq_span_singleton_mul_prod: the resulting characterisation of the nonzero ambiguous ideals.
• NumberField.exists_isTotallyPositive_and_eq_span_singleton_mul_prod_of_map_eq_self: the form the narrow class group consumes for a nonzero ambiguous ideal, with the rational factor replaced by a totally positive generator.

theorem NumberField.map_eq_self_of_eq_span_singleton_mul_prod {K : Type u_1} [Field K] [NumberField K] {Q : ℕ → Ideal (RingOfIntegers K)} (hprime : ∀ p ∈ ramifiedPrimes K, (Q p).IsPrime) (hover : ∀ p ∈ ramifiedPrimes K, (Q p).LiesOver (Ideal.span {↑p})) (hK : Module.finrank ℚ K = 2) (σ : RingOfIntegers K ≃+* RingOfIntegers K) (m : ℕ) {s : Finset ℕ} (hs : ↑s ⊆ ramifiedPrimes K) : Ideal.map σ (Ideal.span {↑m} * ∏ p ∈ s, Q p) = Ideal.span {↑m} * ∏ p ∈ s, Q p

Every rational multiple of a product of ramified primes is fixed by any automorphism. The converse half of map_eq_self_iff_exists_eq_span_singleton_mul_prod: a ring automorphism fixes the ideal generated by a rational integer, and fixes each prime above a ramified rational prime, since there is only one such prime.

theorem NumberField.exists_eq_span_singleton_mul_prod_of_map_eq_self {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} {Q : ℕ → 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 : Ideal (RingOfIntegers K)} (hI0 : I ≠ 0) (hI : Ideal.map (ringOfIntegersQuadraticConj hmin hgen) I = I) : ∃ (m : ℕ), 0 < m ∧ ∃ (s : Finset ℕ), ↑s ⊆ ramifiedPrimes K ∧ I = Ideal.span {↑m} * ∏ p ∈ s, Q p

The structure of an ambiguous ideal. 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. A nonzero ideal I with σI = I is a positive rational integer times a product of distinct primes above ramified rational primes: I = m 𝓞 K · ∏_{p ∈ s} Q p.

The exponents are squarefree because Q p ^ 2 = p 𝓞 K absorbs a repeated ramified prime into the rational factor.

theorem NumberField.map_eq_self_iff_exists_eq_span_singleton_mul_prod {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} {Q : ℕ → 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 : Ideal (RingOfIntegers K)} (hI0 : I ≠ 0) : Ideal.map (ringOfIntegersQuadraticConj hmin hgen) I = I ↔ ∃ (m : ℕ), 0 < m ∧ ∃ (s : Finset ℕ), ↑s ⊆ ramifiedPrimes K ∧ I = Ideal.span {↑m} * ∏ p ∈ s, Q p

The ambiguous ideals of a quadratic field. A nonzero ideal of 𝓞 K is fixed by quadratic conjugation exactly when it is a positive rational integer times a product of distinct primes above ramified rational primes.

theorem NumberField.exists_isTotallyPositive_and_eq_span_singleton_mul_prod_of_map_eq_self {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} {Q : ℕ → 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 : Ideal (RingOfIntegers K)} (hI0 : I ≠ 0) (hI : Ideal.map (ringOfIntegersQuadraticConj hmin hgen) I = I) : ∃ (α : RingOfIntegers K), α ≠ 0 ∧ IsTotallyPositive ↑α ∧ ∃ (s : Finset ℕ), ↑s ⊆ ramifiedPrimes K ∧ I = Ideal.span {α} * ∏ p ∈ s, Q p

An ambiguous ideal is a totally positive principal ideal times ramified primes. The signature-free form of exists_eq_span_singleton_mul_prod_of_map_eq_self: the rational factor is generated by a positive natural number, hence by a totally positive element. This is what the narrow class group Cl⁺(K) consumes, where the ordinary class group only needs the generator to exist.