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!

structure UniformSpaceCat : Type (u + 1)

An object in the category of uniform spaces.

• of :: (
• carrier : Type u

  The underlying uniform space.

• str : UniformSpace self.carrier
• )

@[implicit_reducible]

instance UniformSpaceCat.instCoeSortType : CoeSort UniformSpaceCat (Type u_1)

structure UniformSpaceCat.Hom (X : UniformSpaceCat) (Y : UniformSpaceCat) : Type (max u_1 u_2)

A bundled uniform continuous map.

• hom' : { f : X.carrier → Y.carrier // UniformContinuous f }

  The underlying UniformContinuous function.

theorem UniformSpaceCat.Hom.ext {X : UniformSpaceCat} {Y : UniformSpaceCat} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

theorem UniformSpaceCat.Hom.ext_iff {X : UniformSpaceCat} {Y : UniformSpaceCat} {x y : X.Hom Y} : x = y ↔ x.hom' = y.hom'

@[implicit_reducible]

instance UniformSpaceCat.instLargeCategory : CategoryTheory.LargeCategory UniformSpaceCat

@[implicit_reducible]

instance UniformSpaceCat.instFunLike (X : UniformSpaceCat) (Y : UniformSpaceCat) : FunLike { f : X.carrier → Y.carrier // UniformContinuous f } X.carrier Y.carrier

@[implicit_reducible]

instance UniformSpaceCat.instConcreteCategorySubtypeForallCarrierUniformContinuous : CategoryTheory.ConcreteCategory UniformSpaceCat fun (x1 x2 : UniformSpaceCat) => { f : x1.carrier → x2.carrier // UniformContinuous f }

@[reducible, inline]

abbrev UniformSpaceCat.Hom.hom {X Y : UniformSpaceCat} (f : X.Hom Y) : { f : X.carrier → Y.carrier // UniformContinuous f }

Turn a morphism in UniformSpaceCat back into a function which is UniformContinuous.

@[reducible, inline]

abbrev UniformSpaceCat.ofHom {X Y : Type u} [UniformSpace X] [UniformSpace Y] (f : { f : X → Y // UniformContinuous f }) : { carrier := X, str := inst✝ } ⟶ { carrier := Y, str := inst✝¹ }

Typecheck a function which is UniformContinuous as a morphism in UniformSpaceCat.

@[implicit_reducible]

instance UniformSpaceCat.instInhabited : Inhabited UniformSpaceCat

theorem UniformSpaceCat.coe_of (X : Type u) [UniformSpace X] : { carrier := X, str := inst✝ }.carrier = X

@[simp]

theorem UniformSpaceCat.hom_comp {X Y Z : UniformSpaceCat} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = ⟨⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f), ⋯⟩

@[simp]

theorem UniformSpaceCat.hom_id (X : UniformSpaceCat) : Hom.hom (CategoryTheory.CategoryStruct.id X) = ⟨id, ⋯⟩

@[simp]

theorem UniformSpaceCat.hom_ofHom {X Y : Type u} [UniformSpace X] [UniformSpace Y] (f : { f : X → Y // UniformContinuous f }) : Hom.hom (ofHom f) = f

theorem UniformSpaceCat.coe_comp {X Y Z : UniformSpaceCat} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem UniformSpaceCat.coe_id (X : UniformSpaceCat) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

theorem UniformSpaceCat.coe_mk {X Y : UniformSpaceCat} (f : X.carrier → Y.carrier) (hf : UniformContinuous f) : ⇑{ hom' := ⟨f, hf⟩ }.hom = f

theorem UniformSpaceCat.hom_ext {X Y : UniformSpaceCat} {f g : X ⟶ Y} (h : ⇑(CategoryTheory.ConcreteCategory.hom f) = ⇑(CategoryTheory.ConcreteCategory.hom g)) : f = g

theorem UniformSpaceCat.hom_ext_iff {X Y : UniformSpaceCat} {f g : X ⟶ Y} : f = g ↔ ⇑(CategoryTheory.ConcreteCategory.hom f) = ⇑(CategoryTheory.ConcreteCategory.hom g)

@[implicit_reducible]

instance UniformSpaceCat.hasForgetToTop : CategoryTheory.HasForget₂ UniformSpaceCat TopCat

The forgetful functor from uniform spaces to topological spaces.

structure CpltSepUniformSpace : Type (u + 1)

A (bundled) complete separated uniform space.

• α : Type u

  The underlying space

• isUniformSpace : UniformSpace self.α
• isCompleteSpace : CompleteSpace self.α
• isT0 : T0Space self.α

@[implicit_reducible]

instance CpltSepUniformSpace.instCoeSortType : CoeSort CpltSepUniformSpace (Type u)

def CpltSepUniformSpace.toUniformSpace (X : CpltSepUniformSpace) : UniformSpaceCat

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

instance CpltSepUniformSpace.completeSpace (X : CpltSepUniformSpace) : CompleteSpace X.toUniformSpace.carrier

instance CpltSepUniformSpace.t0Space (X : CpltSepUniformSpace) : T0Space X.toUniformSpace.carrier

def CpltSepUniformSpace.of (X : Type u) [UniformSpace X] [CompleteSpace X] [T0Space X] : CpltSepUniformSpace

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

@[simp]

theorem CpltSepUniformSpace.coe_of (X : Type u) [UniformSpace X] [CompleteSpace X] [T0Space X] : (of X).α = X

@[implicit_reducible]

instance CpltSepUniformSpace.instInhabited : Inhabited CpltSepUniformSpace

@[implicit_reducible]

instance CpltSepUniformSpace.category : CategoryTheory.LargeCategory CpltSepUniformSpace

The category instance on CpltSepUniformSpace.

@[implicit_reducible]

instance CpltSepUniformSpace.instFunLike (X : CpltSepUniformSpace) (Y : CpltSepUniformSpace) : FunLike { f : X.α → Y.α // UniformContinuous f } X.α Y.α

@[implicit_reducible]

instance CpltSepUniformSpace.concreteCategory : CategoryTheory.ConcreteCategory CpltSepUniformSpace fun (x1 x2 : CpltSepUniformSpace) => { f : x1.α → x2.α // UniformContinuous f }

The concrete category instance on CpltSepUniformSpace.

@[implicit_reducible]

instance CpltSepUniformSpace.hasForgetToUniformSpace : CategoryTheory.HasForget₂ CpltSepUniformSpace UniformSpaceCat

@[simp]

theorem CpltSepUniformSpace.hom_comp {X Y Z : CpltSepUniformSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g) = ⟨⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f), ⋯⟩

@[simp]

theorem CpltSepUniformSpace.hom_id (X : CpltSepUniformSpace) : CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X) = ⟨id, ⋯⟩

@[simp]

theorem CpltSepUniformSpace.hom_ofHom {X Y : Type u} [UniformSpace X] [UniformSpace Y] (f : { f : X → Y // UniformContinuous f }) : UniformSpaceCat.Hom.hom (UniformSpaceCat.ofHom f) = f

noncomputable def UniformSpaceCat.completionFunctor : CategoryTheory.Functor UniformSpaceCat CpltSepUniformSpace

The functor turning uniform spaces into complete separated uniform spaces.

@[simp]

theorem UniformSpaceCat.completionFunctor_map {X✝ Y✝ : UniformSpaceCat} (f : X✝ ⟶ Y✝) : completionFunctor.map f = CategoryTheory.ConcreteCategory.ofHom ⟨UniformSpace.Completion.map ⇑f.hom', ⋯⟩

noncomputable def UniformSpaceCat.completionHom (X : UniformSpaceCat) : X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj (completionFunctor.obj X)

The inclusion of a uniform space into its completion.

@[simp]

theorem UniformSpaceCat.completionHom_val (X : UniformSpaceCat) (x : X.carrier) : (CategoryTheory.ConcreteCategory.hom X.completionHom) x = ↑x

noncomputable def UniformSpaceCat.extensionHom {X : UniformSpaceCat} {Y : CpltSepUniformSpace} (f : X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y) : completionFunctor.obj X ⟶ Y

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

@[simp]

theorem UniformSpaceCat.extensionHom_val {X : UniformSpaceCat} {Y : CpltSepUniformSpace} (f : X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y) (x : (completionFunctor.obj X).α) : (CategoryTheory.ConcreteCategory.hom (extensionHom f)) x = UniformSpace.Completion.extension (⇑(CategoryTheory.ConcreteCategory.hom f)) x

@[simp]

theorem UniformSpaceCat.extension_comp_hom {X : UniformSpaceCat} {Y : CpltSepUniformSpace} (f : (CpltSepUniformSpace.of (UniformSpace.Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace) : (extensionHom (CategoryTheory.CategoryStruct.comp X.completionHom f)).hom = f

@[deprecated UniformSpaceCat.extension_comp_hom (since := "2025-12-18")]

theorem UniformSpaceCat.extension_comp_coe {X : UniformSpaceCat} {Y : CpltSepUniformSpace} (f : (CpltSepUniformSpace.of (UniformSpace.Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace) : (extensionHom (CategoryTheory.CategoryStruct.comp X.completionHom f)).hom = f

Alias of UniformSpaceCat.extension_comp_hom.

noncomputable def UniformSpaceCat.adj : completionFunctor ⊣ CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat

The completion functor is left adjoint to the forgetful functor.

@[implicit_reducible]

noncomputable instance UniformSpaceCat.instReflectiveCpltSepUniformSpaceForget₂SubtypeForallαUniformContinuousForallCarrier : CategoryTheory.Reflective (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat)