Documentation

TauCeti.NumberTheory.NumberField.Quadratic.Conjugation.Ambiguous.Narrow

Ambiguous ideals and the narrow class group of a quadratic field #

Let K be a quadratic number field with quadratic conjugation σ. An ideal of 𝓞 K is ambiguous when σI = I. This file proves the descent step of the narrow ambiguous class number formula: a 2-torsion class of the narrow class group Cl⁺(K) is the narrow class of an ambiguous ideal,

C ^ 2 = 1 → ∃ I, σI = I ∧ [I]⁺ = C,

and draws its consequence for the ramified primes: since an ambiguous ideal is a totally positive principal ideal times a product of distinct primes above ramified rational primes, the 2-torsion of Cl⁺(K) is generated by the narrow classes of the ramified primes. Both statements hold with no hypothesis on the signature of K. The ordinary statement (NumberField.exists_map_ringOfIntegersQuadraticConj_eq_self_of_sq_eq_one) needs K totally complex, and genuinely fails for real quadratic fields; the t - 1 genus-theory formula for a real quadratic field is a statement about Cl⁺(K), and this is the descent it rests on (Layer 3 of the multiquadratic roadmap). The generation statement is the narrow form of NumberField.mem_closure_of_sq_eq_one.

Two archimedean inputs replace total complexity, and both come from total positivity.

The last step is where the narrow group earns its keep. In the ordinary class group (ε) J and J have the same class automatically; narrowly one must know that (ε) has a totally positive generator. It does: ε / σε = y / x is totally positive, so ε and σε agree in sign at each real place, and since the real embeddings of a quadratic field are φ and φ ∘ σ (NumberField.realRingHom_eq_or_eq_comp_quadraticConj), either ε or is totally positive. Classically this is the statement that the totally positive units of the base field are trivial, so the ambiguous narrow classes are all strongly ambiguous.

See D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws, Chapter 6, for the ambiguous class number formula and its narrow form.

Main results #

Quadratic conjugation inverts narrow ideal classes. The product I · σI is the extension of the norm ideal relNorm ℤ I, which is generated by a positive rational integer; that generator is totally positive, so I · σI has trivial narrow class.

Every 2-torsion narrow class of a quadratic field is the narrow class of an ambiguous ideal. This is the Hilbert-90 descent step of the narrow ambiguous class number formula, and unlike its ordinary counterpart it needs no hypothesis on the signature of K: the positivity that total complexity supplied in the ordinary case is supplied here by total positivity.

The class of an ambiguous ideal is 2-torsion in the narrow class group. Conjugation acts on Cl⁺(K) by inversion, so the class of an ideal it fixes is its own inverse.

The ambiguous narrow classes are exactly the narrow classes of ambiguous ideals. This is the descent step of the narrow ambiguous class number formula, valid for real and imaginary quadratic fields alike.

theorem NumberField.NarrowClassGroup.mk0_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 : pramifiedPrimes K, (↑(Q p)).IsPrime) (hover : pramifiedPrimes K, (↑(Q p)).LiesOver (Ideal.span {p})) {I : (nonZeroDivisors (Ideal (RingOfIntegers K)))} (hI : Ideal.map (ringOfIntegersQuadraticConj hmin hgen) I = I) :
mk0 I Subgroup.closure ((fun (p : ) => mk0 (Q p)) '' ramifiedPrimes K)

The narrow class of an ambiguous ideal is a product of narrow 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 narrow class of I lies in the subgroup of Cl⁺(K) generated by the narrow classes [Q p]⁺ for ramified p.

The ordinary counterpart NumberField.classGroupMk0_mem_closure_of_map_eq_self discards the rational factor of an ambiguous ideal because it is principal; here it is discarded because it has a totally positive generator (exists_isTotallyPositive_and_eq_span_singleton_mul_prod_of_map_eq_self), which is what the narrow class group asks for.

theorem NumberField.NarrowClassGroup.mem_closure_of_sq_eq_one {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 : pramifiedPrimes K, (↑(Q p)).IsPrime) (hover : pramifiedPrimes K, (↑(Q p)).LiesOver (Ideal.span {p})) {C : NarrowClassGroup K} (hC : C ^ 2 = 1) :
C Subgroup.closure ((fun (p : ) => mk0 (Q p)) '' ramifiedPrimes K)

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

Unlike its ordinary counterpart NumberField.mem_closure_of_sq_eq_one, this needs no hypothesis on the signature of K: it holds for real and imaginary quadratic fields alike. It gives the generation half of the genus-theoretic upper bound, not the exact narrow ambiguous class number.