Embedding of archimedean groups into reals #
This file provides embedding of any archimedean groups into reals.
Main declarations #
Archimedean.embedReal
defines an injectiveM →+o ℝ
for archimedean groupM
with a positive1
element.1
is preserved by the map.Archimedean.exists_orderAddMonoidHom_real_injective
states there exists an injectiveM →+o ℝ
for any archimedean groupM
without specifying the1
element inM
.
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}
:
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)
:
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)
:
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]
Set of rational numbers that are less than the "number" x / 1
.
Formally, these are numbers p / q
such that p • 1 < q • x
.
Instances For
theorem
Archimedean.mkRat_mem_ratLt
{M : Type u_1}
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
{num : ℤ}
{den : ℕ}
(hden : den ≠ 0)
{x : M}
:
@[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
.
Equations
Instances For
theorem
Archimedean.ratLt_bddAbove
{M : Type u_1}
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
(x : M)
:
theorem
Archimedean.ratLt_nonempty
{M : Type u_1}
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
(x : M)
:
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)
:
theorem
Archimedean.ratLt'_bddAbove
{M : Type u_1}
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
(x : M)
:
theorem
Archimedean.ratLt'_nonempty
{M : Type u_1}
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
(x : M)
:
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)
:
theorem
Archimedean.embedRealFun_zero
(M : Type u_1)
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
:
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)
:
theorem
Archimedean.embedRealFun_strictMono
(M : Type u_1)
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
:
noncomputable def
Archimedean.embedReal
(M : Type u_1)
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
:
The bundled M →+o ℝ
for archimedean M
that preserves 1
.
Equations
- Archimedean.embedReal M = { toFun := Archimedean.embedRealFun, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }
Instances For
theorem
Archimedean.embedReal_apply
{M : Type u_1}
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
(a : M)
:
theorem
Archimedean.embedReal_injective
(M : Type u_1)
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
:
@[simp]
theorem
Archimedean.embedReal_one
{M : Type u_1}
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[One M]
[ZeroLEOneClass M]
[NeZero 1]
[Archimedean M]
:
theorem
Archimedean.exists_orderAddMonoidHom_real_injective
(M : Type u_1)
[AddCommGroup M]
[LinearOrder M]
[IsOrderedAddMonoid M]
[Archimedean M]
:
∃ (f : M →+o ℝ), Function.Injective ⇑f