# Documentation

Mathlib.Topology.Category.UniformSpace

# The category of uniform spaces #

We construct the category of uniform spaces, show that the complete separated uniform spaces form a reflective subcategory, and hence possess all limits that uniform spaces do.

TODO: show that uniform spaces actually have all limits!

def UniformSpaceCat :
Type (u + 1)

A (bundled) uniform space.

Instances For

The information required to build morphisms for UniformSpace.

Construct a bundled UniformSpace from the underlying type and the typeclass.

Instances For
@[simp]
theorem UniformSpaceCat.coe_of (X : Type u) [] :
↑() = X
@[simp]
theorem UniformSpaceCat.coe_comp {X : UniformSpaceCat} {Y : UniformSpaceCat} {Z : UniformSpaceCat} (f : X Y) (g : Y Z) :
theorem UniformSpaceCat.coe_mk {X : UniformSpaceCat} {Y : UniformSpaceCat} (f : XY) (hf : ) :
{ val := f, property := hf } = f
theorem UniformSpaceCat.hom_ext {X : UniformSpaceCat} {Y : UniformSpaceCat} {f : X Y} {g : X Y} :
f = g

The forgetful functor from uniform spaces to topological spaces.

structure CpltSepUniformSpace :
Type (u + 1)
• α : Type u

The underlying space

• isUniformSpace : UniformSpace s
• isCompleteSpace :
• isSeparated :

A (bundled) complete separated uniform space.

Instances For

The function forgetting that a complete separated uniform spaces is complete and separated.

Instances For

Construct a bundled UniformSpace from the underlying type and the appropriate typeclasses.

Instances For
@[simp]
theorem CpltSepUniformSpace.coe_of (X : Type u) [] [] [] :
().α = X

The category instance on CpltSepUniformSpace.

The concrete category instance on CpltSepUniformSpace.

The functor turning uniform spaces into complete separated uniform spaces.

Instances For

The inclusion of a uniform space into its completion.

Instances For
@[simp]
theorem UniformSpaceCat.completionHom_val (X : UniformSpaceCat) (x : ) :
= ↑() x

The mate of a morphism from a UniformSpace to a CpltSepUniformSpace.

Instances For

The completion functor is left adjoint to the forgetful functor.

Instances For