Documentation

TauCeti.NumberTheory.NumberField.Quadratic.Conjugation.ClassGroup

Quadratic conjugation acts on the class group by inversion #

For a quadratic number field K = ℚ(√d), NumberField.ringOfIntegersQuadraticConj is the ring automorphism σ : 𝓞 K ≃+* 𝓞 K restricting field conjugation. This file records that its induced action on the class group Cl(𝓞 K) is an involution, sharpens that to inversion (the genus-theoretic mechanism I · σI principal), and concludes that σ therefore acts trivially on the maximal elementary-2 quotient Cl(𝓞 K)/Cl(𝓞 K)².

The reduction has two moves. First the general bridge ClassGroup.mulEquiv_mk0 (in ClassGroup/Equiv.lean): for a ring isomorphism f : R ≃+* R' of Dedekind domains, ClassGroup.mulEquiv f sends the class of an ideal to the class of its pushforward Ideal.map f. Second the inversion: the ideal class of σI is the inverse of the class of I because I · σI is principal — the norm-principality theorem isPrincipal_mul_map_ringOfIntegersQuadraticConj (in Quadratic/Conjugation/Norm/Basic.lean) combined with ClassGroup.mk0_eq_mk0_inv_iff. Since each C⁻¹ and C differ by a square, inversion is trivial on the elementary-2 quotient, giving the identity on Cl/Cl².

This is Layer 3 of the multiquadratic roadmap: the summit isomorphism Gal(K_gen/K) ≅ Cl(K)/Cl(K)² factors the conjugation action through its triviality on Cl/Cl².

See D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws, for the classical genus theory behind the inversion action of conjugation on the class group.

Main results #

source
@[simp]
theorem NumberField.mulEquiv_ringOfIntegersQuadraticConj_involutive {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) :
Function.Involutive ⇑(ClassGroup.mulEquiv (ringOfIntegersQuadraticConj hmin hgen))

Quadratic conjugation acts as an involution on the class group Cl(𝓞 K). This is the group-action shadow of ringOfIntegersQuadraticConj_involutive, sharpened to inversion by mulEquiv_ringOfIntegersQuadraticConj_apply_eq_inv below.

source
@[simp]
theorem NumberField.mulEquiv_ringOfIntegersQuadraticConj_apply_eq_inv {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (C : ClassGroup (RingOfIntegers K)) :
(ClassGroup.mulEquiv (ringOfIntegersQuadraticConj hmin hgen)) C = C⁻¹

Quadratic conjugation acts on the class group by inversion. The induced action of quadratic conjugation σ = ringOfIntegersQuadraticConj on Cl(𝓞 K) sends each class to its inverse, because I · σI is principal (isPrincipal_mul_map_ringOfIntegersQuadraticConj). This sharpens mulEquiv_ringOfIntegersQuadraticConj_involutive from an involution to inversion.

source
@[simp]
theorem NumberField.elementaryTwoQuotientCongr_ringOfIntegersQuadraticConj_apply_eq_self {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (x : TauCeti.ClassGroup.ElementaryTwoQuotient (RingOfIntegers K)) :
(TauCeti.ClassGroup.elementaryTwoQuotientCongr (ClassGroup.mulEquiv (ringOfIntegersQuadraticConj hmin hgen))) x = x

Quadratic conjugation acts trivially on Cl(𝓞 K)/Cl(𝓞 K)². Because it acts on Cl(𝓞 K) by inversion (as I · σI is principal), the induced ZMod 2-linear map on the maximal elementary-2 quotient is the identity. This is the capstone reduction feeding the genus-field 2-rank theorems.

source
theorem NumberField.mulEquiv_ringOfIntegersQuadraticConj_apply_eq_self_iff {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (C : ClassGroup (RingOfIntegers K)) :
(ClassGroup.mulEquiv (ringOfIntegersQuadraticConj hmin hgen)) C = C ↔ C ^ 2 = 1

A class is fixed by quadratic conjugation iff it is 2-torsion. Because quadratic conjugation acts on Cl(𝓞 K) by inversion, the classes it fixes are exactly those equal to their own inverse, i.e. the 2-torsion — the ambiguous classes of genus theory.