Documentation

TauCeti.Algebra.Order.Ring.Units

The sign group of a linearly ordered ring #

For a linearly ordered ring, the positive units Units.posSubgroup R form an index-2 subgroup, so it has finite index. Together with the general finite-index-preimage instance (Subgroup.instFiniteIndexComap), this yields the finiteness of the totally positive units of a number field, hence of its narrow class group.

Being of index 2, the quotient Rˣ ⧸ Units.posSubgroup R is the two-element sign group; Units.signEquiv identifies it with ℤˣ, which is how a sign is usually presented concretely.

Main definitions and results #

source
instance Units.instFiniteIndexPosSubgroup (R : Type u_1) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] :
(posSubgroup R).FiniteIndex

The positive units of a linearly ordered ring form an index-2, hence finite-index, subgroup.

source
theorem Units.instNormalPosSubgroup_tauCeti {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] :
(posSubgroup R).Normal
source
noncomputable def Units.signEquiv (R : Type u_1) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] :
Rˣ ⧸ posSubgroup R ≃* ℤˣ

The sign isomorphism of a linearly ordered ring. The units of R modulo the positive ones form the two-element sign group ℤˣ, the class of a unit being its sign.

The class of a positive unit is sent to 1 and the class of a negative unit to -1; these two values are read off by Units.signEquiv_mk_eq_one_iff and Units.signEquiv_mk_eq_neg_one_iff.

Equations
Instances For
    source
    theorem Units.signEquiv_mk_eq_one_iff {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (u : Rˣ) :
    (signEquiv R) ↑u = 1 ↔ 0 < ↑u

    The sign of a unit is 1 exactly when the unit is positive.

    source
    @[simp]
    theorem Units.signEquiv_mk_eq_neg_one_iff {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (u : Rˣ) :
    (signEquiv R) ↑u = -1 ↔ ↑u < 0

    The sign of a unit is -1 exactly when the unit is negative.