mathlib documentation

topology.category.UniformSpace

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!

source
def UniformSpace  :
Type (u+1)

A (bundled) uniform space.

Equations
source
@[instance]
def UniformSpace.category_theory.unbundled_hom  :
category_theory.unbundled_hom uniform_continuous

The information required to build morphisms for UniformSpace.

Equations
source
@[instance]
def UniformSpace.uniform_space (x : UniformSpace) :
uniform_space ↥x

Equations
source
def UniformSpace.of (α : Type u) [uniform_space α] :
UniformSpace

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

Equations
source
@[instance]
def UniformSpace.inhabited  :
inhabited UniformSpace

Equations
source
@[simp]
theorem UniformSpace.coe_of (X : Type u) [uniform_space X] :
↥(UniformSpace.of X) = X

source
@[instance]
def UniformSpace.has_coe_to_fun (X Y : UniformSpace) :
has_coe_to_fun (X ⟶ Y)

Equations
source
@[simp]
theorem UniformSpace.coe_comp {X Y Z : UniformSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :
⇑(f ≫ g) = ⇑g ∘ ⇑f

source
@[simp]
theorem UniformSpace.coe_id (X : UniformSpace) :
⇑(𝟙 X) = id

source
@[simp]
theorem UniformSpace.coe_mk {X Y : UniformSpace} (f : ↥X → ↥Y) (hf : uniform_continuous f) :
⇑⟨f, hf⟩ = f

source
theorem UniformSpace.hom_ext {X Y : UniformSpace} {f g : X ⟶ Y} (a : ⇑f = ⇑g) :
f = g

source
@[instance]
def UniformSpace.has_forget_to_Top  :
category_theory.has_forget₂ UniformSpace Top

The forgetful functor from uniform spaces to topological spaces.

Equations
source
structure CpltSepUniformSpace  :
Type (u+1)

A (bundled) complete separated uniform space.

source
@[instance]
def CpltSepUniformSpace.has_coe_to_sort  :
has_coe_to_sort CpltSepUniformSpace

Equations
source
def CpltSepUniformSpace.to_UniformSpace (X : CpltSepUniformSpace) :
UniformSpace

Equations
source
@[instance]
def CpltSepUniformSpace.complete_space (X : CpltSepUniformSpace) :
complete_space X.to_UniformSpace.α

source
@[instance]
def CpltSepUniformSpace.separated_space (X : CpltSepUniformSpace) :
separated_space X.to_UniformSpace.α

source
def CpltSepUniformSpace.of (X : Type u) [uniform_space X] [complete_space X] [separated_space X] :
CpltSepUniformSpace

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

Equations
source
@[simp]
theorem CpltSepUniformSpace.coe_of (X : Type u) [uniform_space X] [complete_space X] [separated_space X] :
↥(CpltSepUniformSpace.of X) = X

source
@[instance]
def CpltSepUniformSpace.inhabited  :
inhabited CpltSepUniformSpace

Equations
source
@[instance]
def CpltSepUniformSpace.category  :
category_theory.large_category CpltSepUniformSpace

The category instance on CpltSepUniformSpace.

Equations
source
@[instance]
def CpltSepUniformSpace.concrete_category  :
category_theory.concrete_category CpltSepUniformSpace

The concrete category instance on CpltSepUniformSpace.

Equations
source
@[instance]
def CpltSepUniformSpace.has_forget_to_UniformSpace  :
category_theory.has_forget₂ CpltSepUniformSpace UniformSpace

Equations
source
def UniformSpace.completion_functor  :
UniformSpace ⥤ CpltSepUniformSpace

The functor turning uniform spaces into complete separated uniform spaces.

Equations
source
def UniformSpace.completion_hom (X : UniformSpace) :
X ⟶ (category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj (UniformSpace.completion_functor.obj X)

The inclusion of a uniform space into its completion.

Equations
source
@[simp]
theorem UniformSpace.completion_hom_val (X : UniformSpace) (x : ↥X) :
⇑(X.completion_hom) x = ↑x

source
def UniformSpace.extension_hom {X : UniformSpace} {Y : CpltSepUniformSpace} (f : X ⟶ (category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj Y) :
UniformSpace.completion_functor.obj X ⟶ Y

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

Equations
source
@[simp]
theorem UniformSpace.extension_hom_val {X : UniformSpace} {Y : CpltSepUniformSpace} (f : X ⟶ (category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj Y) (x : ↥((UniformSpace.completion_functor.obj X).to_UniformSpace)) :
⇑(UniformSpace.extension_hom f) x = uniform_space.completion.extension ⇑f x

source
@[simp]
theorem UniformSpace.extension_comp_coe {X : UniformSpace} {Y : CpltSepUniformSpace} (f : (CpltSepUniformSpace.of (uniform_space.completion ↥X)).to_UniformSpace ⟶ Y.to_UniformSpace) :
UniformSpace.extension_hom (X.completion_hom ≫ f) = f

source
def UniformSpace.adj  :
UniformSpace.completion_functor ⊣ category_theory.forget₂ CpltSepUniformSpace UniformSpace

The completion functor is left adjoint to the forgetful functor.

Equations
source
@[instance]
def UniformSpace.category_theory.is_right_adjoint  :
category_theory.is_right_adjoint (category_theory.forget₂ CpltSepUniformSpace UniformSpace)

Equations
source
@[instance]
def UniformSpace.category_theory.reflective  :
category_theory.reflective (category_theory.forget₂ CpltSepUniformSpace UniformSpace)

Equations