Comparison of Cauchy reals and Bourbaki reals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 uniform_space 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 metric_space/cau_seq_filter also relates the notions of Cauchy sequences in metric spaces and Cauchy filters in general uniform spaces, and metric_space/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/uniform_space/abstract_completion which provides an abstract caracterization 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

Tags #

real numbers, completion, uniform spaces

source

theorem rat.uniform_space_eq :

absolute_value.abs.uniform_space = pseudo_metric_space.to_uniform_space

The metric space uniform structure on ℚ (which presupposes the existence of real numbers) agrees with the one coming directly from (abs : ℚ → ℚ).

source

def rational_cau_seq_pkg :

abstract_completion ℚ

Cauchy reals packaged as a completion of ℚ using the absolute value route.

Equations

rational_cau_seq_pkg = {space := ℝ, coe := coe coe_to_lift, uniform_struct := pseudo_metric_space.to_uniform_space real.pseudo_metric_space, complete := real.complete_space, separation := _, uniform_inducing := rational_cau_seq_pkg._proof_1, dense := rational_cau_seq_pkg._proof_2}

source

@[protected, instance]

def compare_reals.Q.comm_ring :

comm_ring compare_reals.Q

source

def compare_reals.Q :

Type

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.uniform_space_eq that they are equal, but they are not definitionaly equal, so it would confuse the type class system (and probably also human readers).

Equations