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.

Equations

• UniformSpaceCat.instUnbundledHomUniformSpaceUniformContinuous = ⋯

instance UniformSpaceCat.instConcreteCategory : CategoryTheory.ConcreteCategory UniformSpaceCat

Equations

• UniformSpaceCat.instConcreteCategory = inferInstanceAs (CategoryTheory.ConcreteCategory (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] : ↑(UniformSpaceCat.of X) = X

instance UniformSpaceCat.instCoeFunHomForallαUniformSpace (X : UniformSpaceCat) (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 : 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) : ↑⟨f, 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.

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.α

theorem CpltSepUniformSpace.isCompleteSpace (self : CpltSepUniformSpace) : CompleteSpace self.α

theorem CpltSepUniformSpace.isT0 (self : CpltSepUniformSpace) : 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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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] : (CpltSepUniformSpace.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.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).obj (UniformSpaceCat.completionFunctor.obj X)

The inclusion of a uniform space into its completion.

Equations

• X.completionHom = ⟨↑↑X, ⋯⟩

@[simp]

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

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 = let_fun this := inferInstance; this

@[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.of (UniformSpace.Completion ↑X)).toUniformSpace ⟶ Y.toUniformSpace) : UniformSpaceCat.extensionHom (CategoryTheory.CategoryStruct.comp X.completionHom 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.instReflectiveCpltSepUniformSpaceForget₂ : CategoryTheory.Reflective (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat)

Equations

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