Embedding of archimedean groups into reals

This file provides embedding of any archimedean groups into reals.

Main declarations

• Archimedean.embedReal defines an injective M →+o ℝ for archimedean group M with a positive 1 element. 1 is preserved by the map.
• Archimedean.exists_orderAddMonoidHom_real_injective states there exists an injective M →+o ℝ for any archimedean group M without specifying the 1 element in M.

theorem mul_smul_one_lt_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] {num : ℤ} {n den : ℕ} (hn : 0 < n) {x : M} : (num * ↑n) • 1 < (↑n * ↑den) • x ↔ num • 1 < den • x

theorem num_smul_one_lt_den_smul_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] {u v : ℚ} {x y : M} (hu : u.num • 1 < u.den • x) (hv : v.num • 1 < v.den • y) : (u + v).num • 1 < (u + v).den • (x + y)

For u v : ℚ and x y : M, one can informally write u < x → v < y → u + v < x + y. We formalize this using smul.

theorem num_le_nat_mul_den {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] {num : ℤ} {den : ℕ} {x : M} (h : num • 1 ≤ den • x) {n : ℤ} (hn : x ≤ n • 1) : num ≤ n * ↑den

Given x from M, one can informally write that, by transitivity, num / den ≤ x → x ≤ n → num / den ≤ n for den : ℕ and num n : ℕ. To avoid writing division for integer num and den, we express this in terms of multiplication.

@[reducible, inline]

abbrev Archimedean.ratLt {M : Type u_1} [AddCommGroup M] [LinearOrder M] [One M] (x : M) : Set ℚ

Set of rational numbers that are less than the "number" x / 1. Formally, these are numbers p / q such that p • 1 < q • x.

theorem Archimedean.mkRat_mem_ratLt {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] {num : ℤ} {den : ℕ} (hden : den ≠ 0) {x : M} : mkRat num den ∈ ratLt x ↔ num • 1 < den • x

@[reducible, inline]

abbrev Archimedean.ratLt' {M : Type u_1} [AddCommGroup M] [LinearOrder M] [One M] (x : M) : Set ℝ

ratLt as a set of real numbers.

@[reducible, inline]

noncomputable abbrev Archimedean.embedRealFun {M : Type u_1} [AddCommGroup M] [LinearOrder M] [One M] (x : M) : ℝ

Mapping M to ℝ, defined as the supremum of ratLt' x.

theorem Archimedean.ratLt_bddAbove {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M) : BddAbove (ratLt x)

theorem Archimedean.ratLt_nonempty {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M) : (ratLt x).Nonempty

theorem Archimedean.ratLt_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x y : M) : ratLt (x + y) = ratLt x + ratLt y

theorem Archimedean.ratLt'_bddAbove {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M) : BddAbove (ratLt' x)

theorem Archimedean.ratLt'_nonempty {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M) : (ratLt' x).Nonempty

theorem Archimedean.ratLt'_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x y : M) : ratLt' (x + y) = ratLt' x + ratLt' y

theorem Archimedean.embedRealFun_zero (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] : embedRealFun 0 = 0

theorem Archimedean.embedRealFun_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x y : M) : embedRealFun (x + y) = embedRealFun x + embedRealFun y

theorem Archimedean.embedRealFun_strictMono (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] : StrictMono embedRealFun

noncomputable def Archimedean.embedReal (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] : M →+o ℝ

The bundled M →+o ℝ for archimedean M that preserves 1.

theorem Archimedean.embedReal_apply {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (a : M) : (embedReal M) a = embedRealFun a

theorem Archimedean.embedReal_injective (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] : Function.Injective ⇑(embedReal M)

@[simp]

theorem Archimedean.embedReal_one {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] [Archimedean M] : (embedReal M) 1 = 1

theorem Archimedean.exists_orderAddMonoidHom_real_injective (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Archimedean M] : ∃ (f : M →+o ℝ), Function.Injective ⇑f