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.

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

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

    Equations
    Instances For
      @[simp]
      instance UniformSpaceCat.instCoeFunHomForallαUniformSpace (X : UniformSpaceCat) (Y : UniformSpaceCat) :
      CoeFun (X Y) fun (x : X Y) => XY
      Equations
      theorem UniformSpaceCat.coe_mk {X : UniformSpaceCat} {Y : UniformSpaceCat} (f : XY) (hf : UniformContinuous f) :
      f, hf = f

      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

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

        Equations
        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

            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
                Equations
                • X.instUniformSpaceObjForget = let_fun this := inferInstance; this

                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