Norm-principality for quadratic conjugation

For a quadratic number field K = ℚ(√d) with quadratic conjugation σ = NumberField.ringOfIntegersQuadraticConj, this file proves the genus-theoretic key fact that I · σI is principal for every ideal I of 𝓞 K. This is the hypothesis consumed by NumberField.mulEquiv_ringOfIntegersQuadraticConj_apply_eq_inv.

Along the way it records the elementwise norm identities algebraMap_norm_eq_mul_quadraticConj (N(y) = y · σy for y : K) and algebraMap_norm_eq_mul_ringOfIntegersQuadraticConj (its form for y : 𝓞 K), and their consequence mul_ringOfIntegersQuadraticConj_unit_eq_one_or_neg_one for a unit of 𝓞 K, whose norm is a unit of ℤ. The dictionary between the two ways of writing a norm condition is norm_eq_intCast_iff_mul_ringOfIntegersQuadraticConj_eq_intCast: N(x) = n iff x σx = n.

The proof runs through the relative ideal norm: I · σI has the same relative norm as (Ideal.relNorm ℤ I).map (algebraMap ℤ (𝓞 K)) and contains it, hence equals it, and that extension of a principal ℤ-ideal is principal. The zero ideal needs no separate treatment.

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

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

The norm as a product with the conjugate. Applying Algebra.norm ℚ to y : K and coercing back to K gives the product y · σy of y with its quadratic conjugate.

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

The norm as a product with the conjugate, for an algebraic integer. For x : 𝓞 K, the field norm of x is the image in K of the product x · σx of x with its quadratic conjugate. This is algebraMap_norm_eq_mul_quadraticConj transported along algebraMap (𝓞 K) K.

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

The conjugation norm of a unit is ±1. For a unit u of 𝓞 K in a quadratic number field, u σu is the extension of the integral norm of u, which is a unit of ℤ. Which of the two signs occurs is a genuine invariant of K: -1 is attained in ℚ(√2) and in no imaginary quadratic field.

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

The rational norm reads off the conjugation product. For x : 𝓞 K and an integer n, the field norm N(x) is n exactly when x σx = n: both sides are the image of the other under an injective ring homomorphism, by algebraMap_norm_eq_mul_ringOfIntegersQuadraticConj. It is the translation between the two ways this file and its neighbours state a norm condition.

@[simp]

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

The norm-ideal identity. For quadratic conjugation σ = ringOfIntegersQuadraticConj, the product I · σI is the extension to 𝓞 K of the relative norm ideal relNorm ℤ I.

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

Norm-principality (Lemma A). For quadratic conjugation σ = ringOfIntegersQuadraticConj, the product I · σI is a principal ideal, for every ideal I of 𝓞 K. This is the genus-theoretic hypothesis fed to mulEquiv_ringOfIntegersQuadraticConj_apply_eq_inv.