# mathlibdocumentation

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 UniformSpace  :
Type (u+1)

A (bundled) uniform space.

Equations
@[instance]

The information required to build morphisms for UniformSpace.

Equations
@[instance]

@[instance]

@[instance]

Equations
def UniformSpace.of (α : Type u)  :

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

Equations
@[instance]

Equations
@[simp]
theorem UniformSpace.coe_of (X : Type u)  :
= X

@[instance]

Equations
@[simp]
theorem UniformSpace.coe_comp {X Y Z : UniformSpace} (f : X Y) (g : Y Z) :
(f g) = g f

@[simp]

@[simp]
theorem UniformSpace.coe_mk {X Y : UniformSpace} (f : X → Y) (hf : uniform_continuous f) :
f, hf⟩ = f

theorem UniformSpace.hom_ext {X Y : UniformSpace} {f g : X Y} :
f = gf = g

@[instance]

The forgetful functor from uniform spaces to topological spaces.

Equations
structure CpltSepUniformSpace  :
Type (u+1)
• α : Type ?
• is_uniform_space :
• is_complete_space :
• is_separated :

A (bundled) complete separated uniform space.

Equations
@[instance]

@[instance]

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

Equations
@[simp]
theorem CpltSepUniformSpace.coe_of (X : Type u)  :

@[instance]

Equations
@[instance]

The category instance on CpltSepUniformSpace.

Equations
@[instance]

The concrete category instance on CpltSepUniformSpace.

Equations
@[instance]

Equations

The functor turning uniform spaces into complete separated uniform spaces.

Equations

The inclusion of a uniform space into its completion.

Equations

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

Equations

The completion functor is left adjoint to the forgetful functor.

Equations
@[instance]

Equations
@[instance]

Equations