Ambiguous ideals of a quadratic field #
An ideal of 𝓞 K is ambiguous when quadratic conjugation σ fixes it, σI = I; an ideal class
is ambiguous when σ fixes it, which for a quadratic field means exactly that the class is
2-torsion (NumberField.mulEquiv_ringOfIntegersQuadraticConj_apply_eq_self_iff, since σ acts by
inversion). Every ambiguous ideal obviously has an ambiguous class. This file proves the converse
for an imaginary quadratic field: every ambiguous class is the class of an ambiguous ideal, so
the two notions of "ambiguous" match up:
C ^ 2 = 1 ↔ ∃ I, σI = I ∧ [I] = C.
This is the descent step of the classical ambiguous class number formula, which counts the
2-torsion of Cl(𝓞 K): it replaces a count of ambiguous classes by a count of ambiguous
ideals. The remaining step of that count — that the class of an ambiguous ideal is a product of
classes of ramified primes, which in turn satisfy the relation ∏ 𝔭 = (θ) of
TauCeti.Multiquadratic.span_singleton_eq_prod_primeFactors — is
NumberField.classGroupMk0_mem_closure_of_map_eq_self in
Quadratic/Conjugation/Ambiguous/Ideal.lean; the two together give the genus-theoretic bound
2-rank ≤ t - 1 of the Multiquadratic roadmap.
The proof is Hilbert's Theorem 90 for the quadratic extension K/ℚ, in the elementary form
available for a degree-two extension. If [σJ] = [J] then (x) σJ = (y) J for nonzero
x y : 𝓞 K; conjugating and cancelling gives (x σx) = (y σy), so x σx and y σy are
associates. The unit relating them has norm the square of the rational N(y) / N(x), and in a
totally complex field total positivity is vacuous, so the norm of a nonzero element is strictly
positive (NumberField.norm_pos_of_isTotallyPositive), which forces x σx = y σy on the nose.
Hilbert 90 then produces ε ≠ 0 with x ε = y σε, and I = (ε) J is an ambiguous ideal in J's
class. For a real quadratic field the positivity fails — that is exactly where the classical
unit index [E : E ∩ N K^×] enters the ambiguous class number formula — so the hypothesis
IsTotallyComplex K is essential rather than technical. The repair is to pass to the narrow
class group, where total positivity restores the sign for every quadratic field; see
Quadratic/Conjugation/Ambiguous/Narrow.lean.
The integral Hilbert 90 result used below is proved in Quadratic.Conjugation.Hilbert90.
For a quadratic field of either signature, this file also defines a strongly ambiguous class to be an ordinary ideal class represented by an ambiguous ideal. The definition and its basic API do not require the totally complex hypothesis; only the converse from an ambiguous class to an ambiguous ideal does.
See F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2, whose Proposition 2.9 is the statement proved here, and D. A. Cox, Primes of the Form x² + ny², §6.A, for the classical ambiguous class number formula.
Main results #
NumberField.mul_ringOfIntegersQuadraticConj_eq_mul_ringOfIntegersQuadraticConj_of_associated: associated norms with a positive norm product are equal, the archimedean input to the descent.NumberField.exists_map_ringOfIntegersQuadraticConj_eq_self_of_sq_eq_one: a2-torsion ideal class of an imaginary quadratic field is the class of an ambiguous ideal.NumberField.classGroupMk0_sq_eq_one_of_map_ringOfIntegersQuadraticConj_eq_self: conversely, the class of an ambiguous ideal is2-torsion.NumberField.IsStronglyAmbiguousClass: an ordinary ideal class is strongly ambiguous when it is represented by an ideal fixed by quadratic conjugation.NumberField.stronglyAmbiguousClassSubgroup: the subgroup of strongly ambiguous ordinary ideal classes.NumberField.sq_eq_one_iff_exists_map_ringOfIntegersQuadraticConj_eq_self: the ambiguous classes are exactly the classes of ambiguous ideals.Ideal.map_map_of_involutive: pushing an ideal forward twice along an involutive ring automorphism returns it.
Pushing an ideal forward twice along an involutive ring automorphism returns it.
Two elements with associated norms and positive norm product have equal norms. If
x σx and y σy are associates in 𝓞 K and the norm of x y is positive, then x σx = y σy:
their ratio is a unit whose norm is the square of the rational N(y) / N(x), so N(x) = ± N(y),
and the sign is fixed by 0 < N(x) N(y).
This is where the archimedean input enters the ambiguous class number formula. For a totally complex
field the norm of a nonzero element is automatically positive; for a real quadratic field the
positivity has to come from total positivity of x y, which is what the narrow class group
supplies.
Every ambiguous ideal class of an imaginary quadratic field is the class of an ambiguous
ideal. Let K be a totally complex quadratic number field with quadratic conjugation σ. A
2-torsion ideal class — equivalently, by
mulEquiv_ringOfIntegersQuadraticConj_apply_eq_self_iff, a class fixed by σ — is the class of an
ideal I with σI = I. This is the Hilbert-90 descent step of the ambiguous class number
formula.
The class of an ambiguous ideal is 2-torsion. An ideal fixed by quadratic conjugation has
a class fixed by the induced action on Cl(𝓞 K), which is 2-torsion because that action is
inversion (mulEquiv_ringOfIntegersQuadraticConj_apply_eq_self_iff). This is the easy direction of
sq_eq_one_iff_exists_map_ringOfIntegersQuadraticConj_eq_self, and needs no hypothesis on the
signature of K.
An ordinary ideal class is strongly ambiguous if it is represented by an ideal fixed by quadratic conjugation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A class is strongly ambiguous exactly when it has a representative fixed by quadratic conjugation.
A conjugation-fixed ideal represents a strongly ambiguous class.
A strongly ambiguous class has a representative fixed by quadratic conjugation.
Every strongly ambiguous class is fixed by quadratic conjugation.
The subgroup of the ordinary class group consisting of strongly ambiguous classes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in the strongly ambiguous class subgroup means having a representative fixed by quadratic conjugation.
The ambiguous classes of an imaginary quadratic field are exactly the classes of ambiguous
ideals. For a totally complex quadratic number field, an ideal class is 2-torsion — equivalently
fixed by quadratic conjugation — precisely when it is represented by an ideal that conjugation
fixes. This is the descent step of the ambiguous class number formula: it turns the count of
2-torsion classes into a count of ambiguous ideals. Classifying those ideals — their classes are
products of classes of ramified primes — is classGroupMk0_mem_closure_of_map_eq_self.