mathlib documentation

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
def UniformSpace.of (α : Type u) [uniform_space α] :

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

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

@[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)

A (bundled) complete separated uniform space.

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

Equations

The functor turning uniform spaces into complete separated uniform spaces.

Equations