Hausdorff completions of uniform spaces #
The goal is to construct a left-adjoint to the inclusion of complete Hausdorff uniform spaces
into all uniform spaces. Any uniform space
α gets a completion
completion α and a morphism
(ie. uniformly continuous map)
coe : α → completion α which solves the universal
mapping problem of factorizing morphisms from
α to any complete Hausdorff uniform space
It means any uniformly continuous
f : α → β gives rise to a unique morphism
completion.extension f : completion α → β such that
f = completion.extension f ∘ coe.
completion.extension f is defined for all maps from
β but it has the desired
properties only if
f is uniformly continuous.
coe is not injective if
α is not Hausdorff. But its image is always
dense. The adjoint functor acting on morphisms is then constructed by the usual abstract nonsense.
For every uniform spaces
β, it turns
f : α → β into a morphism
completion.map f : completion α → completion β
coe ∘ f = (completion.map f) ∘ coe
f is uniformly continuous. This construction is compatible with composition.
In this file we introduce the following concepts:
Cauchy αthe uniform completion of the uniform space
α(using Cauchy filters). These are not minimal filters.
This formalization is mostly based on N. Bourbaki: General Topology I. M. James: Topologies and Uniformities From a slightly different perspective in order to reuse material in topology.uniform_space.basic.
Space of Cauchy filters
This is essentially the completion of a uniform space. The embeddings are the neighbourhood filters. This space is not minimal, the separated uniform space (i.e. quotiented on the intersection of all entourages) is necessary for this.
"Extension" to the completion. It is defined for any map
returns an arbitrary constant value if
f is not uniformly continuous
Completion functor acting on morphisms