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

Equations
Instances For

The information required to build morphisms for UniformSpace.

Equations
Equations
Equations
• x.instUniformSpaceα = x.str

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

Equations
• = { α := α, str := inst }
Instances For
Equations
@[simp]
theorem UniformSpaceCat.coe_of (X : Type u) [] :
= X
instance UniformSpaceCat.instCoeFunHomForallαUniformSpace (X : UniformSpaceCat) (Y : UniformSpaceCat) :
CoeFun (X Y) fun (x : X Y) => XY
Equations
• X.instCoeFunHomForallαUniformSpace Y = { coe := }
@[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 : ) :
f, 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.

Equations
• One or more equations did not get rendered due to their size.
structure CpltSepUniformSpace :
Type (u + 1)

A (bundled) complete separated uniform space.

Instances For
Equations

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

Equations
• X.toUniformSpace =
Instances For
Equations
• =
instance CpltSepUniformSpace.t0Space (X : CpltSepUniformSpace) :
T0Space X.toUniformSpace
Equations
• =

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

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

The category instance on CpltSepUniformSpace.

Equations

The concrete category instance on CpltSepUniformSpace.

Equations

The functor turning uniform spaces into complete separated uniform spaces.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The inclusion of a uniform space into its completion.

Equations
• X.completionHom = X,
Instances For
@[simp]
theorem UniformSpaceCat.completionHom_val (X : UniformSpaceCat) (x : ) :
X.completionHom x = () x

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

Equations
Instances For
Equations
• X.instUniformSpaceObjForget = let_fun this := inferInstance; this
@[simp]

The completion functor is left adjoint to the forgetful functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For