Documentation

TauCeti.NumberTheory.NumberField.Units.Signature.Integer

The total sign homomorphism of a number field, valued in ℤˣ #

NumberField.fieldUnitSignature records the sign of a field unit of K at each real place as a class in ℝˣ ⧸ Units.posSubgroup ℝ. Transporting each of those classes along the sign isomorphism Units.signEquiv gives the same data in the concrete two-element group ℤˣ:

signHom : Kˣ →* ({w : InfinitePlace K // w.IsReal} → ℤˣ).

This is the archimedean half of a multiplicative congruence in group-theoretic form: x is totally positive exactly when signHom x = 1. There is no second sign homomorphism here — this is NumberField.fieldUnitSignature read in ℤˣ, and the two are interchangeable through Units.signEquiv.

Surjectivity of signHom is not formal — it is weak approximation at the real places, and is inherited from NumberField.fieldUnitSignature_surjective. The composite (𝓞 K)ˣ → Kˣ → ({w // w.IsReal} → ℤˣ) need not be surjective, and its failure to be so is exactly the obstruction that separates the narrow class group from the wide one; nothing here asserts otherwise.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.GlobalNumberFields.signHom {K : Type u_1} [Field K] :
Kˣ →* { w : NumberField.InfinitePlace K // w.IsReal } → ℤˣ

The total sign homomorphism of a number field: the signs of a field unit of K at all of the real places at once, valued in the product of copies of ℤˣ indexed by those places.

It is NumberField.fieldUnitSignature with each component read through the sign isomorphism Units.signEquiv, so it carries exactly the same information.

The domain is Kˣ rather than K, so that every value really is a sign: a formulation on K would have to invent a sign for 0.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.signHom_apply {K : Type u_1} [Field K] (x : Kˣ) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :
    signHom x w = (Units.signEquiv ℝ) (NumberField.fieldUnitSignature x w)

    Componentwise evaluation of the total sign homomorphism.

    source
    theorem TauCeti.GlobalNumberFields.signHom_apply_eq_one_iff {K : Type u_1} [Field K] (x : Kˣ) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :
    signHom x w = 1 ↔ 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑x

    A sign is 1 exactly at a positive element.

    source
    theorem TauCeti.GlobalNumberFields.signHom_apply_eq_neg_one_iff {K : Type u_1} [Field K] (x : Kˣ) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :
    signHom x w = -1 ↔ (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑x < 0

    A sign is -1 exactly at a negative element.

    source
    @[simp]
    theorem TauCeti.GlobalNumberFields.signHom_eq_one_iff {K : Type u_1} [Field K] (x : Kˣ) :
    signHom x = 1 ↔ NumberField.IsTotallyPositive ↑x

    The kernel of the total sign homomorphism is the totally positive elements.

    source
    theorem TauCeti.GlobalNumberFields.signHom_surjective {K : Type u_1} [Field K] [NumberField K] :
    Function.Surjective ⇑signHom

    The total sign homomorphism is surjective on Kˣ. Every pattern of signs at the real places of K is realized by an element of Kˣ.

    This is NumberField.fieldUnitSignature_surjective read in ℤˣ. Surjectivity fails in general after restricting along (𝓞 K)ˣ → Kˣ, and that failure is the obstruction which separates the narrow class group of K from the wide one; nothing here bears on the restricted map.