# Conditionally complete linear ordered fields #

This file shows that the reals are unique, or, more formally, given a type satisfying the common axioms of the reals (field, conditionally complete, linearly ordered) that there is an isomorphism preserving these properties to the reals. This is LinearOrderedField.inducedOrderRingIso for ℚ. Moreover this isomorphism is unique.

We introduce definitions of conditionally complete linear ordered fields, and show all such are archimedean. We also construct the natural map from a LinearOrderedField to such a field.

## Main definitions #

• ConditionallyCompleteLinearOrderedField: A field satisfying the standard axiomatization of the real numbers, being a Dedekind complete and linear ordered field.
• LinearOrderedField.inducedMap: A (unique) map from any archimedean linear ordered field to a conditionally complete linear ordered field. Various bundlings are available.

## Main results #

• LinearOrderedField.uniqueOrderRingHom : Uniqueness of OrderRingHoms from an archimedean linear ordered field to a conditionally complete linear ordered field.
• LinearOrderedField.uniqueOrderRingIso : Uniqueness of OrderRingIsos between two conditionally complete linearly ordered fields.

## Tags #

reals, conditionally complete, ordered field, uniqueness

class ConditionallyCompleteLinearOrderedField (α : Type u_5) extends , , , , :
Type u_5

A field which is both linearly ordered and conditionally complete with respect to the order. This axiomatizes the reals.

• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• exists_pair_ne : ∃ (x : α) (y : α), x y
• zero_le_one : 0 1
• mul_pos : ∀ (a b : α), 0 < a0 < b0 < a * b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun (x x_1 : α) => x x_1
• decidableEq :
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α),
• zpow_succ' : ∀ (n : ) (a : α), LinearOrderedField.zpow (Int.ofNat n.succ) a =
• zpow_neg' : ∀ (n : ) (a : α), = (LinearOrderedField.zpow (n.succ) a)⁻¹
• nnratCast : ℚ≥0α
• ratCast : α
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den
• nnqsmul : ℚ≥0αα
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a
• ratCast_def : ∀ (q : ), q = q.num / q.den
• qsmul : αα
• qsmul_def : ∀ (a : ) (x : α), = a * x
• sup : ααα
• le_sup_left : ∀ (a b : α), a a b

The supremum is an upper bound on the first argument

• le_sup_right : ∀ (a b : α), b a b

The supremum is an upper bound on the second argument

• sup_le : ∀ (a b c : α), a cb ca b c

The supremum is the least upper bound

• inf : ααα
• inf_le_left : ∀ (a b : α), a b a

The infimum is a lower bound on the first argument

• inf_le_right : ∀ (a b : α), a b b

The infimum is a lower bound on the second argument

• le_inf : ∀ (a b c : α), a ba ca b c

The infimum is the greatest lower bound

• sSup : Set αα
• sInf : Set αα
• le_csSup : ∀ (s : Set α) (a : α), a sa sSup s

a ≤ sSup s for all a ∈ s.

• csSup_le : ∀ (s : Set α) (a : α), s.Nonemptya sSup s a

sSup s ≤ a for all a ∈ upperBounds s.

• csInf_le : ∀ (s : Set α) (a : α), a ssInf s a

sInf s ≤ a for all a ∈ s.

• le_csInf : ∀ (s : Set α) (a : α), s.Nonemptya a sInf s

a ≤ sInf s for all a ∈ lowerBounds s.

• csSup_of_not_bddAbove : ∀ (s : Set α), sSup s =

If a set is not bounded above, its supremum is by convention sSup ∅.

• csInf_of_not_bddBelow : ∀ (s : Set α), sInf s =

If a set is not bounded below, its infimum is by convention sInf ∅.

Instances
@[instance 100]

Any conditionally complete linearly ordered field is archimedean.

Equations
• =

The reals are a conditionally complete linearly ordered field.

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

### Rational cut map #

The idea is that a conditionally complete linear ordered field is fully characterized by its copy of the rationals. Hence we define LinearOrderedField.cutMap β : α → Set β which sends a : α to the "rationals in β" that are less than a.

def LinearOrderedField.cutMap {α : Type u_2} (β : Type u_3) [] (a : α) :
Set β

The lower cut of rationals inside a linear ordered field that are less than a given element of another linear ordered field.

Equations
• = Rat.cast '' {t : | t < a}
Instances For
theorem LinearOrderedField.cutMap_mono {α : Type u_2} (β : Type u_3) [] {a₁ : α} {a₂ : α} (h : a₁ a₂) :
@[simp]
theorem LinearOrderedField.mem_cutMap_iff {α : Type u_2} {β : Type u_3} [] {a : α} {b : β} :
∃ (q : ), q < a q = b
theorem LinearOrderedField.coe_mem_cutMap_iff {α : Type u_2} {β : Type u_3} [] {a : α} {q : } [] :
q < a
theorem LinearOrderedField.cutMap_self {α : Type u_2} (a : α) :
= Set.range Rat.cast
theorem LinearOrderedField.cutMap_coe {α : Type u_2} (β : Type u_3) (q : ) :
= Rat.cast '' {r : | r < q}
theorem LinearOrderedField.cutMap_nonempty {α : Type u_2} (β : Type u_3) [] (a : α) :
.Nonempty
theorem LinearOrderedField.cutMap_bddAbove {α : Type u_2} (β : Type u_3) [] (a : α) :
theorem LinearOrderedField.cutMap_add {α : Type u_2} (β : Type u_3) [] (a : α) (b : α) :

### Induced map #

LinearOrderedField.cutMap spits out a Set β. To get something in β, we now take the supremum.

def LinearOrderedField.inducedMap (α : Type u_2) (β : Type u_3) (x : α) :
β

The induced order preserving function from a linear ordered field to a conditionally complete linear ordered field, defined by taking the Sup in the codomain of all the rationals less than the input.

Equations
Instances For
theorem LinearOrderedField.inducedMap_mono (α : Type u_2) (β : Type u_3) [] :
theorem LinearOrderedField.inducedMap_rat (α : Type u_2) (β : Type u_3) [] (q : ) :
= q
@[simp]
theorem LinearOrderedField.inducedMap_zero (α : Type u_2) (β : Type u_3) [] :
@[simp]
theorem LinearOrderedField.inducedMap_one (α : Type u_2) (β : Type u_3) [] :
theorem LinearOrderedField.inducedMap_nonneg {α : Type u_2} {β : Type u_3} [] {a : α} (ha : 0 a) :
theorem LinearOrderedField.coe_lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [] {a : α} {q : } :
q < q < a
theorem LinearOrderedField.lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [] {a : α} {b : β} :
∃ (q : ), b < q q < a
@[simp]
theorem LinearOrderedField.inducedMap_self {β : Type u_3} (b : β) :
@[simp]
theorem LinearOrderedField.inducedMap_inducedMap (α : Type u_2) (β : Type u_3) (γ : Type u_4) [] (a : α) :
theorem LinearOrderedField.inducedMap_inv_self (β : Type u_3) (γ : Type u_4) (b : β) :
theorem LinearOrderedField.inducedMap_add (α : Type u_2) (β : Type u_3) [] (x : α) (y : α) :
theorem LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap {α : Type u_2} {β : Type u_3} [] {a : α} (ha : 0 < a) (b : β) (hb : b LinearOrderedField.cutMap β (a * a)) :
b

Preparatory lemma for inducedOrderRingHom.

theorem LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self {α : Type u_2} {β : Type u_3} [] {a : α} (ha : 0 < a) (b : β) (hba : b < ) :
cLinearOrderedField.cutMap β (a * a), b < c

Preparatory lemma for inducedOrderRingHom.

def LinearOrderedField.inducedAddHom (α : Type u_2) (β : Type u_3) [] :
α →+ β

inducedMap as an additive homomorphism.

Equations
• = { toFun := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem LinearOrderedField.inducedOrderRingHom_toFun (α : Type u_2) (β : Type u_3) [] :
∀ (a : α),
def LinearOrderedField.inducedOrderRingHom (α : Type u_2) (β : Type u_3) [] :
α →+*o β

inducedMap as an OrderRingHom.

Equations
• = let __src := .mkRingHomOfMulSelfOfTwoNeZero ; { toRingHom := __src, monotone' := }
Instances For
def LinearOrderedField.inducedOrderRingIso (β : Type u_3) (γ : Type u_4) :
β ≃+*o γ

The isomorphism of ordered rings between two conditionally complete linearly ordered fields.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearOrderedField.coe_inducedOrderRingIso (β : Type u_3) (γ : Type u_4) :
@[simp]
theorem LinearOrderedField.inducedOrderRingIso_symm (β : Type u_3) (γ : Type u_4) :
@[simp]
instance LinearOrderedField.uniqueOrderRingHom (α : Type u_2) (β : Type u_3) [] :
Unique (α →+*o β)

There is a unique ordered ring homomorphism from an archimedean linear ordered field to a conditionally complete linear ordered field.

Equations
instance LinearOrderedField.uniqueOrderRingIso (β : Type u_3) (γ : Type u_4) :
Unique (β ≃+*o γ)

There is a unique ordered ring isomorphism between two conditionally complete linear ordered fields.

Equations
theorem ringHom_monotone {R : Type u_5} {S : Type u_6} [] (hR : ∀ (r : R), 0 r∃ (s : R), s ^ 2 = r) (f : R →+* S) :

There exists no nontrivial ring homomorphism ℝ →+* ℝ.

Equations