Totally positive elements of a number field

An element x of a number field K is totally positive when it is strictly positive under every real embedding K →+* ℝ — equivalently, at every real infinite place. This is the archimedean positivity condition underlying the narrow class group of the multiquadratic roadmap (Layer 3): the narrow class group Cl⁺(K) is the quotient of the fractional ideals by the principal ideals admitting a totally positive generator. It surjects onto the ordinary class group Cl(K) (forgetting the positivity condition), and the 2-rank of Cl⁺(K) is what the genus-theory t - 1 formula (with t the number of ramified primes) computes for a real quadratic field in the multiquadratic roadmap.

This file introduces the predicate and its multiplicative structure. The totally positive elements are closed under multiplication and inversion and contain every nonzero square, so the totally positive units form a subgroup of Kˣ. That subgroup is the kernel of the sign (signature) map on units; the signs not realized by units measure the difference between Cl⁺(K) and Cl(K).

The file also records that totallyPositiveUnits has finite index — a finite intersection, over the real places, of the finite-index preimages of the positive units of ℝ — which is what makes the narrow class group finite (see NarrowClassGroup.Finite).

Main definitions and results

• NumberField.IsTotallyPositive: strict positivity at every real place, with isTotallyPositive_iff its introduction/elimination form.
• NumberField.isTotallyPositive_one, IsTotallyPositive.mul, IsTotallyPositive.inv, IsTotallyPositive.map, isTotallyPositive_sq: the multiplicative and functorial structure, including that nonzero squares are totally positive.
• NumberField.isTotallyPositive_ratCast: a positive rational number is totally positive, with NumberField.isTotallyPositive_intCast its integer special case.
• NumberField.totallyPositiveUnits: the subgroup of totally positive units of Kˣ (the kernel of the unit signature map), with sq_mem_totallyPositiveUnits. For a totally complex field it is everything (totallyPositiveUnits_eq_top), since total positivity is then vacuous (not_isReal_of_isTotallyComplex makes IsTotallyPositive simp to True).
• NumberField.totallyPositiveIntegerUnits: the corresponding subgroup of the arithmetic units (𝓞 K)ˣ, the preimage of totallyPositiveUnits under (𝓞 K)ˣ → Kˣ, with mem_totallyPositiveIntegerUnits and sq_mem_totallyPositiveIntegerUnits.
• NumberField.exists_isTotallyPositive_sub_mem: every residue class modulo a nonzero ideal of 𝓞 K contains a nonzero totally positive integer.
• NumberField.norm_nonneg_of_isTotallyPositive: the field norm of a totally positive element is nonnegative, and NumberField.norm_pos_of_isTotallyPositive: for a nonzero such element it is strictly positive.
• NumberField.finiteIndex_totallyPositiveUnits: totallyPositiveUnits has finite index (via Units.instFiniteIndexPosSubgroup and the general Subgroup.instFiniteIndexComap).

def NumberField.IsTotallyPositive {K : Type u_1} [Field K] (x : K) : Prop

An element of a number field is totally positive when it is strictly positive under every real embedding K →+* ℝ (equivalently, at every real infinite place w). For a totally complex field the condition is vacuous; the content is at the real places.

Equations

• NumberField.IsTotallyPositive x = ∀ (w : NumberField.InfinitePlace K) (hw : w.IsReal), 0 < (NumberField.InfinitePlace.embedding_of_isReal hw) x

@[simp]

theorem NumberField.isTotallyPositive_iff {K : Type u_1} [Field K] {x : K} : IsTotallyPositive x ↔ ∀ (w : InfinitePlace K) (hw : w.IsReal), 0 < (InfinitePlace.embedding_of_isReal hw) x

Introduction and elimination form of IsTotallyPositive: total positivity is exactly strict positivity at every real infinite place.

theorem NumberField.isTotallyPositive_one {K : Type u_1} [Field K] : IsTotallyPositive 1

The element 1 is totally positive: every real embedding sends it to 1 > 0.

theorem NumberField.IsTotallyPositive.map {K : Type u_1} [Field K] {L : Type u_2} [Field L] (f : K →+* L) {x : K} (hx : IsTotallyPositive x) : IsTotallyPositive (f x)

A homomorphism of number fields sends totally positive elements to totally positive elements: every real place of the target restricts to a real place of the source.

theorem NumberField.IsTotallyPositive.mul {K : Type u_1} [Field K] {x y : K} (hx : IsTotallyPositive x) (hy : IsTotallyPositive y) : IsTotallyPositive (x * y)

Totally positive elements are closed under multiplication: a product of positives is positive at each real place.

theorem NumberField.IsTotallyPositive.inv {K : Type u_1} [Field K] {x : K} (hx : IsTotallyPositive x) : IsTotallyPositive x⁻¹

A totally positive element has a totally positive inverse: real embeddings send inverses to inverses, and the reciprocal of a positive real is positive.

theorem NumberField.isTotallyPositive_sq {K : Type u_1} [Field K] {x : K} (hx : x ≠ 0) : IsTotallyPositive (x ^ 2)

Every nonzero square is totally positive: at each real place its value is the square of a nonzero real.

theorem NumberField.isTotallyPositive_ratCast {K : Type u_1} [Field K] {q : ℚ} (hq : 0 < q) : IsTotallyPositive ↑q

A positive rational number is totally positive in any field: every real embedding fixes it. The cast is Rat.cast, which agrees with algebraMap ℚ K whenever the latter is available.

theorem NumberField.isTotallyPositive_intCast {K : Type u_1} [Field K] {n : ℤ} (hn : 0 < n) : IsTotallyPositive ↑n

A positive rational integer is totally positive: the integer special case of isTotallyPositive_ratCast.

noncomputable def NumberField.totallyPositiveUnits {K : Type u_1} [Field K] : Subgroup Kˣ

The subgroup of totally positive units of Kˣ: the intersection, over the real infinite places w, of the preimages of the positive units of ℝ under the real embedding w. It is the kernel of the sign (signature) map on units, and controls the comparison between the narrow class group Cl⁺(K) and the ordinary class group Cl(K).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumberField.mem_totallyPositiveUnits {K : Type u_1} [Field K] {u : Kˣ} : u ∈ totallyPositiveUnits ↔ IsTotallyPositive ↑u

A unit lies in totallyPositiveUnits exactly when its underlying field element is totally positive.

theorem NumberField.sq_mem_totallyPositiveUnits {K : Type u_1} [Field K] (u : Kˣ) : u ^ 2 ∈ totallyPositiveUnits

Every square of a unit is a totally positive unit.

@[simp]

theorem NumberField.not_isReal_of_isTotallyComplex {K : Type u_1} [Field K] [IsTotallyComplex K] (w : InfinitePlace K) : ¬w.IsReal

A totally complex field has no real infinite places. As a simp lemma this discharges the vacuous real-place hypotheses in totally-positive statements: IsTotallyPositive x then reduces to True (via isTotallyPositive_iff), so total positivity is automatic for every element.

@[simp]

theorem NumberField.totallyPositiveUnits_eq_top {K : Type u_1} [Field K] [IsTotallyComplex K] : totallyPositiveUnits = ⊤

For a totally complex field every unit is (vacuously) totally positive: totallyPositiveUnits = ⊤.

noncomputable def NumberField.totallyPositiveIntegerUnits {K : Type u_1} [Field K] : Subgroup (RingOfIntegers K)ˣ

The subgroup of totally positive integer units of (𝓞 K)ˣ: the preimage of totallyPositiveUnits under the inclusion (𝓞 K)ˣ → Kˣ, i.e. the integer units whose image in K is totally positive. It is the kernel of the integer-unit signature map; the signatures realized by units — the quotient of (𝓞 K)ˣ by this subgroup — are the archimedean input to the comparison between the narrow and ordinary class groups.

Equations

• NumberField.totallyPositiveIntegerUnits = Subgroup.comap (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) NumberField.totallyPositiveUnits

@[simp]

theorem NumberField.mem_totallyPositiveIntegerUnits {K : Type u_1} [Field K] {u : (RingOfIntegers K)ˣ} : u ∈ totallyPositiveIntegerUnits ↔ IsTotallyPositive ((algebraMap (RingOfIntegers K) K) ↑u)

Membership in totallyPositiveIntegerUnits is total positivity of the image in K.

theorem NumberField.sq_mem_totallyPositiveIntegerUnits {K : Type u_1} [Field K] (u : (RingOfIntegers K)ˣ) : u ^ 2 ∈ totallyPositiveIntegerUnits

Every square of an integer unit is a totally positive integer unit.

@[simp]

theorem NumberField.totallyPositiveIntegerUnits_eq_top {K : Type u_1} [Field K] [IsTotallyComplex K] : totallyPositiveIntegerUnits = ⊤

For a totally complex field every integer unit is (vacuously) totally positive: totallyPositiveIntegerUnits = ⊤.

theorem NumberField.exists_isTotallyPositive_sub_mem {K : Type u_1} [Field K] [NumberField K] {H : Ideal (RingOfIntegers K)} (hH : H ≠ ⊥) (a : RingOfIntegers K) : ∃ (b : RingOfIntegers K), b ≠ 0 ∧ b - a ∈ H ∧ IsTotallyPositive ↑b

Every residue class modulo a nonzero ideal contains a nonzero totally positive integer. Adding a large enough multiple of the square of a nonzero element of H makes every real embedding of a positive without moving a out of its class modulo H.

This is the archimedean adjustment behind any construction that has to reconcile an ideal-theoretic congruence with the real places, such as choosing a coprime representative of a narrow ideal class or a generator congruent to one modulo a ray-class modulus.

theorem NumberField.norm_nonneg_of_isTotallyPositive {K : Type u_1} [Field K] [NumberField K] {x : K} (hpos : IsTotallyPositive x) : 0 ≤ (Algebra.norm ℚ) x

The norm of a totally positive element is nonnegative.

Over a totally complex field the hypothesis is vacuous (not_isReal_of_isTotallyComplex), so the conclusion holds for every x there, including x = 0 whose norm is 0.

theorem NumberField.norm_pos_of_isTotallyPositive {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) (hpos : IsTotallyPositive x) : 0 < (Algebra.norm ℚ) x

The norm of a nonzero totally positive element is positive.

Over a totally complex field the hypothesis IsTotallyPositive x is vacuous (not_isReal_of_isTotallyComplex), so this covers imaginary quadratic fields as a special case.

instance NumberField.finiteIndex_totallyPositiveUnits {K : Type u_1} [Field K] [NumberField K] : totallyPositiveUnits.FiniteIndex

totallyPositiveUnits has finite index in Kˣ: it is a finite intersection, over the real infinite places, of the finite-index preimages of the positive units of ℝ (via the general Units.instFiniteIndexPosSubgroup and Subgroup.instFiniteIndexComap).