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.instUnbundledHomUniformSpaceUniformContinuous : CategoryTheory.UnbundledHom @UniformContinuous

The information required to build morphisms for UniformSpace.

instance instUniformSpaceCatLargeCategory : CategoryTheory.LargeCategory UniformSpaceCat

Equations

• instUniformSpaceCatLargeCategory = CategoryTheory.BundledHom.category fun (α β : Type ?u.9) (Iα : UniformSpace α) (Iβ : UniformSpace β) => Subtype UniformContinuous

instance UniformSpaceCat.instHasForget : CategoryTheory.HasForget UniformSpaceCat

Equations

• UniformSpaceCat.instHasForget = inferInstanceAs (CategoryTheory.HasForget (CategoryTheory.Bundled UniformSpace))

instance UniformSpaceCat.instCoeSortType : CoeSort UniformSpaceCat (Type u_1)

Equations

• UniformSpaceCat.instCoeSortType = CategoryTheory.Bundled.coeSort

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

Equations

• x.instUniformSpaceα = x.str

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

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

Equations

• UniformSpaceCat.of α = { α := α, str := inst✝ }

instance UniformSpaceCat.instInhabited : Inhabited UniformSpaceCat

Equations

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

@[simp]

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

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

Equations

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

@[simp]

theorem UniformSpaceCat.coe_comp {X Y 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 Y : UniformSpaceCat} (f : ↑X → ↑Y) (hf : UniformContinuous f) : ↑⟨f, hf⟩ = f

theorem UniformSpaceCat.hom_ext {X Y : UniformSpaceCat} {f 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.

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.α
• isT0 : T0Space self.α

instance CpltSepUniformSpace.instCoeSortType : CoeSort CpltSepUniformSpace (Type u)

Equations

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

def CpltSepUniformSpace.toUniformSpace (X : CpltSepUniformSpace) : UniformSpaceCat

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

Equations

• X.toUniformSpace = UniformSpaceCat.of X.α

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

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

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.

Equations

• CpltSepUniformSpace.of X = CpltSepUniformSpace.mk X

@[simp]

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

instance CpltSepUniformSpace.instInhabited : Inhabited CpltSepUniformSpace

Equations

• CpltSepUniformSpace.instInhabited = { 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.hasForget : CategoryTheory.HasForget CpltSepUniformSpace

The concrete category instance on CpltSepUniformSpace.

Equations

• CpltSepUniformSpace.hasForget = CategoryTheory.InducedCategory.hasForget 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).obj (completionFunctor.obj X)

The inclusion of a uniform space into its completion.

Equations

• X.completionHom = ⟨UniformSpace.Completion.coe', ⋯⟩

@[simp]

theorem UniformSpaceCat.completionHom_val (X : UniformSpaceCat) (x : (CategoryTheory.forget UniformSpaceCat).obj X) : (CategoryTheory.forget UniformSpaceCat).map 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.

Equations

• UniformSpaceCat.extensionHom f = ⟨UniformSpace.Completion.extension ((CategoryTheory.forget UniformSpaceCat).map f), ⋯⟩

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

Equations

• X.instUniformSpaceObjForget = inferInstance

@[simp]

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

@[simp]

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

noncomputable def UniformSpaceCat.adj : 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.instReflectiveCpltSepUniformSpaceForget₂ : CategoryTheory.Reflective (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat)

Equations

• UniformSpaceCat.instReflectiveCpltSepUniformSpaceForget₂ = CategoryTheory.Reflective.mk UniformSpaceCat.completionFunctor UniformSpaceCat.adj