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 ConditionallyCompleteLinearOrderedField.inducedOrderRingIso. Moreover this isomorphism is unique.

We show all conditionally complete linear ordered fields are archimedean. We also construct the natural map from a linearly ordered field to such a field.

Main definitions

• ConditionallyCompleteLinearOrderedField.inducedMap: A (unique) map from any archimedean linear ordered field to a conditionally complete linear ordered field. Various bundlings are available.

Main results

• ConditionallyCompleteLinearOrderedField.uniqueOrderRingHom : Uniqueness of OrderRingHoms from an archimedean linear ordered field to a conditionally complete linear ordered field.
• ConditionallyCompleteLinearOrderedField.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

theorem ConditionallyCompleteLinearOrderedField.to_archimedean {α : Type u_1} [Field α] [ConditionallyCompleteLinearOrder α] [IsStrictOrderedRing α] : Archimedean α

Any conditionally complete linearly ordered field is archimedean.

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_1} (β : Type u_2) [Field α] [LinearOrder α] [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_1} (β : Type u_2) [Field α] [LinearOrder α] [DivisionRing β] {a₁ a₂ : α} (h : a₁ ≤ a₂) : cutMap β a₁ ⊆ cutMap β a₂

@[simp]

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

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

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

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

theorem LinearOrderedField.cutMap_nonempty {α : Type u_1} (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [Archimedean α] (a : α) : (cutMap β a).Nonempty

theorem LinearOrderedField.cutMap_bddAbove {α : Type u_1} (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a : α) : BddAbove (cutMap β a)

theorem LinearOrderedField.cutMap_add {α : Type u_1} (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b

Induced map

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

def ConditionallyCompleteLinearOrderedField.inducedMap (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [Field β] [ConditionallyCompleteLinearOrder β] (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

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

theorem ConditionallyCompleteLinearOrderedField.inducedMap_mono (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : Monotone (inducedMap α β)

theorem ConditionallyCompleteLinearOrderedField.inducedMap_rat (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (q : ℚ) : inducedMap α β ↑q = ↑q

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_zero (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : inducedMap α β 0 = 0

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_one (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : inducedMap α β 1 = 1

theorem ConditionallyCompleteLinearOrderedField.inducedMap_nonneg {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} (ha : 0 ≤ a) : 0 ≤ inducedMap α β a

theorem ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {q : ℚ} : ↑q < inducedMap α β a ↔ ↑q < a

theorem ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff {α : Type u_1} {β : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {b : β} : b < inducedMap α β a ↔ ∃ (q : ℚ), b < ↑q ∧ ↑q < a

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_self {β : Type u_2} [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] (b : β) : inducedMap β β b = b

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap (α : Type u_1) (β : Type u_2) (γ : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] [Archimedean α] (a : α) : inducedMap β γ (inducedMap α β a) = inducedMap α γ a

theorem ConditionallyCompleteLinearOrderedField.inducedMap_inv_self (β : Type u_2) (γ : Type u_3) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] (b : β) : inducedMap γ β (inducedMap β γ b) = b

theorem ConditionallyCompleteLinearOrderedField.inducedMap_add (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (x y : α) : inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y

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

Preparatory lemma for inducedOrderRingHom.

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

Preparatory lemma for inducedOrderRingHom.

def ConditionallyCompleteLinearOrderedField.inducedAddHom (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : α →+ β

inducedMap as an additive homomorphism.

Equations

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

def ConditionallyCompleteLinearOrderedField.inducedOrderRingHom (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : α →+*o β

inducedMap as an OrderRingHom.

Equations

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

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedOrderRingHom_toFun (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a✝ : α) : (inducedOrderRingHom α β) a✝ = (inducedAddHom α β) a✝

def ConditionallyCompleteLinearOrderedField.inducedOrderRingIso (β : Type u_2) (γ : Type u_3) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : β ≃+*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 ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso (β : Type u_2) (γ : Type u_3) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : ⇑(inducedOrderRingIso β γ) = inducedMap β γ

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm (β : Type u_2) (γ : Type u_3) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : (inducedOrderRingIso β γ).symm = inducedOrderRingIso γ β

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self (β : Type u_2) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] : inducedOrderRingIso β β = OrderRingIso.refl β

@[instance_reducible]

def ConditionallyCompleteLinearOrderedField.uniqueOrderRingHom (α : Type u_1) (β : Type u_2) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : Unique (α →+*o β)

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

Equations

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

@[instance_reducible]

def ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso (β : Type u_2) (γ : Type u_3) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : Unique (β ≃+*o γ)

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

Equations

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