# 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.

## References #

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.UniformSpace.Basic.

def CauchyFilter (α : Type u) [] :

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.

Equations
• = { f : // }
Instances For
instance CauchyFilter.instNeBotValFilterCauchy {α : Type u} [] (f : ) :
Equations
• =
def CauchyFilter.gen {α : Type u} [] (s : Set (α × α)) :
Set ()

The pairs of Cauchy filters generated by a set.

Equations
Instances For
theorem CauchyFilter.monotone_gen {α : Type u} [] :
Monotone CauchyFilter.gen
Equations
theorem CauchyFilter.mem_uniformity {α : Type u} [] {s : Set ()} :
s ∃ t ∈ ,
theorem CauchyFilter.basis_uniformity {α : Type u} [] {ι : Sort u_1} {p : ιProp} {s : ιSet (α × α)} (h : ) :
Filter.HasBasis () p (CauchyFilter.gen s)
theorem CauchyFilter.mem_uniformity' {α : Type u} [] {s : Set ()} :
s ∃ t ∈ , ∀ (f g : ), t f ×ˢ g(f, g) s
def CauchyFilter.pureCauchy {α : Type u} [] (a : α) :

Embedding of α into its completion CauchyFilter α

Equations
• = { val := pure a, property := }
Instances For
theorem CauchyFilter.uniformInducing_pureCauchy {α : Type u} [] :
UniformInducing CauchyFilter.pureCauchy
theorem CauchyFilter.uniformEmbedding_pureCauchy {α : Type u} [] :
UniformEmbedding CauchyFilter.pureCauchy
theorem CauchyFilter.denseRange_pureCauchy {α : Type u} [] :
DenseRange CauchyFilter.pureCauchy
theorem CauchyFilter.denseInducing_pureCauchy {α : Type u} [] :
DenseInducing CauchyFilter.pureCauchy
theorem CauchyFilter.denseEmbedding_pureCauchy {α : Type u} [] :
DenseEmbedding CauchyFilter.pureCauchy
Equations
• =
Equations
instance CauchyFilter.instNonemptyCauchyFilter {α : Type u} [] [h : ] :
Equations
• =
def CauchyFilter.extend {α : Type u} [] {β : Type v} [] (f : αβ) :
β

Extend a uniformly continuous function α → β to a function CauchyFilter α → β. Outputs junk when f is not uniformly continuous.

Equations
• = if then else fun (x : ) => f ()
Instances For
theorem CauchyFilter.extend_pureCauchy {α : Type u} [] {β : Type v} [] [] {f : αβ} (hf : ) (a : α) :
theorem CauchyFilter.uniformContinuous_extend {α : Type u} [] {β : Type v} [] [] {f : αβ} :
theorem CauchyFilter.inseparable_iff {α : Type u} [] {f : } {g : } :
f ×ˢ g
theorem CauchyFilter.inseparable_iff_of_le_nhds {α : Type u} [] {f : } {g : } {a : α} {b : α} (ha : f nhds a) (hb : g nhds b) :
theorem CauchyFilter.inseparable_lim_iff {α : Type u} [] [] {f : } {g : } :
Inseparable (lim f) (lim g)
theorem CauchyFilter.cauchyFilter_eq {α : Type u_1} [] [] [] {f : } {g : } :
lim f = lim g
def UniformSpace.Completion (α : Type u_1) [] :
Type u_1

Hausdorff completion of α

Equations
Instances For
instance UniformSpace.Completion.inhabited (α : Type u_1) [] [] :
Equations
Equations
• = SeparationQuotient.instUniformSpace
Equations
• =
instance UniformSpace.Completion.t0Space (α : Type u_1) [] :
Equations
• =

The map from a uniform space to its completion.

porting note: this was added to create a target for the @[coe] attribute.

Equations
• α = SeparationQuotient.mk CauchyFilter.pureCauchy
Instances For

Automatic coercion from α to its completion. Not always injective.

Equations
• = { coe := α }
theorem UniformSpace.Completion.coe_eq (α : Type u_1) [] :
α = SeparationQuotient.mk CauchyFilter.pureCauchy
theorem UniformSpace.Completion.comap_coe_eq_uniformity (α : Type u_1) [] :
Filter.comap (fun (p : α × α) => (α p.1, α p.2)) =

The Haudorff completion as an abstract completion.

Equations
• UniformSpace.Completion.cPkg = { space := , coe := α, uniformStruct := inferInstance, complete := , separation := , uniformInducing := , dense := }
Instances For
Equations
• = { default := UniformSpace.Completion.cPkg }

The uniform bijection between a complete space and its uniform completion.

Equations
Instances For
Equations
• =
theorem UniformSpace.Completion.denseRange_coe₂ {α : Type u_1} [] {β : Type u_2} [] :
DenseRange fun (x : α × β) => (α x.1, β x.2)
theorem UniformSpace.Completion.denseRange_coe₃ {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] :
DenseRange fun (x : α × β × γ) => (α x.1, β x.2.1, γ x.2.2)
theorem UniformSpace.Completion.induction_on {α : Type u_1} [] {p : } (a : ) (hp : IsClosed {a : | p a}) (ih : ∀ (a : α), p (α a)) :
p a
theorem UniformSpace.Completion.induction_on₂ {α : Type u_1} [] {β : Type u_2} [] {p : } (a : ) (b : ) (hp : IsClosed {x : | p x.1 x.2}) (ih : ∀ (a : α) (b : β), p (α a) (β b)) :
p a b
theorem UniformSpace.Completion.induction_on₃ {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] {p : } (a : ) (b : ) (c : ) (hp : IsClosed {x : | p x.1 x.2.1 x.2.2}) (ih : ∀ (a : α) (b : β) (c : γ), p (α a) (β b) (γ c)) :
p a b c
theorem UniformSpace.Completion.ext {α : Type u_1} [] {Y : Type u_4} [] [] {f : } {g : } (hf : ) (hg : ) (h : ∀ (a : α), f (α a) = g (α a)) :
f = g
theorem UniformSpace.Completion.ext' {α : Type u_1} [] {Y : Type u_4} [] [] {f : } {g : } (hf : ) (hg : ) (h : ∀ (a : α), f (α a) = g (α a)) (a : ) :
f a = g a
def UniformSpace.Completion.extension {α : Type u_1} [] {β : Type u_2} [] (f : αβ) :

"Extension" to the completion. It is defined for any map f but returns an arbitrary constant value if f is not uniformly continuous

Equations
Instances For
theorem UniformSpace.Completion.uniformContinuous_extension {α : Type u_1} [] {β : Type u_2} [] {f : αβ} [] :
theorem UniformSpace.Completion.continuous_extension {α : Type u_1} [] {β : Type u_2} [] {f : αβ} [] :
theorem UniformSpace.Completion.extension_coe {α : Type u_1} [] {β : Type u_2} [] {f : αβ} [] (hf : ) (a : α) :
= f a
theorem UniformSpace.Completion.extension_unique {α : Type u_1} [] {β : Type u_2} [] {f : αβ} [] [] (hf : ) {g : } (hg : ) (h : ∀ (a : α), f a = g (α a)) :
@[simp]
theorem UniformSpace.Completion.extension_comp_coe {α : Type u_1} [] {β : Type u_2} [] [] [] {f : } (hf : ) :
= f
def UniformSpace.Completion.map {α : Type u_1} [] {β : Type u_2} [] (f : αβ) :

Completion functor acting on morphisms

Equations
Instances For
theorem UniformSpace.Completion.uniformContinuous_map {α : Type u_1} [] {β : Type u_2} [] {f : αβ} :
theorem UniformSpace.Completion.continuous_map {α : Type u_1} [] {β : Type u_2} [] {f : αβ} :
theorem UniformSpace.Completion.map_coe {α : Type u_1} [] {β : Type u_2} [] {f : αβ} (hf : ) (a : α) :
UniformSpace.Completion.map f (α a) = β (f a)
theorem UniformSpace.Completion.map_unique {α : Type u_1} [] {β : Type u_2} [] {f : αβ} {g : } (hg : ) (h : ∀ (a : α), β (f a) = g (α a)) :
@[simp]
theorem UniformSpace.Completion.map_id {α : Type u_1} [] :
theorem UniformSpace.Completion.extension_map {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] [] [] {f : βγ} {g : αβ} (hf : ) (hg : ) :
theorem UniformSpace.Completion.map_comp {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] {g : βγ} {f : αβ} (hg : ) (hf : ) :

The isomorphism between the completion of a uniform space and the completion of its separation quotient.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def UniformSpace.Completion.extension₂ {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] (f : αβγ) :

Extend a two variable map to the Hausdorff completions.

Equations
Instances For
theorem UniformSpace.Completion.extension₂_coe_coe {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] {f : αβγ} [] (hf : ) (a : α) (b : β) :
UniformSpace.Completion.extension₂ f (α a) (β b) = f a b
theorem UniformSpace.Completion.uniformContinuous_extension₂ {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] (f : αβγ) [] :
def UniformSpace.Completion.map₂ {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] (f : αβγ) :

Lift a two variable map to the Hausdorff completions.

Equations
Instances For
theorem UniformSpace.Completion.uniformContinuous_map₂ {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] (f : αβγ) :
theorem UniformSpace.Completion.continuous_map₂ {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] {δ : Type u_4} [] {f : αβγ} {a : } {b : } (ha : ) (hb : ) :
Continuous fun (d : δ) => UniformSpace.Completion.map₂ f (a d) (b d)
theorem UniformSpace.Completion.map₂_coe_coe {α : Type u_1} [] {β : Type u_2} [] {γ : Type u_3} [] (a : α) (b : β) (f : αβγ) (hf : ) :
UniformSpace.Completion.map₂ f (α a) (β b) = γ (f a b)