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!
The information required to build morphisms for UniformSpace
.
Construct a bundled UniformSpace
from the underlying type and the typeclass.
Instances For
The forgetful functor from uniform spaces to topological spaces.
- α : Type u
The underlying space
- isUniformSpace : UniformSpace s.α
- isCompleteSpace : CompleteSpace s.α
- isSeparated : SeparatedSpace s.α
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
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
The mate of a morphism from a UniformSpace
to a CpltSepUniformSpace
.
Instances For
The completion functor is left adjoint to the forgetful functor.