Units of norm -1 and total positivity in a quadratic field

Let K = ℚ(√d) be a quadratic number field, presented by θ : 𝓞 K with minpoly ℤ θ = X² - d and Algebra.adjoin ℚ {θ} = ⊤. This file records how a unit of norm -1 interacts with total positivity.

The mechanism is a sign count carried by the norm. Every real embedding of K is one fixed embedding φ, or φ composed with quadratic conjugation σ (NumberField.realRingHom_eq_or_eq_comp_quadraticConj), so the two signs an element x receives are those of φ x and φ (σ x), whose product is N(x). Hence N(x) > 0 says the two signs agree, that is, x or -x is totally positive (NumberField.isTotallyPositive_or_isTotallyPositive_neg_of_norm_pos), and a nonzero element has negative norm exactly when neither it nor its negative is totally positive. Multiplying by a unit of norm -1 exchanges the two cases, so such a unit lets every nonzero x be scaled to a totally positive element by a unit of 𝓞 K. Conversely, when 0 < d the generator has negative norm N(θ) = -d, so a totally positive unit multiple v · θ forces N(v) = -1.

Main results

• NumberField.exists_unit_isTotallyPositive_smul_of_norm_eq_neg_one: a unit of norm -1 makes some unit multiple of every nonzero element totally positive.
• NumberField.norm_eq_neg_one_of_isTotallyPositive_smul_gen: conversely, for 0 < d, a totally positive unit multiple of θ exhibits a unit of norm -1.

References

• D. A. Cox, Primes of the Form x² + ny², §6.A.
• F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

theorem NumberField.exists_unit_isTotallyPositive_smul_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 : ℚ[↑θ] = ⊤) {u : (RingOfIntegers K)ˣ} (hu : (Algebra.norm ℚ) ↑↑u = -1) {x : K} (hx : x ≠ 0) : ∃ (v : (RingOfIntegers K)ˣ), IsTotallyPositive (v • x)

A unit of norm -1 makes some unit multiple of every nonzero element totally positive. An element of positive norm is already totally positive up to sign; one of negative norm is brought to positive norm by the unit of norm -1. This is the archimedean content of the criterion NumberField.NarrowClassGroup.toClassGroup_injective_of_norm_eq_neg_one.

theorem NumberField.norm_eq_neg_one_of_isTotallyPositive_smul_gen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hd : 0 < d) {v : (RingOfIntegers K)ˣ} (hv : IsTotallyPositive (v • ↑θ)) : (Algebra.norm ℚ) ↑↑v = -1

A totally positive unit multiple of θ produces a unit of norm -1. The converse of exists_unit_isTotallyPositive_smul_of_norm_eq_neg_one for a real quadratic field: the scaling unit itself is the unit of norm -1.