# 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
Instances for UniformSpace
@[protected, instance]

The information required to build morphisms for UniformSpace.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def UniformSpace.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
Equations
def UniformSpace.of (α : Type u)  :

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

Equations
@[protected, instance]
Equations
@[simp]
theorem UniformSpace.coe_of (X : Type u)  :
= X
@[protected, instance]
def UniformSpace.quiver.hom.has_coe_to_fun (X Y : UniformSpace) :
has_coe_to_fun (X Y) (λ (_x : X Y), X → Y)
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
@[protected, instance]

The forgetful functor from uniform spaces to topological spaces.

Equations
structure CpltSepUniformSpace  :
Type (u+1)

A (bundled) complete separated uniform space.

Instances for CpltSepUniformSpace
@[protected, instance]
Equations

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

Equations
@[protected, instance]
@[protected, instance]

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

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

The category instance on CpltSepUniformSpace.

Equations
@[protected, instance]

The concrete category instance on CpltSepUniformSpace.

Equations
@[protected, instance]
Equations
noncomputable def UniformSpace.completion_functor  :

The functor turning uniform spaces into complete separated uniform spaces.

Equations

The inclusion of a uniform space into its completion.

Equations
noncomputable def UniformSpace.extension_hom {X : UniformSpace} {Y : CpltSepUniformSpace}  :

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

Equations

The completion functor is left adjoint to the forgetful functor.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations