Quadratic conjugation and the real places

Let K = ℚ(√d) be a quadratic number field, presented by θ : 𝓞 K with minpoly ℤ θ = X ^ 2 - d and Algebra.adjoin ℚ {θ} = ⊤, and let σ = quadraticConj be its nontrivial ℚ-automorphism. A ring homomorphism K →+* ℝ is determined by the value it gives θ, and that value is one of the two real square roots of d; so any two real embeddings of K either agree or differ by σ.

The arithmetic consequence recorded here is a sign statement: if z / σz is totally positive then z and σz have the same sign at each real place, and since the real embeddings are φ and φ ∘ σ, all real embeddings of z share one sign. Hence z or -z is totally positive, so the principal ideal (z) has a totally positive generator.

This is the archimedean input to the narrow ambiguous class number formula: it is what replaces the total-complexity hypothesis of the ordinary Hilbert-90 descent (NumberField.exists_map_ringOfIntegersQuadraticConj_eq_self_of_sq_eq_one), where the sign of the norm had to be controlled instead. Layer 3 of the multiquadratic roadmap needs the narrow class group for real quadratic fields, where the ordinary descent fails.

Main results

• NumberField.realRingHom_eq_or_eq_comp_quadraticConj: two real embeddings of a quadratic field either agree or differ by quadratic conjugation.
• NumberField.isTotallyPositive_or_isTotallyPositive_neg_of_isTotallyPositive_div_quadraticConj: if z / σ z is totally positive then z or -z is totally positive.
• NumberField.isTotallyPositive_or_isTotallyPositive_neg_of_norm_pos: an element of positive norm is, up to sign, totally positive.
• NumberField.exists_unit_isTotallyPositive_smul_of_norm_pos: the same statement with the sign read as a unit of 𝓞 K scaling the element to a totally positive one.

theorem NumberField.realRingHom_eq_or_eq_comp_quadraticConj {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (φ ψ : K →+* ℝ) : ψ = φ ∨ ∀ (x : K), ψ x = φ ((quadraticConj hmin hgen) x)

The real embeddings of a quadratic field differ by conjugation. Since ρ θ squares to the rational d for every ring homomorphism ρ : K →+* ℝ, two of them send θ to the same square root of d — in which case they agree — or to opposite ones, in which case one is the other precomposed with quadratic conjugation.

theorem NumberField.isTotallyPositive_or_isTotallyPositive_neg_of_isTotallyPositive_div_quadraticConj {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) {z : K} (h : IsTotallyPositive (z / (quadraticConj hmin hgen) z)) : IsTotallyPositive z ∨ IsTotallyPositive (-z)

A quotient by its conjugate that is totally positive forces a sign. If z / σ z is totally positive, then z and σ z have the same sign at each real place; since every real embedding is either φ or φ ∘ σ for one fixed φ, all real embeddings of z have the same sign, so z or -z is totally positive. Over a totally complex field both alternatives hold vacuously.

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

Positive norm forces a sign. In a quadratic field the norm of x is the product of the two values φ x and φ (σ x) that the real embeddings give x, so a positive norm says those values have the same sign and hence that x or -x is totally positive. Over a totally complex field both alternatives hold vacuously.

theorem NumberField.exists_unit_isTotallyPositive_smul_of_norm_pos {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) {y : K} (hnorm : 0 < (Algebra.norm ℚ) y) : ∃ (ε : (RingOfIntegers K)ˣ), IsTotallyPositive (ε • y)

An element of positive norm has a totally positive unit multiple. The unit-scaling form of isTotallyPositive_or_isTotallyPositive_neg_of_norm_pos: since -1 is a unit of 𝓞 K, the two alternatives of that sign statement are a single existential over the units. This is the shape in which a narrow principal class is shown to be trivial.