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. The case N(u) = 1 of isTotallyPositive_or_isTotallyPositive_neg_of_norm_pos, with the norm hypothesis written in the conjugation form u σu = 1 in which the descent arguments of this area produce it.

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: an element of norm -1 need not be ± totally positive, but θ has norm -d, so the extra factor θ restores the positive norm and with it the sign that the +1 case has for free.

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).