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

• UniformSpaceCat = CategoryTheory.Bundled UniformSpace

instance UniformSpaceCat.instUnbundledHomTypeUniformSpaceUniformContinuous : CategoryTheory.UnbundledHom @UniformContinuous

The information required to build morphisms for UniformSpace.

Equations

• UniformSpaceCat.instUnbundledHomTypeUniformSpaceUniformContinuous = (_ : CategoryTheory.UnbundledHom @UniformContinuous)

instance UniformSpaceCat.instConcreteCategoryUniformSpaceCatInstUniformSpaceCatLargeCategory : CategoryTheory.ConcreteCategory UniformSpaceCat

Equations

• UniformSpaceCat.instConcreteCategoryUniformSpaceCatInstUniformSpaceCatLargeCategory = inferInstanceAs (CategoryTheory.ConcreteCategory (CategoryTheory.Bundled UniformSpace))

instance UniformSpaceCat.instCoeSortUniformSpaceCatType : CoeSort UniformSpaceCat (Type u_1)

Equations

• UniformSpaceCat.instCoeSortUniformSpaceCatType = CategoryTheory.Bundled.coeSort

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

Equations

• UniformSpaceCat.instUniformSpaceα x = x.str

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

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

Equations

• UniformSpaceCat.of α = CategoryTheory.Bundled.mk α

instance UniformSpaceCat.instInhabitedUniformSpaceCat : Inhabited UniformSpaceCat

Equations

• UniformSpaceCat.instInhabitedUniformSpaceCat = { default := UniformSpaceCat.of Empty }

@[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) => ↑X → ↑Y

Equations

• UniformSpaceCat.instCoeFunHomUniformSpaceCatToQuiverToCategoryStructInstUniformSpaceCatLargeCategoryForAllαUniformSpace X Y = { coe := (CategoryTheory.forget UniformSpaceCat).toPrefunctor.map }

@[simp]

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

@[simp]

theorem UniformSpaceCat.coe_id (X : UniformSpaceCat) : (CategoryTheory.forget UniformSpaceCat).toPrefunctor.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).toPrefunctor.map f = (CategoryTheory.forget UniformSpaceCat).toPrefunctor.map g → f = g

instance UniformSpaceCat.hasForgetToTop : CategoryTheory.HasForget₂ UniformSpaceCat TopCat

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.

• α : Type u

  The underlying space

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

instance CpltSepUniformSpace.instCoeSortCpltSepUniformSpaceType : CoeSort CpltSepUniformSpace (Type u)

Equations

• CpltSepUniformSpace.instCoeSortCpltSepUniformSpaceType = { coe := CpltSepUniformSpace.α }

def CpltSepUniformSpace.toUniformSpace (X : CpltSepUniformSpace) : UniformSpaceCat

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

Equations

• CpltSepUniformSpace.toUniformSpace X = UniformSpaceCat.of X.α

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

Equations

• (_ : CompleteSpace ↑(CpltSepUniformSpace.toUniformSpace X)) = (_ : CompleteSpace X.α)

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

Equations

• (_ : SeparatedSpace ↑(CpltSepUniformSpace.toUniformSpace X)) = (_ : SeparatedSpace 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.

Equations

• CpltSepUniformSpace.of X = CpltSepUniformSpace.mk X

@[simp]

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

instance CpltSepUniformSpace.instInhabitedCpltSepUniformSpace : Inhabited CpltSepUniformSpace

Equations

• CpltSepUniformSpace.instInhabitedCpltSepUniformSpace = { default := CpltSepUniformSpace.of Empty }

instance CpltSepUniformSpace.category : CategoryTheory.LargeCategory CpltSepUniformSpace

The category instance on CpltSepUniformSpace.

Equations

• CpltSepUniformSpace.category = CategoryTheory.InducedCategory.category CpltSepUniformSpace.toUniformSpace

instance CpltSepUniformSpace.concreteCategory : CategoryTheory.ConcreteCategory CpltSepUniformSpace

The concrete category instance on CpltSepUniformSpace.

Equations

• CpltSepUniformSpace.concreteCategory = CategoryTheory.InducedCategory.concreteCategory CpltSepUniformSpace.toUniformSpace

instance CpltSepUniformSpace.hasForgetToUniformSpace : CategoryTheory.HasForget₂ CpltSepUniformSpace UniformSpaceCat

Equations

• CpltSepUniformSpace.hasForgetToUniformSpace = CategoryTheory.InducedCategory.hasForget₂ CpltSepUniformSpace.toUniformSpace

noncomputable def UniformSpaceCat.completionFunctor : CategoryTheory.Functor UniformSpaceCat CpltSepUniformSpace

The functor turning uniform spaces into complete separated uniform spaces.

Equations

• One or more equations did not get rendered due to their size.

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

The inclusion of a uniform space into its completion.

Equations

• UniformSpaceCat.completionHom X = { val := ↑↑X, property := (_ : UniformContinuous ↑↑X) }

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UniformSpaceCat.extensionHom_val {X : UniformSpaceCat} {Y : CpltSepUniformSpace} (f : X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).toPrefunctor.obj Y) (x : (CategoryTheory.forget CpltSepUniformSpace).toPrefunctor.obj (UniformSpaceCat.completionFunctor.toPrefunctor.obj X)) : (UniformSpaceCat.extensionHom f) x = UniformSpace.Completion.extension ((CategoryTheory.forget UniformSpaceCat).toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.