mathlib docs: topology.category.UniformSpace

source

def UniformSpace :

Type (u+1)

A (bundled) uniform space.

Equations

UniformSpace = category_theory.bundled uniform_space

source

@[instance]

def UniformSpace.category_theory.unbundled_hom :

category_theory.unbundled_hom uniform_continuous

The information required to build morphisms for UniformSpace.

Equations

UniformSpace.category_theory.unbundled_hom = {hom_id := uniform_continuous_id, hom_comp := uniform_continuous.comp}

source

@[instance]

def UniformSpace.uniform_space (x : UniformSpace) :

uniform_space ↥x

Equations

x.uniform_space = x.str

source

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

UniformSpace

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

Equations

UniformSpace.of α = {α := α, str := _inst_1}

source

@[instance]

def UniformSpace.inhabited :

inhabited UniformSpace

Equations

UniformSpace.inhabited = {default := UniformSpace.of empty empty.uniform_space}

source

@[instance]

def UniformSpace.has_coe_to_fun (X Y : UniformSpace) :

has_coe_to_fun (X ⟶ Y)

Equations

X.has_coe_to_fun Y = {F := λ (_x : X ⟶ Y), ↥X → ↥Y, coe := (category_theory.forget UniformSpace).map Y}

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

@[instance]

def UniformSpace.has_forget_to_Top :

category_theory.has_forget₂ UniformSpace Top

The forgetful functor from uniform spaces to topological spaces.

Equations

UniformSpace.has_forget_to_Top = {forget₂ := {obj := λ (X : UniformSpace), Top.of ↥X, map := λ (X Y : UniformSpace) (f : X ⟶ Y), {to_fun := ⇑f, continuous_to_fun := _}, map_id' := UniformSpace.has_forget_to_Top._proof_2, map_comp' := UniformSpace.has_forget_to_Top._proof_3}, forget_comp := UniformSpace.has_forget_to_Top._proof_4}

source

structure CpltSepUniformSpace :

Type (u+1)

α : Type ?
is_uniform_space : uniform_space c.α
is_complete_space : complete_space c.α
is_separated : separated_space c.α

A (bundled) complete separated uniform space.

source

@[instance]

def CpltSepUniformSpace.has_coe_to_sort :

has_coe_to_sort CpltSepUniformSpace

Equations

CpltSepUniformSpace.has_coe_to_sort = {S := Type u, coe := CpltSepUniformSpace.α}

source

def CpltSepUniformSpace.to_UniformSpace :

CpltSepUniformSpace → UniformSpace

Equations

X.to_UniformSpace = UniformSpace.of ↥X

source

@[instance]

def CpltSepUniformSpace.complete_space (X : CpltSepUniformSpace) :

complete_space X.to_UniformSpace.α

Equations

_ = _

source

@[instance]

def CpltSepUniformSpace.separated_space (X : CpltSepUniformSpace) :

separated_space X.to_UniformSpace.α

Equations

_ = _

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

CpltSepUniformSpace.of X = CpltSepUniformSpace.mk X

source

@[instance]

def CpltSepUniformSpace.inhabited :

inhabited CpltSepUniformSpace

Equations

CpltSepUniformSpace.inhabited = {default := CpltSepUniformSpace.of empty CpltSepUniformSpace.inhabited._proof_2}

source

@[instance]

def CpltSepUniformSpace.category :

category_theory.large_category CpltSepUniformSpace

The category instance on CpltSepUniformSpace.

Equations

CpltSepUniformSpace.category = category_theory.induced_category.category CpltSepUniformSpace.to_UniformSpace

source

@[instance]

def CpltSepUniformSpace.concrete_category :

category_theory.concrete_category CpltSepUniformSpace

The concrete category instance on CpltSepUniformSpace.

Equations

CpltSepUniformSpace.concrete_category = category_theory.induced_category.concrete_category CpltSepUniformSpace.to_UniformSpace

source

@[instance]

def CpltSepUniformSpace.has_forget_to_UniformSpace :

category_theory.has_forget₂ CpltSepUniformSpace UniformSpace

Equations

CpltSepUniformSpace.has_forget_to_UniformSpace = category_theory.induced_category.has_forget₂ CpltSepUniformSpace.to_UniformSpace

source

def UniformSpace.completion_functor :

UniformSpace ⥤ CpltSepUniformSpace

The functor turning uniform spaces into complete separated uniform spaces.

Equations

UniformSpace.completion_functor = {obj := λ (X : UniformSpace), CpltSepUniformSpace.of (uniform_space.completion ↥X), map := λ (X Y : UniformSpace) (f : X ⟶ Y), ⟨uniform_space.completion.map f.val, _⟩, map_id' := UniformSpace.completion_functor._proof_8, map_comp' := UniformSpace.completion_functor._proof_9}

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

X.completion_hom = ⟨coe coe_to_lift, _⟩

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} :

(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

UniformSpace.extension_hom f = ⟨uniform_space.completion.extension ⇑f, _⟩

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

UniformSpace.adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : UniformSpace) (Y : CpltSepUniformSpace), {to_fun := λ (f : UniformSpace.completion_functor.obj X ⟶ Y), X.completion_hom ≫ f, inv_fun := λ (f : X ⟶ (category_theory.forget₂ CpltSepUniformSpace UniformSpace).obj Y), UniformSpace.extension_hom f, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := UniformSpace.adj._proof_3, hom_equiv_naturality_right' := UniformSpace.adj._proof_4}

source

@[instance]

def UniformSpace.category_theory.is_right_adjoint :

category_theory.is_right_adjoint (category_theory.forget₂ CpltSepUniformSpace UniformSpace)

Equations

UniformSpace.category_theory.is_right_adjoint = {left := UniformSpace.completion_functor, adj := UniformSpace.adj}

source

@[instance]

def UniformSpace.category_theory.reflective :

category_theory.reflective (category_theory.forget₂ CpltSepUniformSpace UniformSpace)

Equations

UniformSpace.category_theory.reflective = category_theory.reflective.mk

mathlib documentation

topology.category.UniformSpace

The category of uniform spaces

General documentation

Additional documentation

Library

mathlib documentation

topology.​category.​UniformSpace

The category of uniform spaces

General documentation

Additional documentation

Library

topology.category.UniformSpace