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.

References

• https://mathoverflow.net/questions/362991/ who-first-characterized-the-real-numbers-as-the-unique-complete-ordered-field

Tags

reals, conditionally complete, ordered field, uniqueness

class ConditionallyCompleteLinearOrderedField (α : Type u_5) extends LinearOrderedField , Sup , Inf , SupSet , InfSet : Type u_5

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

• add : α → α → α
• 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 : α), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : ℤ → α
• intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
• intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 < a → 0 < b → 0 < a * b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
• decidableEq : 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 = compareOfLessAndEq 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 : α), LinearOrderedField.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.ofNat n.succ) a = LinearOrderedField.zpow (Int.ofNat n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.negSucc n) a = (LinearOrderedField.zpow (↑n.succ) a)⁻¹
• nnratCast : ℚ≥0 → α
• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), LinearOrderedField.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def : ∀ (a : ℚ) (x : α), LinearOrderedField.qsmul 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 ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c

  The infimum is the greatest lower bound

• sSup : Set α → α
• sInf : Set α → α
• le_csSup : ∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup s

  a ≤ sSup s for all a ∈ s.

• csSup_le : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → sSup s ≤ a

  sSup s ≤ a for all a ∈ upperBounds s.

• csInf_le : ∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ a

  sInf s ≤ a for all a ∈ s.

• le_csInf : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s

  a ≤ sInf s for all a ∈ lowerBounds s.

• csSup_of_not_bddAbove : ∀ (s : Set α), ¬BddAbove s → sSup s = sSup ∅

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

• csInf_of_not_bddBelow : ∀ (s : Set α), ¬BddBelow s → sInf s = sInf ∅

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

instance ConditionallyCompleteLinearOrderedField.to_archimedean {α : Type u_2} [ConditionallyCompleteLinearOrderedField α] : Archimedean α

Any conditionally complete linearly ordered field is archimedean.

Equations

• ⋯ = ⋯

instance instConditionallyCompleteLinearOrderedFieldReal : ConditionallyCompleteLinearOrderedField ℝ

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) [LinearOrderedField α] [DivisionRing β] (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

• LinearOrderedField.cutMap β a = Rat.cast '' {t : ℚ | ↑t < a}

theorem LinearOrderedField.cutMap_mono {α : Type u_2} (β : Type u_3) [LinearOrderedField α] [DivisionRing β] {a₁ : α} {a₂ : α} (h : a₁ ≤ a₂) : LinearOrderedField.cutMap β a₁ ⊆ LinearOrderedField.cutMap β a₂

@[simp]

theorem LinearOrderedField.mem_cutMap_iff {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [DivisionRing β] {a : α} {b : β} : b ∈ LinearOrderedField.cutMap β a ↔ ∃ (q : ℚ), ↑q < a ∧ ↑q = b

theorem LinearOrderedField.coe_mem_cutMap_iff {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [DivisionRing β] {a : α} {q : ℚ} [CharZero β] : ↑q ∈ LinearOrderedField.cutMap β a ↔ ↑q < a

theorem LinearOrderedField.cutMap_self {α : Type u_2} [LinearOrderedField α] (a : α) : LinearOrderedField.cutMap α a = Set.Iio a ∩ Set.range Rat.cast

theorem LinearOrderedField.cutMap_coe {α : Type u_2} (β : Type u_3) [LinearOrderedField α] [LinearOrderedField β] (q : ℚ) : LinearOrderedField.cutMap β ↑q = Rat.cast '' {r : ℚ | ↑r < ↑q}

theorem LinearOrderedField.cutMap_nonempty {α : Type u_2} (β : Type u_3) [LinearOrderedField α] [LinearOrderedField β] [Archimedean α] (a : α) : (LinearOrderedField.cutMap β a).Nonempty

theorem LinearOrderedField.cutMap_bddAbove {α : Type u_2} (β : Type u_3) [LinearOrderedField α] [LinearOrderedField β] [Archimedean α] (a : α) : BddAbove (LinearOrderedField.cutMap β a)

theorem LinearOrderedField.cutMap_add {α : Type u_2} (β : Type u_3) [LinearOrderedField α] [LinearOrderedField β] [Archimedean α] (a : α) (b : α) : LinearOrderedField.cutMap β (a + b) = LinearOrderedField.cutMap β a + LinearOrderedField.cutMap β 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) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] (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

• LinearOrderedField.inducedMap α β x = sSup (LinearOrderedField.cutMap β x)

theorem LinearOrderedField.inducedMap_mono (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] : Monotone (LinearOrderedField.inducedMap α β)

theorem LinearOrderedField.inducedMap_rat (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] (q : ℚ) : LinearOrderedField.inducedMap α β ↑q = ↑q

@[simp]

theorem LinearOrderedField.inducedMap_zero (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] : LinearOrderedField.inducedMap α β 0 = 0

@[simp]

theorem LinearOrderedField.inducedMap_one (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] : LinearOrderedField.inducedMap α β 1 = 1

theorem LinearOrderedField.inducedMap_nonneg {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] {a : α} (ha : 0 ≤ a) : 0 ≤ LinearOrderedField.inducedMap α β a

theorem LinearOrderedField.coe_lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] {a : α} {q : ℚ} : ↑q < LinearOrderedField.inducedMap α β a ↔ ↑q < a

theorem LinearOrderedField.lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] {a : α} {b : β} : b < LinearOrderedField.inducedMap α β a ↔ ∃ (q : ℚ), b < ↑q ∧ ↑q < a

@[simp]

theorem LinearOrderedField.inducedMap_self {β : Type u_3} [ConditionallyCompleteLinearOrderedField β] (b : β) : LinearOrderedField.inducedMap β β b = b

@[simp]

theorem LinearOrderedField.inducedMap_inducedMap (α : Type u_2) (β : Type u_3) (γ : Type u_4) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [ConditionallyCompleteLinearOrderedField γ] [Archimedean α] (a : α) : LinearOrderedField.inducedMap β γ (LinearOrderedField.inducedMap α β a) = LinearOrderedField.inducedMap α γ a

theorem LinearOrderedField.inducedMap_inv_self (β : Type u_3) (γ : Type u_4) [ConditionallyCompleteLinearOrderedField β] [ConditionallyCompleteLinearOrderedField γ] (b : β) : LinearOrderedField.inducedMap γ β (LinearOrderedField.inducedMap β γ b) = b

theorem LinearOrderedField.inducedMap_add (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] (x : α) (y : α) : LinearOrderedField.inducedMap α β (x + y) = LinearOrderedField.inducedMap α β x + LinearOrderedField.inducedMap α β y

theorem LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] {a : α} (ha : 0 < a) (b : β) (hb : b ∈ LinearOrderedField.cutMap β (a * a)) : b ≤ LinearOrderedField.inducedMap α β a * LinearOrderedField.inducedMap α β a

Preparatory lemma for inducedOrderRingHom.

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

Preparatory lemma for inducedOrderRingHom.

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

inducedMap as an additive homomorphism.

Equations

• LinearOrderedField.inducedAddHom α β = { toFun := LinearOrderedField.inducedMap α β, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem LinearOrderedField.inducedOrderRingHom_toFun (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] : ∀ (a : α), (LinearOrderedField.inducedOrderRingHom α β) a = (LinearOrderedField.inducedAddHom α β) a

def LinearOrderedField.inducedOrderRingHom (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] : α →+*o β

inducedMap as an OrderRingHom.

Equations

• LinearOrderedField.inducedOrderRingHom α β = let __src := (LinearOrderedField.inducedAddHom α β).mkRingHomOfMulSelfOfTwoNeZero ⋯ ⋯ ⋯; { toRingHom := __src, monotone' := ⋯ }

def LinearOrderedField.inducedOrderRingIso (β : Type u_3) (γ : Type u_4) [ConditionallyCompleteLinearOrderedField β] [ConditionallyCompleteLinearOrderedField γ] : β ≃+*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.

@[simp]

theorem LinearOrderedField.coe_inducedOrderRingIso (β : Type u_3) (γ : Type u_4) [ConditionallyCompleteLinearOrderedField β] [ConditionallyCompleteLinearOrderedField γ] : ⇑(LinearOrderedField.inducedOrderRingIso β γ) = LinearOrderedField.inducedMap β γ

@[simp]

theorem LinearOrderedField.inducedOrderRingIso_symm (β : Type u_3) (γ : Type u_4) [ConditionallyCompleteLinearOrderedField β] [ConditionallyCompleteLinearOrderedField γ] : (LinearOrderedField.inducedOrderRingIso β γ).symm = LinearOrderedField.inducedOrderRingIso γ β

@[simp]

theorem LinearOrderedField.inducedOrderRingIso_self (β : Type u_3) [ConditionallyCompleteLinearOrderedField β] : LinearOrderedField.inducedOrderRingIso β β = OrderRingIso.refl β

instance LinearOrderedField.uniqueOrderRingHom (α : Type u_2) (β : Type u_3) [LinearOrderedField α] [ConditionallyCompleteLinearOrderedField β] [Archimedean α] : Unique (α →+*o β)

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

Equations

• LinearOrderedField.uniqueOrderRingHom α β = uniqueOfSubsingleton (LinearOrderedField.inducedOrderRingHom α β)

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

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

Equations

• LinearOrderedField.uniqueOrderRingIso β γ = uniqueOfSubsingleton (LinearOrderedField.inducedOrderRingIso β γ)

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

instance Real.RingHom.unique : Unique (ℝ →+* ℝ)

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

Equations

• Real.RingHom.unique = { default := RingHom.id ℝ, uniq := Real.RingHom.unique.proof_1 }