# Documentation

Mathlib.Topology.UniformSpace.Completion

# 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) (↑) : α → 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 ∘ (↑). Actually Completion.extension f is defined for all maps from α to β but it has the desired properties only if f is uniformly continuous.

Beware that (↑) 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 α and β, it turns f : α → β into a morphism Completion.map f : Completion α → Completion β such that (↑) ∘ f = (Completion.map f) ∘ (↑) provided f is uniformly continuous. This construction is compatible with composition.

In this file we introduce the following concepts:

• CauchyFilter α the uniform completion of the uniform space α (using Cauchy filters). These are not minimal filters.

• Completion α := Quotient (separationSetoid (CauchyFilter α)) the Hausdorff completion.

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.