Quadratic conjugation on a quadratic number field

For a quadratic number field K — presented by an algebraic integer θ : 𝓞 K generating K over ℚ whose minimal polynomial over ℤ is X² - d — this file constructs the nontrivial ℚ-algebra automorphism of K, characterised by θ ↦ -θ, and restricts it to a ring automorphism of 𝓞 K. This is the field-theoretic conjugation of ℚ(√d).

It is the field-theoretic conjugation underlying the genus theory of the multiquadratic roadmap (Layer 3): downstream (Conjugation/ClassGroup.lean), its induced action on the class group Cl(𝓞 K) is shown to be by inversion — the fact that I · σI is principal — the mechanism behind the summit isomorphism Gal(K_gen/K) ≅ Cl(K)/Cl(K)². Here we build the automorphism and record that it is an involution on K and on 𝓞 K.

See D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws, for the classical genus theory this supports.

Main definitions and results

• NumberField.quadraticConj: the conjugation K ≃ₐ[ℚ] K, sending θ ↦ -θ, with quadraticConj_gen (quadraticConj θ = -θ), quadraticConj_ne_one and quadraticConj_involutive.
• NumberField.ringOfIntegersQuadraticConj: its restriction to a ring automorphism 𝓞 K ≃+* 𝓞 K, with coe_ringOfIntegersQuadraticConj, ringOfIntegersQuadraticConj_gen, and ringOfIntegersQuadraticConj_involutive.

noncomputable def NumberField.quadraticConj {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : Gal(K/ℚ)

Quadratic conjugation. The nontrivial ℚ-automorphism of the quadratic field K = ℚ(√d), characterised by θ ↦ -θ. Since θ and -θ share a minimal polynomial, it is the PowerBasis.equivOfMinpoly between their power bases.

Equations

• NumberField.quadraticConj hmin hgen = (NumberField.quadraticPowerBasis✝ hgen).equivOfMinpoly (NumberField.quadraticPowerBasisNeg✝ hgen) ⋯

@[simp]

theorem NumberField.quadraticConj_gen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : (quadraticConj hmin hgen) ↑θ = -↑θ

Quadratic conjugation sends the generator θ to -θ.

theorem NumberField.quadraticConj_ne_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : quadraticConj hmin hgen ≠ 1

Quadratic conjugation is nontrivial: it is not the identity, since it sends the nonzero generator θ to its negative -θ.

@[simp]

theorem NumberField.quadraticConj_involutive {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : Function.Involutive ⇑(quadraticConj hmin hgen)

Quadratic conjugation is an involution on K (applying it twice is the identity).

noncomputable def NumberField.ringOfIntegersQuadraticConj {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : RingOfIntegers K ≃+* RingOfIntegers K

Quadratic conjugation on the ring of integers. The restriction of quadraticConj to 𝓞 K, a ring automorphism 𝓞 K ≃+* 𝓞 K. This is the automorphism whose action on ClassGroup (𝓞 K) is by inversion (the genus-theoretic fact that I · σI is principal).

Equations

• NumberField.ringOfIntegersQuadraticConj hmin hgen = NumberField.RingOfIntegers.mapRingEquiv (NumberField.quadraticConj hmin hgen).toRingEquiv

@[simp]

theorem NumberField.coe_ringOfIntegersQuadraticConj {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (x : RingOfIntegers K) : ↑((ringOfIntegersQuadraticConj hmin hgen) x) = (quadraticConj hmin hgen) ↑x

Passing to K, ringOfIntegersQuadraticConj x is quadraticConj of the image of x.

@[simp]

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

Quadratic conjugation on 𝓞 K sends the generator θ to -θ.

@[simp]

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

Quadratic conjugation is an involution on 𝓞 K (applying it twice is the identity).