Hausdorff completions of uniform spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Extend a uniformly continuous function
α → β to a function
Cauchy α → β. Outputs junk when
f is not uniformly continuous.
Hausdorff completion of
The Haudorff completion as an abstract completion.
The uniform bijection between a complete space and its uniform completion.
"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
The isomorphism between the completion of a uniform space and the completion of its separation quotient.
Extend a two variable map to the Hausdorff completions.
Lift a two variable map to the Hausdorff completions.