Units and quadratic conjugation

This file records two sign and square-class consequences for units in a quadratic number field. A unit whose product with its quadratic conjugate is one is, up to sign, totally positive. It follows from Dirichlet's unit theorem that a real quadratic field in which every unit has conjugation norm one has a totally positive unit that is not a square.

These are the archimedean unit inputs to the narrow ambiguous class number formula.

Main results

• NumberField.isTotallyPositive_or_neg_of_mul_ringOfIntegersQuadraticConj_eq_one: a unit of conjugation norm one is, up to sign, totally positive.
• NumberField.exists_isTotallyPositive_notMem_square: under the stated real and norm-one hypotheses, there is a totally positive unit that is not a square.

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

A unit of norm one is ± a totally positive unit. If u σu = 1 then u / σu = u² is totally positive, so u and σu have the same sign at every real place; since every real embedding of a quadratic field is one fixed embedding, or that embedding composed with σ, all real embeddings give u the same sign.

theorem NumberField.isTotallyPositive_or_neg_of_mul_ringOfIntegersQuadraticConj_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} (hnorm : u * (ringOfIntegersQuadraticConj hmin hgen) u = -1) : IsTotallyPositive ↑(θ * u) ∨ IsTotallyPositive (-↑(θ * u))

A nonzero element of norm minus one makes θ times it ± totally positive. The -1 companion of isTotallyPositive_or_neg_of_mul_ringOfIntegersQuadraticConj_eq_one: when u σu = -1 the ratio θu / σ(θu) is the square u ^ 2, so θu and its conjugate have the same sign at every real place. The extra factor θ is what absorbs the sign that the +1 case does not have to.

theorem NumberField.exists_isTotallyPositive_notMem_square {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hreal : ¬IsTotallyComplex K) (hnorm : ∀ (u : (RingOfIntegers K)ˣ), ↑u * (ringOfIntegersQuadraticConj hmin hgen) ↑u = 1) : ∃ (ε : (RingOfIntegers K)ˣ), IsTotallyPositive ↑↑ε ∧ ε ∉ Subgroup.square (RingOfIntegers K)ˣ

A real quadratic field with no unit of norm -1 has a totally positive unit that is not a square. With every unit of norm one, every unit is ± a totally positive unit (isTotallyPositive_or_neg_of_mul_ringOfIntegersQuadraticConj_eq_one); were every totally positive unit a square, the unit group would be generated by -1 together with the squares, so the squares would have index at most 2. But a field with a real place has unit rank 1, where the exact index is 2 ^ (rank + 1) = 4 (NumberField.units_sq_index_eq).