Archimedean classes of a linearly ordered ring

The archimedean classes of a linearly ordered ring can be given the structure of an AddCommMonoid, by defining

• 0 = mk 1
• mk x + mk y = mk (x * y)

For a linearly ordered field, we can define a negative as

• -mk x = mk x⁻¹

which turns them into a LinearOrderedAddCommGroupWithTop.

Implementation notes

We give Archimedean class an additive structure, rather than a multiplicative one, for the following reasons:

• In the ring version of Hahn embedding theorem, the subtype FiniteArchimedeanClass R of non-top elements in ArchimedeanClass R naturally becomes the additive abelian group for the ring HahnSeries (FiniteArchimedeanClass R) ℝ.
• The order we defined on ArchimedeanClass R matches the order on AddValuation, rather than the one on Valuation.

instance ArchimedeanClass.instZero {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : Zero (ArchimedeanClass R)

Equations

• ArchimedeanClass.instZero = { zero := ArchimedeanClass.mk 1 }

@[simp]

theorem ArchimedeanClass.mk_one {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : mk 1 = 0

instance ArchimedeanClass.instAdd {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : Add (ArchimedeanClass R)

Multipilication in R transfers to Addition in ArchimedeanClass R.

Equations

• ArchimedeanClass.instAdd = { add := ArchimedeanClass.lift₂ (fun (x y : R) => ArchimedeanClass.mk (x * y)) ⋯ }

@[simp]

theorem ArchimedeanClass.mk_mul {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] (x y : R) : mk (x * y) = mk x + mk y

instance ArchimedeanClass.instSMulNat {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : SMul ℕ (ArchimedeanClass R)

Equations

• ArchimedeanClass.instSMulNat = { smul := fun (n : ℕ) => ArchimedeanClass.lift (fun (x : R) => ArchimedeanClass.mk (x ^ n)) ⋯ }

@[simp]

theorem ArchimedeanClass.mk_pow {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] (n : ℕ) (x : R) : mk (x ^ n) = n • mk x

instance ArchimedeanClass.instAddCommMagma {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : AddCommMagma (ArchimedeanClass R)

Equations

• ArchimedeanClass.instAddCommMagma = { toAdd := ArchimedeanClass.instAdd, add_comm := ⋯ }

instance ArchimedeanClass.instAddCommMonoid {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : AddCommMonoid (ArchimedeanClass R)

Equations

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

instance ArchimedeanClass.instIsOrderedAddMonoid {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : IsOrderedAddMonoid (ArchimedeanClass R)

noncomputable instance ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] : LinearOrderedAddCommMonoidWithTop (ArchimedeanClass R)

Equations

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

noncomputable def ArchimedeanClass.addValuation (R : Type u_1) [LinearOrder R] [CommRing R] [IsOrderedRing R] : AddValuation R (ArchimedeanClass R)

ArchimedeanClass.mk defines an AddValuation on the ring R.

Equations

• ArchimedeanClass.addValuation R = AddValuation.of ArchimedeanClass.mk ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ArchimedeanClass.addValuation_apply {R : Type u_1} [LinearOrder R] [CommRing R] [IsOrderedRing R] (a : R) : (addValuation R) a = mk a

theorem ArchimedeanClass.add_left_cancel_of_ne_top {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x y z : ArchimedeanClass R} (hx : x ≠ ⊤) (h : x + y = x + z) : y = z

theorem ArchimedeanClass.add_right_cancel_of_ne_top {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x y z : ArchimedeanClass R} (hx : x ≠ ⊤) (h : y + x = z + x) : y = z

instance ArchimedeanClass.instNeg {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] : Neg (ArchimedeanClass R)

Equations

• ArchimedeanClass.instNeg = { neg := ArchimedeanClass.lift (fun (x : R) => ArchimedeanClass.mk x⁻¹) ⋯ }

@[simp]

theorem ArchimedeanClass.mk_inv {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] (x : R) : mk x⁻¹ = -mk x

instance ArchimedeanClass.instSMulInt {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] : SMul ℤ (ArchimedeanClass R)

Equations

• ArchimedeanClass.instSMulInt = { smul := fun (n : ℤ) => ArchimedeanClass.lift (fun (x : R) => ArchimedeanClass.mk (x ^ n)) ⋯ }

@[simp]

theorem ArchimedeanClass.mk_zpow {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] (n : ℤ) (x : R) : mk (x ^ n) = n • mk x

noncomputable instance ArchimedeanClass.instLinearOrderedAddCommGroupWithTop {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] : LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)

Equations

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