Archimedean classes of a linearly ordered group

This file defines archimedean classes of a given linearly ordered group. Archimedean classes measure to what extent the group fails to be Archimedean. For additive group, elements a and b in the same class are "equivalent" in the sense that there exist two natural numbers m and n such that |a| ≤ m • |b| and |b| ≤ n • |a|. An element a in a higher class than b is "infinitesimal" to b in the sense that n • |a| < |b| for all natural number n.

Main definitions

• ArchimedeanClass is the archimedean class for additive linearly ordered group.
• MulArchimedeanClass is the archimedean class for multiplicative linearly ordered group.
• ArchimedeanClass.orderHom and MulArchimedeanClass.orderHom are OrderHom over archimedean classes lifted from ordered group homomorphisms.

Main statements

The following theorems state that an ordered commutative group is (mul-)archimedean if and only if all non-identity elements belong to the same (Mul-)ArchimedeanClass:

• ArchimedeanClass.archimedean_of_mk_eq_mk / MulArchimedeanClass.mulArchimedean_of_mk_eq_mk
• ArchimedeanClass.mk_eq_mk_of_archimedean / MulArchimedeanClass.mk_eq_mk_of_mulArchimedean

Implementation notes

Archimedean classes are equipped with a linear order, where elements with smaller absolute value are placed in a higher classes by convention. Ordering backwards this way simplifies formalization of theorems such as the Hahn embedding theorem.

To naturally derive this order, we first define it on the underlying group via the type synonym (Mul-)ArchimedeanOrder, and define (Mul-)ArchimedeanClass as Antisymmetrization of the order.

def MulArchimedeanOrder (M : Type u_1) : Type u_1

Type synonym to equip a ordered group with a new Preorder defined by the infinitesimal order of elements. a is said less than b if b is infinitesimal comparing to a, or more precisely, ∀ n, |b|ₘ ^ n < |a|ₘ. If a and b are neither infinitesimal to each other, they are equivalent in this order.

Equations

• MulArchimedeanOrder M = M

def ArchimedeanOrder (M : Type u_1) : Type u_1

Type synonym to equip a ordered group with a new Preorder defined by the infinitesimal order of elements. a is said less than b if b is infinitesimal comparing to a, or more precisely, ∀ n, n • |b| < |a|. If a and b are neither infinitesimal to each other, they are equivalent in this order.

Equations

• ArchimedeanOrder M = M

def MulArchimedeanOrder.of {M : Type u_1} : M ≃ MulArchimedeanOrder M

Create a MulArchimedeanOrder element from the underlying type.

Equations

• MulArchimedeanOrder.of = Equiv.refl M

def ArchimedeanOrder.of {M : Type u_1} : M ≃ ArchimedeanOrder M

Create a ArchimedeanOrder element from the underlying type.

Equations

• ArchimedeanOrder.of = Equiv.refl M

def MulArchimedeanOrder.val {M : Type u_1} : MulArchimedeanOrder M ≃ M

Retrieve the underlying value from a MulArchimedeanOrder element.

Equations

• MulArchimedeanOrder.val = Equiv.refl (MulArchimedeanOrder M)

def ArchimedeanOrder.val {M : Type u_1} : ArchimedeanOrder M ≃ M

Retrieve the underlying value from a ArchimedeanOrder element.

Equations

• ArchimedeanOrder.val = Equiv.refl (ArchimedeanOrder M)

@[simp]

theorem MulArchimedeanOrder.of_symm_eq {M : Type u_1} : of.symm = val

@[simp]

theorem ArchimedeanOrder.of_symm_eq {M : Type u_1} : of.symm = val

@[simp]

theorem MulArchimedeanOrder.val_symm_eq {M : Type u_1} : val.symm = of

@[simp]

theorem ArchimedeanOrder.val_symm_eq {M : Type u_1} : val.symm = of

@[simp]

theorem MulArchimedeanOrder.of_val {M : Type u_1} (a : MulArchimedeanOrder M) : of (val a) = a

@[simp]

theorem ArchimedeanOrder.of_val {M : Type u_1} (a : ArchimedeanOrder M) : of (val a) = a

@[simp]

theorem MulArchimedeanOrder.val_of {M : Type u_1} (a : M) : val (of a) = a

@[simp]

theorem ArchimedeanOrder.val_of {M : Type u_1} (a : M) : val (of a) = a

instance MulArchimedeanOrder.instLE {M : Type u_1} [Group M] [Lattice M] : LE (MulArchimedeanOrder M)

Equations

• MulArchimedeanOrder.instLE = { le := fun (a b : MulArchimedeanOrder M) => ∃ (n : ℕ), mabs (MulArchimedeanOrder.val b) ≤ mabs (MulArchimedeanOrder.val a) ^ n }

instance ArchimedeanOrder.instLE {M : Type u_1} [AddGroup M] [Lattice M] : LE (ArchimedeanOrder M)

Equations

• ArchimedeanOrder.instLE = { le := fun (a b : ArchimedeanOrder M) => ∃ (n : ℕ), |ArchimedeanOrder.val b| ≤ n • |ArchimedeanOrder.val a| }

instance MulArchimedeanOrder.instLT {M : Type u_1} [Group M] [Lattice M] : LT (MulArchimedeanOrder M)

Equations

• MulArchimedeanOrder.instLT = { lt := fun (a b : MulArchimedeanOrder M) => ∀ (n : ℕ), mabs (MulArchimedeanOrder.val b) ^ n < mabs (MulArchimedeanOrder.val a) }

instance ArchimedeanOrder.instLT {M : Type u_1} [AddGroup M] [Lattice M] : LT (ArchimedeanOrder M)

Equations

• ArchimedeanOrder.instLT = { lt := fun (a b : ArchimedeanOrder M) => ∀ (n : ℕ), n • |ArchimedeanOrder.val b| < |ArchimedeanOrder.val a| }

theorem MulArchimedeanOrder.le_def {M : Type u_1} [Group M] [Lattice M] {a b : MulArchimedeanOrder M} : a ≤ b ↔ ∃ (n : ℕ), mabs (val b) ≤ mabs (val a) ^ n

theorem ArchimedeanOrder.le_def {M : Type u_1} [AddGroup M] [Lattice M] {a b : ArchimedeanOrder M} : a ≤ b ↔ ∃ (n : ℕ), |val b| ≤ n • |val a|

theorem MulArchimedeanOrder.lt_def {M : Type u_1} [Group M] [Lattice M] {a b : MulArchimedeanOrder M} : a < b ↔ ∀ (n : ℕ), mabs (val b) ^ n < mabs (val a)

theorem ArchimedeanOrder.lt_def {M : Type u_1} [AddGroup M] [Lattice M] {a b : ArchimedeanOrder M} : a < b ↔ ∀ (n : ℕ), n • |val b| < |val a|

instance MulArchimedeanOrder.instPreorder {M : Type u_2} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Preorder (MulArchimedeanOrder M)

Equations

• MulArchimedeanOrder.instPreorder = { toLE := MulArchimedeanOrder.instLE, toLT := MulArchimedeanOrder.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance ArchimedeanOrder.instPreorder {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Preorder (ArchimedeanOrder M)

Equations

• ArchimedeanOrder.instPreorder = { toLE := ArchimedeanOrder.instLE, toLT := ArchimedeanOrder.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance MulArchimedeanOrder.instIsTotalLe {M : Type u_2} [CommGroup M] [LinearOrder M] : IsTotal (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) => x1 ≤ x2

instance ArchimedeanOrder.instIsTotalLe {M : Type u_2} [AddCommGroup M] [LinearOrder M] : IsTotal (ArchimedeanOrder M) fun (x1 x2 : ArchimedeanOrder M) => x1 ≤ x2

noncomputable def MulArchimedeanOrder.orderHom {M : Type u_2} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_3} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) : MulArchimedeanOrder M →o MulArchimedeanOrder N

An OrderMonoidHom can be made to an OrderHom between their MulArchimedeanOrder.

Equations

• MulArchimedeanOrder.orderHom f = { toFun := fun (a : MulArchimedeanOrder M) => MulArchimedeanOrder.of (f (MulArchimedeanOrder.val a)), monotone' := ⋯ }

noncomputable def ArchimedeanOrder.orderHom {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_3} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) : ArchimedeanOrder M →o ArchimedeanOrder N

An OrderAddMonoidHom can be made to an OrderHom between their ArchimedeanOrder.

Equations

• ArchimedeanOrder.orderHom f = { toFun := fun (a : ArchimedeanOrder M) => ArchimedeanOrder.of (f (ArchimedeanOrder.val a)), monotone' := ⋯ }

def MulArchimedeanClass (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Type u_1

MulArchimedeanClass is the antisymmetrization of MulArchimedeanOrder.

Equations

• MulArchimedeanClass M = Antisymmetrization (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) => x1 ≤ x2

def ArchimedeanClass (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Type u_1

ArchimedeanClass is the antisymmetrization of ArchimedeanOrder.

Equations

• ArchimedeanClass M = Antisymmetrization (ArchimedeanOrder M) fun (x1 x2 : ArchimedeanOrder M) => x1 ≤ x2

def MulArchimedeanClass.mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a : M) : MulArchimedeanClass M

The archimedean class of a given element.

Equations

• MulArchimedeanClass.mk a = toAntisymmetrization (fun (x1 x2 : MulArchimedeanOrder M) => x1 ≤ x2) (MulArchimedeanOrder.of a)

def ArchimedeanClass.mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : M) : ArchimedeanClass M

The archimedean class of a given element.

Equations

• ArchimedeanClass.mk a = toAntisymmetrization (fun (x1 x2 : ArchimedeanOrder M) => x1 ≤ x2) (ArchimedeanOrder.of a)

theorem MulArchimedeanClass.ind {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {motive : MulArchimedeanClass M → Prop} (mk : ∀ (a : M), motive (mk a)) (x : MulArchimedeanClass M) : motive x

An induction principle for MulArchimedeanClass.

theorem ArchimedeanClass.ind {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {motive : ArchimedeanClass M → Prop} (mk : ∀ (a : M), motive (mk a)) (x : ArchimedeanClass M) : motive x

An induction principle for ArchimedeanClass

theorem MulArchimedeanClass.mk_surjective (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Function.Surjective mk

theorem ArchimedeanClass.mk_surjective (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Function.Surjective mk

@[simp]

theorem MulArchimedeanClass.range_mk (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Set.range mk = Set.univ

@[simp]

theorem ArchimedeanClass.range_mk (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Set.range mk = Set.univ

theorem MulArchimedeanClass.mk_eq_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} : mk a = mk b ↔ (∃ (m : ℕ), mabs b ≤ mabs a ^ m) ∧ ∃ (n : ℕ), mabs a ≤ mabs b ^ n

theorem ArchimedeanClass.mk_eq_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} : mk a = mk b ↔ (∃ (m : ℕ), |b| ≤ m • |a|) ∧ ∃ (n : ℕ), |a| ≤ n • |b|

noncomputable def MulArchimedeanClass.out {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (A : MulArchimedeanClass M) : M

Choose a representative element from a given archimedean class.

Equations

• A.out = MulArchimedeanOrder.val (Quotient.out A)

noncomputable def ArchimedeanClass.out {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (A : ArchimedeanClass M) : M

Choose a representative element from a given archimedean class.

Equations

• A.out = ArchimedeanOrder.val (Quotient.out A)

@[simp]

theorem MulArchimedeanClass.mk_out {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (A : MulArchimedeanClass M) : mk A.out = A

@[simp]

theorem ArchimedeanClass.mk_out {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (A : ArchimedeanClass M) : mk A.out = A

@[simp]

theorem MulArchimedeanClass.mk_inv {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a : M) : mk a⁻¹ = mk a

@[simp]

theorem ArchimedeanClass.mk_neg {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : M) : mk (-a) = mk a

theorem MulArchimedeanClass.mk_div_comm {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a b : M) : mk (a / b) = mk (b / a)

theorem ArchimedeanClass.mk_sub_comm {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a b : M) : mk (a - b) = mk (b - a)

@[simp]

theorem MulArchimedeanClass.mk_mabs {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a : M) : mk (mabs a) = mk a

@[simp]

theorem ArchimedeanClass.mk_abs {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : M) : mk |a| = mk a

noncomputable instance MulArchimedeanClass.instLinearOrder {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : LinearOrder (MulArchimedeanClass M)

Equations

• MulArchimedeanClass.instLinearOrder = id inferInstance

noncomputable instance ArchimedeanClass.instLinearOrder {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : LinearOrder (ArchimedeanClass M)

Equations

• ArchimedeanClass.instLinearOrder = id inferInstance

theorem MulArchimedeanClass.mk_le_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} : mk a ≤ mk b ↔ ∃ (n : ℕ), mabs b ≤ mabs a ^ n

theorem ArchimedeanClass.mk_le_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} : mk a ≤ mk b ↔ ∃ (n : ℕ), |b| ≤ n • |a|

theorem MulArchimedeanClass.mk_lt_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} : mk a < mk b ↔ ∀ (n : ℕ), mabs b ^ n < mabs a

theorem ArchimedeanClass.mk_lt_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} : mk a < mk b ↔ ∀ (n : ℕ), n • |b| < |a|

noncomputable instance MulArchimedeanClass.instOrderTop {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : OrderTop (MulArchimedeanClass M)

1 is in its own class (see MulArchimedeanClass.mk_eq_top_iff), which is also the largest class.

Equations

• MulArchimedeanClass.instOrderTop = { top := MulArchimedeanClass.mk 1, le_top := ⋯ }

noncomputable instance ArchimedeanClass.instOrderTop {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : OrderTop (ArchimedeanClass M)

0 is in its own class (see ArchimedeanClass.mk_eq_top_iff), which is also the largest class.

Equations

• ArchimedeanClass.instOrderTop = { top := ArchimedeanClass.mk 0, le_top := ⋯ }

@[simp]

theorem MulArchimedeanClass.mk_one (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : mk 1 = ⊤

@[simp]

theorem ArchimedeanClass.mk_zero (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : mk 0 = ⊤

@[simp]

theorem MulArchimedeanClass.mk_eq_top_iff {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} : mk a = ⊤ ↔ a = 1

@[simp]

theorem ArchimedeanClass.mk_eq_top_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} : mk a = ⊤ ↔ a = 0

@[simp]

theorem MulArchimedeanClass.out_top (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : ⊤.out = 1

@[simp]

theorem ArchimedeanClass.out_top (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : ⊤.out = 0

instance MulArchimedeanClass.instNontrivial (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] [Nontrivial M] : Nontrivial (MulArchimedeanClass M)

instance ArchimedeanClass.instNontrivial (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Nontrivial M] : Nontrivial (ArchimedeanClass M)

theorem MulArchimedeanClass.mk_antitoneOn (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : AntitoneOn mk (Set.Ici 1)

theorem ArchimedeanClass.mk_antitoneOn (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : AntitoneOn mk (Set.Ici 0)

theorem MulArchimedeanClass.mk_monotoneOn (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : MonotoneOn mk (Set.Iic 1)

theorem ArchimedeanClass.mk_monotoneOn (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : MonotoneOn mk (Set.Iic 0)

theorem MulArchimedeanClass.min_le_mk_mul {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a b : M) : min (mk a) (mk b) ≤ mk (a * b)

theorem ArchimedeanClass.min_le_mk_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a b : M) : min (mk a) (mk b) ≤ mk (a + b)

theorem MulArchimedeanClass.mk_left_le_mk_mul {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (hab : mk a ≤ mk b) : mk a ≤ mk (a * b)

theorem ArchimedeanClass.mk_left_le_mk_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (hab : mk a ≤ mk b) : mk a ≤ mk (a + b)

theorem MulArchimedeanClass.mk_right_le_mk_mul {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (hba : mk b ≤ mk a) : mk b ≤ mk (a * b)

theorem ArchimedeanClass.mk_right_le_mk_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (hba : mk b ≤ mk a) : mk b ≤ mk (a + b)

theorem MulArchimedeanClass.mk_mul_eq_mk_left {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk a < mk b) : mk (a * b) = mk a

theorem ArchimedeanClass.mk_add_eq_mk_left {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk a < mk b) : mk (a + b) = mk a

theorem MulArchimedeanClass.mk_mul_eq_mk_right {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk b < mk a) : mk (a * b) = mk b

theorem ArchimedeanClass.mk_add_eq_mk_right {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk b < mk a) : mk (a + b) = mk b

theorem MulArchimedeanClass.mk_prod {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {ι : Type u_2} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M} : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hnonempty))

The product over a set of an elements in distinct classes is in the lowest class.

theorem ArchimedeanClass.mk_sum {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {ι : Type u_2} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M} : StrictMonoOn (mk ∘ a) ↑s → mk (∑ i ∈ s, a i) = mk (a (s.min' hnonempty))

The sum over a set of an elements in distinct classes is in the lowest class.

theorem MulArchimedeanClass.lt_of_mk_lt_mk_of_one_le {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk a < mk b) (hpos : 1 ≤ a) : b < a

theorem ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk a < mk b) (hpos : 0 ≤ a) : b < a

theorem MulArchimedeanClass.lt_of_mk_lt_mk_of_le_one {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk a < mk b) (hneg : a ≤ 1) : a < b

theorem ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk a < mk b) (hneg : a ≤ 0) : a < b

theorem MulArchimedeanClass.one_lt_of_one_lt_of_mk_lt {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (ha : 1 < a) (hab : mk a < mk (b / a)) : 1 < b

theorem ArchimedeanClass.pos_of_pos_of_mk_lt {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (ha : 0 < a) (hab : mk a < mk (b - a)) : 0 < b

theorem MulArchimedeanClass.mulArchimedean_of_mk_eq_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b) : MulArchimedean M

theorem ArchimedeanClass.archimedean_of_mk_eq_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (h : ∀ (a : M), a ≠ 0 → ∀ (b : M), b ≠ 0 → mk a = mk b) : Archimedean M

theorem MulArchimedeanClass.mk_eq_mk_of_mulArchimedean {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} [MulArchimedean M] (ha : a ≠ 1) (hb : b ≠ 1) : mk a = mk b

theorem ArchimedeanClass.mk_eq_mk_of_archimedean {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} [Archimedean M] (ha : a ≠ 0) (hb : b ≠ 0) : mk a = mk b

noncomputable def MulArchimedeanClass.orderHom {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) : MulArchimedeanClass M →o MulArchimedeanClass N

An OrderMonoidHom can be lifted to an OrderHom over archimedean classes.

Equations

• MulArchimedeanClass.orderHom f = (MulArchimedeanOrder.orderHom f).antisymmetrization

noncomputable def ArchimedeanClass.orderHom {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) : ArchimedeanClass M →o ArchimedeanClass N

An OrderAddMonoidHom can be lifted to an OrderHom over archimedean classes.

Equations

• ArchimedeanClass.orderHom f = (ArchimedeanOrder.orderHom f).antisymmetrization

@[simp]

theorem MulArchimedeanClass.orderHom_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) (a : M) : (orderHom f) (mk a) = mk (f a)

@[simp]

theorem ArchimedeanClass.orderHom_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) (a : M) : (orderHom f) (mk a) = mk (f a)

theorem MulArchimedeanClass.map_mk_eq {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) (h : mk a = mk b) : mk (f a) = mk (f b)

theorem ArchimedeanClass.map_mk_eq {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) (h : mk a = mk b) : mk (f a) = mk (f b)

theorem MulArchimedeanClass.map_mk_le {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) (h : mk a ≤ mk b) : mk (f a) ≤ mk (f b)

theorem ArchimedeanClass.map_mk_le {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) (h : mk a ≤ mk b) : mk (f a) ≤ mk (f b)

theorem MulArchimedeanClass.orderHom_injective {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] {f : M →*o N} (h : Function.Injective ⇑f) : Function.Injective ⇑(orderHom f)

theorem ArchimedeanClass.orderHom_injective {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] {f : M →+o N} (h : Function.Injective ⇑f) : Function.Injective ⇑(orderHom f)

@[simp]

theorem MulArchimedeanClass.orderHom_top {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) : (orderHom f) ⊤ = ⊤

@[simp]

theorem ArchimedeanClass.orderHom_top {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) : (orderHom f) ⊤ = ⊤