Documentation

TauCeti.NumberTheory.NumberField.Units.Signature.Surjective

The signature map of a number field is surjective #

NumberField.fieldUnitSignature records the sign of an element of Kˣ under each real embedding of a number field K, as a point of the sign group {w : InfinitePlace K // w.IsReal} → ℝˣ ⧸ Units.posSubgroup ℝ. This file proves that every sign pattern is realized: the signature map is surjective, its kernel being the totally positive elements, so Kˣ ⧸ totallyPositiveUnits is the sign group and the totally positive elements have index exactly 2 ^ r₁ in Kˣ, with r₁ the number of real places.

The input is weak approximation at the real places, NumberField.exists_ne_zero_forall_isReal_pos. The analogous unit signature NumberField.unitSignature need not be surjective, so the index of the totally positive units inside (𝓞 K)ˣ need not equal 2 ^ r₁: it is a genuine arithmetic invariant, and the gap between it and 2 ^ r₁ is exactly what the narrow class group measures.

Main results #

References #

The statement that Kˣ realizes every sign pattern is the archimedean half of weak approximation; see J. Neukirch, Algebraic Number Theory, Chapter I, and the discussion of the narrow class group in H. Cohn, A Classical Invitation to Algebraic Numbers and Class Fields.

source
theorem NumberField.fieldUnitSignature_surjective {K : Type u_1} [Field K] [NumberField K] :
Function.Surjective ⇑fieldUnitSignature

The signature map of a number field is surjective. Every assignment of a sign to each real place of K is realized by an element of Kˣ.

This is weak approximation at the real places; it says nothing about the signatures realized by the units of 𝓞 K, which form a genuinely smaller subgroup in general.

source
noncomputable def NumberField.quotientTotallyPositiveUnitsEquiv {K : Type u_1} [Field K] [NumberField K] :
Kˣ ⧸ totallyPositiveUnits ≃* ({ w : InfinitePlace K // w.IsReal } → ℝˣ ⧸ Units.posSubgroup ℝ)

The sign group is the quotient of Kˣ by the totally positive elements.

Equations
Instances For
    source
    @[simp]
    theorem NumberField.quotientTotallyPositiveUnitsEquiv_mk {K : Type u_1} [Field K] [NumberField K] (u : Kˣ) :
    quotientTotallyPositiveUnitsEquiv ↑u = fieldUnitSignature u

    The quotient equivalence sends the class of u : Kˣ to its signature.

    source
    theorem NumberField.card_realSignPatterns {K : Type u_1} [Field K] [NumberField K] :
    Nat.card ({ w : InfinitePlace K // w.IsReal } → ℝˣ ⧸ Units.posSubgroup ℝ) = 2 ^ InfinitePlace.nrRealPlaces K

    There are 2 ^ r₁ sign patterns at the real places, r₁ being their number: the codomain of NumberField.fieldUnitSignature is a product of r₁ two-element sign groups.

    source
    theorem NumberField.index_totallyPositiveUnits {K : Type u_1} [Field K] [NumberField K] :
    totallyPositiveUnits.index = 2 ^ InfinitePlace.nrRealPlaces K

    The totally positive elements of Kˣ have index 2 ^ r₁, with r₁ the number of real places of K. This is the exact value of the index whose finiteness is NumberField.finiteIndex_totallyPositiveUnits.

    source
    @[simp]
    theorem NumberField.totallyPositiveUnits_eq_top_iff {K : Type u_1} [Field K] [NumberField K] :
    totallyPositiveUnits = ⊤ ↔ InfinitePlace.nrRealPlaces K = 0

    Every element of Kˣ is totally positive exactly when K has no real place. One direction is vacuity of total positivity over a totally complex field; the other needs an element of Kˣ negative at a given real place, which is what surjectivity of the signature provides.