Documentation

Mathlib.Algebra.Order.Ring.Archimedean

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 ℝ⟦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] [IsStrictOrderedRing R] :

Zero (ArchimedeanClass R)

Equations

@[simp]

theorem ArchimedeanClass.mk_one {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

mk 1 = 0

@[simp]

theorem ArchimedeanClass.top_ne_zero {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

@[simp]

theorem ArchimedeanClass.zero_ne_top {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

instance ArchimedeanClass.instAdd {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

Add (ArchimedeanClass R)

Multiplication in R transfers to addition in ArchimedeanClass R.

Equations

@[simp]

theorem ArchimedeanClass.mk_mul {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] (x y : R) :

mk (x * y) = mk x + mk y

instance ArchimedeanClass.instSMulNat {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

SMul ℕ (ArchimedeanClass R)

Equations

@[simp]

theorem ArchimedeanClass.mk_pow {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] (n : ℕ) (x : R) :

mk (x ^ n) = n • mk x

instance ArchimedeanClass.instAddCommMagma {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

AddCommMagma (ArchimedeanClass R)

Equations

instance ArchimedeanClass.instAddCommMonoid {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

AddCommMonoid (ArchimedeanClass R)

Equations

instance ArchimedeanClass.instIsOrderedAddMonoid {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

IsOrderedAddMonoid (ArchimedeanClass R)

theorem ArchimedeanClass.isAddRegular_mk {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x : R} (hx : x ≠ 0) :

IsAddRegular (mk x)

noncomputable instance ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] :

LinearOrderedAddCommMonoidWithTop (ArchimedeanClass R)

Equations

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

AddValuation R (ArchimedeanClass R)

ArchimedeanClass.mk defines an AddValuation on the ring R.

Equations

Instances For

@[simp]

theorem ArchimedeanClass.addValuation_apply {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] (a : R) :

(addValuation R) a = mk a

@[simp]

theorem ArchimedeanClass.orderHom_zero {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] (f : S →+o R) :

(orderHom f) 0 = mk (f 1)

@[simp]

theorem ArchimedeanClass.mk_eq_zero_of_archimedean {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] {x : S} (h : x ≠ 0) :

mk x = 0

theorem ArchimedeanClass.eq_zero_or_top_of_archimedean {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (x : ArchimedeanClass S) :

x = 0 ∨ x = ⊤

theorem ArchimedeanClass.mk_map_of_archimedean {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+o R) {x : S} (h : x ≠ 0) :

mk (f x) = mk (f 1)

See mk_map_of_archimedean' for a version taking M →+*o R.

theorem ArchimedeanClass.mk_map_of_archimedean' {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : S} (h : x ≠ 0) :

mk (f x) = 0

See mk_map_of_archimedean for a version taking M →+o R.

theorem ArchimedeanClass.mk_le_mk_add_of_archimedean {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) (x : R) (y : S) :

mk x ≤ mk (f y) + mk x

theorem ArchimedeanClass.mk_le_add_mk_of_archimedean {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) (x : R) (y : S) :

mk x ≤ mk x + mk (f y)

theorem ArchimedeanClass.mk_map_nonneg_of_archimedean {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) (y : S) :

0 ≤ mk (f y)

theorem ArchimedeanClass.lt_of_pos_of_archimedean {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : R} (hx : 0 < mk x) {y : S} (hy : 0 < y) :

x < f y

theorem ArchimedeanClass.lt_of_neg_of_archimedean {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : R} (hx : 0 < mk x) {y : S} (hy : y < 0) :

f y < x

@[simp]

theorem ArchimedeanClass.mk_intCast {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] {n : ℤ} (h : n ≠ 0) :

mk ↑n = 0

theorem ArchimedeanClass.mk_intCast_nonneg {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] (n : ℤ) :

0 ≤ mk ↑n

@[simp]

theorem ArchimedeanClass.mk_natCast {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] {n : ℕ} :

n ≠ 0 → mk ↑n = 0

@[simp]

theorem ArchimedeanClass.mk_ofNat {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] {n : ℕ} [n.AtLeastTwo] :

mk (OfNat.ofNat n) = 0

theorem ArchimedeanClass.mk_natCast_nonneg {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] (n : ℕ) :

0 ≤ mk ↑n

theorem ArchimedeanClass.exists_nat_ge_of_mk_nonneg {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ mk x) :

∃ (n : ℕ), x ≤ ↑n

theorem ArchimedeanClass.exists_nat_gt_of_mk_nonneg {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ mk x) :

∃ (n : ℕ), x < ↑n

theorem ArchimedeanClass.exists_int_ge_of_mk_nonneg {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ mk x) :

∃ (n : ℤ), x ≤ ↑n

theorem ArchimedeanClass.exists_int_gt_of_mk_nonneg {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ mk x) :

∃ (n : ℤ), x < ↑n

theorem ArchimedeanClass.exists_int_le_of_mk_nonneg {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ mk x) :

∃ (n : ℤ), ↑n ≤ x

theorem ArchimedeanClass.exists_int_lt_of_mk_nonneg {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {x : R} (hx : 0 ≤ mk x) :

∃ (n : ℤ), ↑n < x

theorem ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean {R : Type u_1} [LinearOrder R] [CommRing R] [IsStrictOrderedRing R] {S : Type u_3} [LinearOrder S] [CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) {x : R} {r s : S} (hr : f r ≤ x) (hs : x ≤ f s) :

0 ≤ mk x

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

theorem ArchimedeanClass.mk_le_mk_iff_denselyOrdered {R : Type u_1} {S : Type u_2} [LinearOrder R] [LinearOrder S] [CommRing R] [IsStrictOrderedRing R] [Ring S] [IsStrictOrderedRing S] [DenselyOrdered R] [Archimedean R] {x y : S} (f : R →+* S) (hf : StrictMono ⇑f) :

mk x ≤ mk y ↔ ∃ (q : R), 0 < f q ∧ f q * |y| ≤ |x|

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

Neg (ArchimedeanClass R)

Equations

@[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

@[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

@[simp]

theorem ArchimedeanClass.mk_div {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] (x y : R) :

mk (x / y) = mk x - mk y

@[simp]

theorem ArchimedeanClass.mk_ratCast {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] {q : ℚ} (h : q ≠ 0) :

mk ↑q = 0

theorem ArchimedeanClass.mk_ratCast_nonneg {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] (q : ℚ) :

0 ≤ mk ↑q

theorem ArchimedeanClass.mk_le_mk_iff_ratCast {R : Type u_1} [LinearOrder R] [Field R] [IsOrderedRing R] {x y : R} :

mk x ≤ mk y ↔ ∃ (q : ℚ), 0 < q ∧ ↑q * |y| ≤ |x|