Abstract theory of Hausdorff completions of uniform spaces #
This file characterizes Hausdorff completions of a uniform space α as complete Hausdorff spaces equipped with a map from α which has dense image and induce the original uniform structure on α. Assuming these properties we "extend" uniformly continuous maps from α to complete Hausdorff spaces to the completions of α. This is the universal property expected from a completion. It is then used to extend uniformly continuous maps from α to α' to maps between completions of α and α'.
This file does not construct any such completion, it only study consequences of their existence.
The first advantage is that formal properties are clearly highlighted without interference from
construction details. The second advantage is that this framework can then be used to compare
different completion constructions. See
topology/uniform_space/compare_reals for an example.
Of course the comparison comes from the universal property as usual.
A general explicit construction of completions is done in
to a functor from uniform spaces to complete Hausdorff uniform spaces that is left adjoint to the
uniform_space/UniformSpace for the category packaging.
Implementation notes #
A tiny technical advantage of using a characteristic predicate such as the properties listed in
abstract_completion instead of stating the universal property is that the universal property
derived from the predicate is more universe polymorphic.
We don't know any traditional text discussing this. Real world mathematics simply silently identify the results of any two constructions that lead to something one could reasonnably call a completion.
uniform spaces, completion, universal property
- space : Type ?
- coe : α → self.space
- uniform_struct : uniform_space self.space
- complete : complete_space self.space
- separation : separated_space self.space
- uniform_inducing : uniform_inducing self.coe
- dense : dense_range self.coe
A completion of
α is the data of a complete separated uniform space (from the same universe)
and a map from
α with dense range and inducing the original uniform structure on
The bijection between two completions of the same uniform space.
Products of completions
Extend two variable map to completions.
Lift two variable maps to completions.