The field norm on a quadratic number field

For a quadratic number field K = ℚ(√d) presented by an algebraic integer θ : 𝓞 K generating K over ℚ with minpoly ℤ θ = X² - d, this file computes the field norm Algebra.norm ℚ on K in terms of the coordinates in the basis 1, θ:

• norm_gen_eq_neg_radicand: the norm of the generator, N(θ) = -d (negative of the radicand);
• norm_add_mul_gen: in the coordinates x = b + aθ the norm is N(b + aθ) = b² - d·a², and TauCeti.NumberField.norm_int_add_mul_gen is the same formula for the integer norm on 𝓞 K;
• norm_pos_of_radicand_neg: when d < 0 — the imaginary quadratic case, where K is totally complex — the norm is strictly positive on every nonzero element;
• radicand_pos_of_norm_eq_neg_one: consequently an element of norm -1 forces 0 < d;
• exists_norm_eq_neg_one_of_sq_sub_mul_sq_eq_neg_one: a solution of the negative Pell equation b² - d a² = -1 supplies a unit of norm -1.

The positivity is a descent input for the genus theory of the multiquadratic roadmap: for a norm-±1 element α it upgrades N(α) = ±1 to N(α) = 1, the hypothesis of Hilbert's Theorem 90 used to realise a 2-torsion class by an ambiguous ideal.

See D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws.

@[simp]

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

The norm of the generator is the negative of the radicand: N(θ) = -d. It is the constant coefficient of the minimal polynomial X² - d, times the sign (-1)^{[K:ℚ]} = +1.

@[simp]

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

The norm in the basis 1, θ: N(b + aθ) = b² - d·a². This is the generic quadratic norm formula with Tr(θ) = 0 and N(θ) = -d. The left-hand side uses the rat-cast normal form ↑b + ↑a * θ (simp rewrites algebraMap ℚ K to ↑ via eq_ratCast), so it is a valid @[simp] normalization rule.

@[simp]

theorem TauCeti.NumberField.norm_int_add_mul_gen {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (a b : ℤ) : (Algebra.norm ℤ) (↑b + ↑a * θ) = b ^ 2 - d * a ^ 2

The integer norm in the basis 1, θ: on 𝓞 K, N(b + aθ) = b² - d·a² for integers a, b. This is norm_add_mul_gen read through Algebra.coe_norm_int.

theorem NumberField.norm_pos_of_radicand_neg {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hd : d < 0) {x : K} (hx : x ≠ 0) : 0 < (Algebra.norm ℚ) x

The norm is positive in the imaginary case. When d < 0 the field K = ℚ(√d) is totally complex, and N(b + aθ) = b² + |d|·a², so the norm is strictly positive on every nonzero element. This is the sign input that turns a norm-±1 element into a norm-1 one for Hilbert 90.

theorem NumberField.radicand_pos_of_norm_eq_neg_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) {x : K} (hx : (Algebra.norm ℚ) x = -1) : 0 < d

An element of norm -1 only exists in the real case. For d < 0 the norm is positive on every nonzero element (norm_pos_of_radicand_neg), and d = 0 is excluded because the radicand is not a square; so an element of norm -1 forces 0 < d.

theorem NumberField.exists_norm_eq_neg_one_of_sq_sub_mul_sq_eq_neg_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) {a b : ℤ} (hab : b ^ 2 - d * a ^ 2 = -1) : ∃ (u : (RingOfIntegers K)ˣ), (Algebra.norm ℚ) ↑↑u = -1

A solution of the negative Pell equation gives a unit of norm -1. If b² - d a² = -1 then b + aθ has norm -1, hence is a unit of 𝓞 K (an algebraic integer is a unit exactly when its norm is ±1). This is a concrete source of units of norm -1: for d = 2, a = b = 1 gives the unit 1 + √2.