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 ofOrderRingHom
s from an archimedean linear ordered field to a conditionally complete linear ordered field.LinearOrderedField.uniqueOrderRingIso
: Uniqueness ofOrderRingIso
s 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
A field which is both linearly ordered and conditionally complete with respect to the order. This axiomatizes the reals.
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- 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 : α → α → α
- 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
- 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
- exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
- zero_le_one : 0 ≤ 1
- min : α → α → α
- max : α → α → α
- compare : α → α → Ordering
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableEq : DecidableEq α
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
- inv : α → α
- div : α → α → α
- 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 : ℚ → α
- nnqsmul : ℚ≥0 → α → α
- nnqsmul_def : ∀ (q : ℚ≥0) (a : α), LinearOrderedField.nnqsmul q a = ↑q * a
- qsmul : ℚ → α → α
- qsmul_def : ∀ (a : ℚ) (x : α), LinearOrderedField.qsmul a x = ↑a * x
- sup : α → α → α
The supremum is an upper bound on the first argument
The supremum is an upper bound on the second argument
The supremum is the least upper bound
- inf : α → α → α
The infimum is a lower bound on the first argument
The infimum is a lower bound on the second argument
The infimum is the greatest lower bound
- sSup : Set α → α
- sInf : Set α → α
a ≤ sSup s
for alla ∈ s
.- csSup_le : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → sSup s ≤ a
sSup s ≤ a
for alla ∈ upperBounds s
. sInf s ≤ a
for alla ∈ s
.- le_csInf : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s
a ≤ sInf s
for alla ∈ lowerBounds s
. If a set is not bounded above, its supremum is by convention
sSup ∅
.If a set is not bounded below, its infimum is by convention
sInf ∅
.
Instances
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
.
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}
Instances For
Induced map #
LinearOrderedField.cutMap
spits out a Set β
. To get something in β
, we now take the supremum.
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)
Instances For
Preparatory lemma for inducedOrderRingHom
.
Preparatory lemma for inducedOrderRingHom
.
inducedMap
as an additive homomorphism.
Equations
- LinearOrderedField.inducedAddHom α β = { toFun := LinearOrderedField.inducedMap α β, map_zero' := ⋯, map_add' := ⋯ }
Instances For
inducedMap
as an OrderRingHom
.
Equations
- LinearOrderedField.inducedOrderRingHom α β = { toRingHom := (LinearOrderedField.inducedAddHom α β).mkRingHomOfMulSelfOfTwoNeZero ⋯ ⋯ ⋯, monotone' := ⋯ }
Instances For
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
There is a unique ordered ring homomorphism from an archimedean linear ordered field to a conditionally complete linear ordered field.
There is a unique ordered ring isomorphism between two conditionally complete linear ordered fields.
There exists no nontrivial ring homomorphism ℝ →+* ℝ
.
Equations
- Real.RingHom.unique = { default := RingHom.id ℝ, uniq := Real.RingHom.unique.proof_1 }