mathlib3 documentation

topology.category.UniformSpace

The category of uniform spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
Instances for UniformSpace
source
@[protected, instance]
def UniformSpace.uniform_continuous.category_theory.unbundled_hom  :
category_theory.unbundled_hom uniform_continuous

The information required to build morphisms for UniformSpace.

Equations
source
@[protected, instance]
def UniformSpace.large_category  :
category_theory.large_category UniformSpace
source
@[protected, instance]
def UniformSpace.concrete_category  :
category_theory.concrete_category UniformSpace
source
@[protected, instance]
def UniformSpace.has_coe_to_sort  :
has_coe_to_sort UniformSpace (Type u_1)
Equations
source
@[protected, 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
@[protected, instance]
def UniformSpace.inhabited  :
inhabited UniformSpace
Equations
source
@[simp]
theorem UniformSpace.coe_of (X : Type u) [uniform_space X] :
↥(UniformSpace.of X) = X
source
@[protected, instance]
def UniformSpace.quiver.hom.has_coe_to_fun (X Y : UniformSpace) :
has_coe_to_fun (X ⟶ Y) (λ (_x : X ⟶ Y), ↥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} :
⇑f = ⇑g → f = g
source
@[protected, 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.

Instances for CpltSepUniformSpace
source
@[protected, instance]
def CpltSepUniformSpace.has_coe_to_sort  :
has_coe_to_sort CpltSepUniformSpace (Type u)
Equations
source
def CpltSepUniformSpace.to_UniformSpace (X : CpltSepUniformSpace) :
UniformSpace

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

Equations
source
@[protected, instance]
def CpltSepUniformSpace.complete_space (X : CpltSepUniformSpace) :
complete_space X.to_UniformSpace.α
source
@[protected, 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
@[protected, instance]
def CpltSepUniformSpace.inhabited  :
inhabited CpltSepUniformSpace
Equations
source
@[protected, instance]
def CpltSepUniformSpace.category  :
category_theory.large_category CpltSepUniformSpace

The category instance on CpltSepUniformSpace.

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

The concrete category instance on CpltSepUniformSpace.

Equations
source
@[protected, instance]
def CpltSepUniformSpace.has_forget_to_UniformSpace  :
category_theory.has_forget₂ CpltSepUniformSpace UniformSpace
Equations
source
noncomputable 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
noncomputable 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
noncomputable def UniformSpace.adj  :
UniformSpace.completion_functor ⊣ category_theory.forget₂ CpltSepUniformSpace UniformSpace

The completion functor is left adjoint to the forgetful functor.

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