doc-next-gen

Mathlib.Topology.UniformSpace.CompareReals

Module docstring

{"# Comparison of Cauchy reals and Bourbaki reals

In Data.Real.Basic real numbers are defined using the so called Cauchy construction (although it is due to Georg Cantor). More precisely, this construction applies to commutative rings equipped with an absolute value with values in a linear ordered field.

On the other hand, in the UniformSpace folder, we construct completions of general uniform spaces, which allows to construct the Bourbaki real numbers. In this file we build uniformly continuous bijections from Cauchy reals to Bourbaki reals and back. This is a cross sanity check of both constructions. Of course those two constructions are variations on the completion idea, simply with different level of generality. Comparing with Dedekind cuts or quasi-morphisms would be of a completely different nature.

Note that MetricSpace/cau_seq_filter also relates the notions of Cauchy sequences in metric spaces and Cauchy filters in general uniform spaces, and MetricSpace/Completion makes sure the completion (as a uniform space) of a metric space is a metric space.

Historical note: mathlib used to define real numbers in an intermediate way, using completion of uniform spaces but extending multiplication in an ad-hoc way.

TODO: * Upgrade this isomorphism to a topological ring isomorphism. * Do the same comparison for p-adic numbers

Implementation notes

The heavy work is done in Topology/UniformSpace/AbstractCompletion which provides an abstract characterization of completions of uniform spaces, and isomorphisms between them. The only work left here is to prove the uniform space structure coming from the absolute value on ℚ (with values in ℚ, not referring to ℝ) coincides with the one coming from the metric space structure (which of course does use ℝ).

References

  • [N. Bourbaki, Topologie générale][bourbaki1966]

Tags

real numbers, completion, uniform spaces "}

Rat.uniformSpace_eq theorem
: (AbsoluteValue.abs : AbsoluteValue ℚ ℚ).uniformSpace = PseudoMetricSpace.toUniformSpace
Full source 
/-- The metric space uniform structure on ℚ (which presupposes the existence
of real numbers) agrees with the one coming directly from (abs : ℚ → ℚ). -/
theorem Rat.uniformSpace_eq :
    (AbsoluteValue.abs : AbsoluteValue ℚ ℚ).uniformSpace = PseudoMetricSpace.toUniformSpace := by
  ext s
  rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]
  simp only [Rat.dist_eq, AbsoluteValue.abs_apply, ← Rat.cast_sub, ← Rat.cast_abs, Rat.cast_lt,
    abs_sub_comm]
Equality of Uniform Structures on Rational Numbers: Absolute Value vs Metric Space
Informal description
The uniform space structure on the rational numbers $\mathbb{Q}$ induced by the standard absolute value function $|\cdot| : \mathbb{Q} \to \mathbb{Q}$ coincides with the uniform space structure derived from the metric space structure on $\mathbb{Q}$ (where the metric is given by $d(x,y) = |x - y|$).
rationalCauSeqPkg definition
: @AbstractCompletion ℚ <| (@AbsoluteValue.abs ℚ _).uniformSpace
Full source 
/-- Cauchy reals packaged as a completion of ℚ using the absolute value route. -/
def rationalCauSeqPkg : @AbstractCompletion ℚ <| (@AbsoluteValue.abs ℚ _).uniformSpace :=
  @AbstractCompletion.mk
    (space := ℝ)
    (coe := ((↑) : ℚ → ℝ))
    (uniformStruct := by infer_instance)
    (complete := by infer_instance)
    (separation := by infer_instance)
    (isUniformInducing := by
      rw [Rat.uniformSpace_eq]
      exact Rat.isUniformEmbedding_coe_real.isUniformInducing)
    (dense := Rat.isDenseEmbedding_coe_real.dense)
Completion of rationals via absolute value yielding real numbers
Informal description
The structure `rationalCauSeqPkg` represents the completion of the rational numbers ℚ using the uniform space structure induced by the standard absolute value on ℚ. This completion yields the real numbers ℝ, with the canonical embedding of ℚ into ℝ. The completion is equipped with a uniform structure, is complete and Hausdorff, and the embedding of ℚ into ℝ is uniformly continuous and has dense image.
CompareReals.Q definition
Full source 
/-- Type wrapper around ℚ to make sure the absolute value uniform space instance is picked up
instead of the metric space one. We proved in `Rat.uniformSpace_eq` that they are equal,
but they are not definitionaly equal, so it would confuse the type class system (and probably
also human readers). -/
def Q :=
  ℚ deriving CommRing, Inhabited
Rational numbers with absolute value uniform structure
Informal description
The type `Q` is a wrapper around the rational numbers `ℚ` used to ensure the uniform space structure derived from the absolute value on `ℚ` is used, rather than the metric space structure. While these two structures are proven to be equal (in `Rat.uniformSpace_eq`), they are not definitionally equal, which could cause confusion in type class resolution and human interpretation.
CompareReals.uniformSpace instance
: UniformSpace Q
Full source 
instance uniformSpace : UniformSpace Q :=
  (@AbsoluteValue.abs ℚ _).uniformSpace
Uniform Space Structure on Rational Numbers via Absolute Value
Informal description
The rational numbers $\mathbb{Q}$ are equipped with a uniform space structure induced by the standard absolute value function.
CompareReals.Bourbakiℝ definition
: Type
Full source 
/-- Real numbers constructed as in Bourbaki. -/
def Bourbakiℝ : Type :=
  Completion Q deriving Inhabited
Bourbaki real numbers
Informal description
The type representing the real numbers constructed via the Bourbaki completion of the rational numbers equipped with the uniform space structure induced by the absolute value.
CompareReals.Bourbaki.uniformSpace instance
: UniformSpace Bourbakiℝ
Full source 
instance Bourbaki.uniformSpace : UniformSpace Bourbakiℝ :=
  Completion.uniformSpace Q
Uniform Space Structure on Bourbaki Reals
Informal description
The Bourbaki real numbers $\text{Bourbaki}\mathbb{R}$ are equipped with a uniform space structure, inherited from the completion of the rational numbers with their absolute value-induced uniform structure.
CompareReals.bourbakiPkg definition
: AbstractCompletion Q
Full source 
/-- Bourbaki reals packaged as a completion of Q using the general theory. -/
def bourbakiPkg : AbstractCompletion Q :=
  Completion.cPkg
Bourbaki real numbers as completion of rationals
Informal description
The Bourbaki real numbers are constructed as the completion of the rational numbers $\mathbb{Q}$ equipped with the uniform space structure induced by the standard absolute value, using the general theory of uniform space completions.
CompareReals.compareEquiv definition
: Bourbakiℝ ≃ᵤ ℝ
Full source 
/-- The uniform bijection between Bourbaki and Cauchy reals. -/
noncomputable def compareEquiv : BourbakiℝBourbakiℝ ≃ᵤ ℝ :=
  bourbakiPkg.compareEquiv rationalCauSeqPkg
Uniform equivalence between Bourbaki and Cauchy reals
Informal description
The uniform equivalence between the Bourbaki real numbers (constructed via uniform space completion of the rationals) and the Cauchy real numbers (constructed via Cauchy sequences of rationals). This bijection is uniformly continuous in both directions.