Documentation

Mathlib.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 UniformSpaceCat :
Type (u + 1)

A (bundled) uniform space.

Instances For

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

    Instances For
      @[simp]
      theorem UniformSpaceCat.coe_mk {X : UniformSpaceCat} {Y : UniformSpaceCat} (f : XY) (hf : UniformContinuous f) :
      { val := f, property := hf } = f

      The forgetful functor from uniform spaces to topological spaces.

      structure CpltSepUniformSpace :
      Type (u + 1)

      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 functor turning uniform spaces into complete separated uniform spaces.

            Instances For

              The inclusion of a uniform space into its completion.

              Instances For

                The completion functor is left adjoint to the forgetful functor.

                Instances For