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.

instance UniformSpaceCat.instUnbundledHomTypeUniformSpaceUniformContinuous : CategoryTheory.UnbundledHom @UniformContinuous

The information required to build morphisms for UniformSpace.

instance UniformSpaceCat.instConcreteCategoryUniformSpaceCatInstUniformSpaceCatLargeCategory : CategoryTheory.ConcreteCategory UniformSpaceCat

instance UniformSpaceCat.instCoeSortUniformSpaceCatType : CoeSort UniformSpaceCat (Type u_1)

instance UniformSpaceCat.instUniformSpaceα (x : UniformSpaceCat) : UniformSpace ↑x

def UniformSpaceCat.of (α : Type u) [UniformSpace α] : UniformSpaceCat

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

instance UniformSpaceCat.instInhabitedUniformSpaceCat : Inhabited UniformSpaceCat

@[simp]

theorem UniformSpaceCat.coe_of (X : Type u) [UniformSpace X] : ↑(UniformSpaceCat.of X) = X

instance UniformSpaceCat.instCoeFunHomUniformSpaceCatToQuiverToCategoryStructInstUniformSpaceCatLargeCategoryForAllαUniformSpace (X : UniformSpaceCat) (Y : UniformSpaceCat) : CoeFun (X ⟶ Y) fun x => ↑X → ↑Y

@[simp]

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

@[simp]

theorem UniformSpaceCat.coe_id (X : UniformSpaceCat) : (CategoryTheory.forget UniformSpaceCat).map (CategoryTheory.CategoryStruct.id X) = id

theorem UniformSpaceCat.coe_mk {X : UniformSpaceCat} {Y : UniformSpaceCat} (f : ↑X → ↑Y) (hf : UniformContinuous f) : ↑{ val := f, property := hf } = f

theorem UniformSpaceCat.hom_ext {X : UniformSpaceCat} {Y : UniformSpaceCat} {f : X ⟶ Y} {g : X ⟶ Y} : (CategoryTheory.forget UniformSpaceCat).map f = (CategoryTheory.forget UniformSpaceCat).map g → f = g

instance UniformSpaceCat.hasForgetToTop : CategoryTheory.HasForget₂ UniformSpaceCat TopCat

The forgetful functor from uniform spaces to topological spaces.

structure CpltSepUniformSpace : Type (u + 1)

• α : Type u

  The underlying space

• isUniformSpace : UniformSpace s.α
• isCompleteSpace : CompleteSpace s.α
• isSeparated : SeparatedSpace s.α

A (bundled) complete separated uniform space.

instance CpltSepUniformSpace.instCoeSortCpltSepUniformSpaceType : 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 ↑(CpltSepUniformSpace.toUniformSpace X)

instance CpltSepUniformSpace.separatedSpace (X : CpltSepUniformSpace) : SeparatedSpace ↑(CpltSepUniformSpace.toUniformSpace X)

def CpltSepUniformSpace.of (X : Type u) [UniformSpace X] [CompleteSpace X] [SeparatedSpace 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] [SeparatedSpace X] : (CpltSepUniformSpace.of X).α = X

instance CpltSepUniformSpace.instInhabitedCpltSepUniformSpace : Inhabited CpltSepUniformSpace

instance CpltSepUniformSpace.category : CategoryTheory.LargeCategory CpltSepUniformSpace

The category instance on CpltSepUniformSpace.

instance CpltSepUniformSpace.concreteCategory : CategoryTheory.ConcreteCategory CpltSepUniformSpace

The concrete category instance on CpltSepUniformSpace.

instance CpltSepUniformSpace.hasForgetToUniformSpace : CategoryTheory.HasForget₂ CpltSepUniformSpace UniformSpaceCat

noncomputable def UniformSpaceCat.completionFunctor : CategoryTheory.Functor UniformSpaceCat CpltSepUniformSpace

The functor turning uniform spaces into complete separated uniform spaces.

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

The inclusion of a uniform space into its completion.

@[simp]

theorem UniformSpaceCat.completionHom_val (X : UniformSpaceCat) (x : (CategoryTheory.forget UniformSpaceCat).obj X) : (CategoryTheory.forget UniformSpaceCat).map (UniformSpaceCat.completionHom X) x = ↑((CategoryTheory.forget UniformSpaceCat).obj X) x

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

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

instance UniformSpaceCat.instUniformSpaceObjUniformSpaceCatToQuiverToCategoryStructInstUniformSpaceCatLargeCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForget (X : UniformSpaceCat) : UniformSpace ((CategoryTheory.forget UniformSpaceCat).obj X)

@[simp]

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

@[simp]

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

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

The completion functor is left adjoint to the forgetful functor.

noncomputable instance UniformSpaceCat.instIsRightAdjointUniformSpaceCatInstUniformSpaceCatLargeCategoryCpltSepUniformSpaceCategoryForget₂ConcreteCategoryInstConcreteCategoryUniformSpaceCatInstUniformSpaceCatLargeCategoryHasForgetToUniformSpace : CategoryTheory.IsRightAdjoint (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat)

noncomputable instance UniformSpaceCat.instReflectiveUniformSpaceCatCpltSepUniformSpaceInstUniformSpaceCatLargeCategoryCategoryForget₂ConcreteCategoryInstConcreteCategoryUniformSpaceCatInstUniformSpaceCatLargeCategoryHasForgetToUniformSpace : CategoryTheory.Reflective (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat)