Documentation

Mathlib.Algebra.Order.CompleteField

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 #

Main results #

References #

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.

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) [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
    Instances For
      theorem LinearOrderedField.cutMap_mono {α : Type u_2} (β : Type u_3) [LinearOrderedField α] [DivisionRing β] {a₁ : α} {a₂ : α} (h : a₁ 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 β] :
      theorem LinearOrderedField.cutMap_coe {α : Type u_2} (β : Type u_3) [LinearOrderedField α] [LinearOrderedField β] (q : ) :
      LinearOrderedField.cutMap β q = Rat.cast '' {r : | r < q}

      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
      Instances For
        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

        inducedMap as an additive homomorphism.

        Equations
        Instances For

          inducedMap as an OrderRingHom.

          Equations
          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.

              Equations

              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} [OrderedRing R] [LinearOrderedRing S] (hR : ∀ (r : R), 0 r∃ (s : R), s ^ 2 = r) (f : R →+* S) :

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

              Equations