mathlib3 documentation

topology.category.Top.open_nhds

The category of open neighborhoods of a point #

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

Given an object X of the category Top of topological spaces and a point x : X, this file builds the type open_nhds x of open neighborhoods of x in X and endows it with the partial order given by inclusion and the corresponding category structure (as a full subcategory of the poset category set X). This is used in topology.sheaves.stalks to build the stalk of a sheaf at x as a limit over open_nhds x.

Main declarations #

Besides open_nhds, the main constructions here are:

inclusion (x : X): the obvious functor open_nhds x ⥤ opens X
functor_nhds: An open map f : X ⟶ Y induces a functor open_nhds x ⥤ open_nhds (f x)
adjunction_nhds: An open map f : X ⟶ Y induces an adjunction between open_nhds x and open_nhds (f x).

def topological_space.open_nhds {X : Top} (x : ↥X) :

The type of open neighbourhoods of a point x in a (bundled) topological space.

Equations

topological_space.open_nhds x = category_theory.full_subcategory (λ (U : topological_space.opens ↥X), x ∈ U)

Instances for topological_space.open_nhds

@[protected, instance]

def topological_space.open_nhds.partial_order {X : Top} (x : ↥X) :

partial_order (topological_space.open_nhds x)

Equations

topological_space.open_nhds.partial_order x = {le := λ (U V : topological_space.open_nhds x), U.obj ≤ V.obj, lt := preorder.lt._default (λ (U V : topological_space.open_nhds x), U.obj ≤ V.obj), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def topological_space.open_nhds.lattice {X : Top} (x : ↥X) :

lattice (topological_space.open_nhds x)

Equations

topological_space.open_nhds.lattice x = {sup := λ (U V : topological_space.open_nhds x), {obj := U.obj ⊔ V.obj, property := _}, le := partial_order.le (topological_space.open_nhds.partial_order x), lt := partial_order.lt (topological_space.open_nhds.partial_order x), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (U V : topological_space.open_nhds x), {obj := U.obj ⊓ V.obj, property := _}, inf_le_left := _, inf_le_right := _, le_inf := _}

@[protected, instance]

def topological_space.open_nhds.order_top {X : Top} (x : ↥X) :

order_top (topological_space.open_nhds x)

Equations

topological_space.open_nhds.order_top x = {top := {obj := ⊤, property := trivial}, le_top := _}

@[protected, instance]

def topological_space.open_nhds.inhabited {X : Top} (x : ↥X) :

inhabited (topological_space.open_nhds x)

Equations

topological_space.open_nhds.inhabited x = {default := ⊤}

@[protected, instance]

def topological_space.open_nhds.open_nhds_category {X : Top} (x : ↥X) :

category_theory.category (topological_space.open_nhds x)

Equations

topological_space.open_nhds.open_nhds_category x = _.mpr (category_theory.full_subcategory.category (λ (U : topological_space.opens ↥X), x ∈ U))

@[protected, instance]

def topological_space.open_nhds.opens_nhds_hom_has_coe_to_fun {X : Top} {x : ↥X} {U V : topological_space.open_nhds x} :

has_coe_to_fun (U ⟶ V) (λ (_x : U ⟶ V), ↥(U.obj) → ↥(V.obj))

Equations

topological_space.open_nhds.opens_nhds_hom_has_coe_to_fun = {coe := λ (f : U ⟶ V) (x_1 : ↥(U.obj)), ⟨↑x_1, _⟩}

def topological_space.open_nhds.inf_le_left {X : Top} {x : ↥X} (U V : topological_space.open_nhds x) :

U ⊓ V ⟶ U

The inclusion U ⊓ V ⟶ U as a morphism in the category of open sets.

Equations

U.inf_le_left V = category_theory.hom_of_le _

def topological_space.open_nhds.inf_le_right {X : Top} {x : ↥X} (U V : topological_space.open_nhds x) :

U ⊓ V ⟶ V

The inclusion U ⊓ V ⟶ V as a morphism in the category of open sets.

Equations

U.inf_le_right V = category_theory.hom_of_le _

def topological_space.open_nhds.inclusion {X : Top} (x : ↥X) :

topological_space.open_nhds x ⥤ topological_space.opens ↥X

The inclusion functor from open neighbourhoods of x to open sets in the ambient topological space.

Equations

topological_space.open_nhds.inclusion x = category_theory.full_subcategory_inclusion (λ (U : topological_space.opens ↥X), x ∈ U)

@[simp]

theorem topological_space.open_nhds.inclusion_obj {X : Top} (x : ↥X) (U : topological_space.opens ↥X) (p : x ∈ U) :

(topological_space.open_nhds.inclusion x).obj {obj := U, property := p} = U

theorem topological_space.open_nhds.open_embedding {X : Top} {x : ↥X} (U : topological_space.open_nhds x) :

open_embedding ⇑(U.obj.inclusion)

def topological_space.open_nhds.map {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

topological_space.open_nhds (⇑f x) ⥤ topological_space.open_nhds x

The preimage functor from neighborhoods of f x to neighborhoods of x.

Equations

topological_space.open_nhds.map f x = {obj := λ (U : topological_space.open_nhds (⇑f x)), {obj := (topological_space.opens.map f).obj U.obj, property := _}, map := λ (U V : topological_space.open_nhds (⇑f x)) (i : U ⟶ V), (topological_space.opens.map f).map i, map_id' := _, map_comp' := _}

@[simp]

theorem topological_space.open_nhds.map_obj {X Y : Top} (f : X ⟶ Y) (x : ↥X) (U : topological_space.opens ↥Y) (q : ⇑f x ∈ U) :

(topological_space.open_nhds.map f x).obj {obj := U, property := q} = {obj := (topological_space.opens.map f).obj U, property := q}

@[simp]

theorem topological_space.open_nhds.map_id_obj {X : Top} (x : ↥X) (U : topological_space.open_nhds (⇑(𝟙 X) x)) :

(topological_space.open_nhds.map (𝟙 X) x).obj U = U

@[simp]

theorem topological_space.open_nhds.map_id_obj' {X : Top} (x : ↥X) (U : set ↥X) (p : is_open U) (q : ⇑(𝟙 X) x ∈ {carrier := U, is_open' := p}) :

(topological_space.open_nhds.map (𝟙 X) x).obj {obj := {carrier := U, is_open' := p}, property := q} = {obj := {carrier := U, is_open' := p}, property := q}

@[simp]

theorem topological_space.open_nhds.map_id_obj_unop {X : Top} (x : ↥X) (U : (topological_space.open_nhds x)ᵒᵖ) :

(topological_space.open_nhds.map (𝟙 X) x).obj (opposite.unop U) = opposite.unop U

@[simp]

theorem topological_space.open_nhds.op_map_id_obj {X : Top} (x : ↥X) (U : (topological_space.open_nhds x)ᵒᵖ) :

(topological_space.open_nhds.map (𝟙 X) x).op.obj U = U

def topological_space.open_nhds.inclusion_map_iso {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

topological_space.open_nhds.inclusion (⇑f x) ⋙ topological_space.opens.map f ≅ topological_space.open_nhds.map f x ⋙ topological_space.open_nhds.inclusion x

opens.map f and open_nhds.map f form a commuting square (up to natural isomorphism) with the inclusion functors into opens X.

Equations

topological_space.open_nhds.inclusion_map_iso f x = category_theory.nat_iso.of_components (λ (U : topological_space.open_nhds (⇑f x)), {hom := 𝟙 ((topological_space.open_nhds.inclusion (⇑f x) ⋙ topological_space.opens.map f).obj U), inv := 𝟙 ((topological_space.open_nhds.map f x ⋙ topological_space.open_nhds.inclusion x).obj U), hom_inv_id' := _, inv_hom_id' := _}) _

@[simp]

theorem topological_space.open_nhds.inclusion_map_iso_hom {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

(topological_space.open_nhds.inclusion_map_iso f x).hom = 𝟙 (topological_space.open_nhds.inclusion (⇑f x) ⋙ topological_space.opens.map f)

@[simp]

theorem topological_space.open_nhds.inclusion_map_iso_inv {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

(topological_space.open_nhds.inclusion_map_iso f x).inv = 𝟙 (topological_space.open_nhds.map f x ⋙ topological_space.open_nhds.inclusion x)

@[simp]

theorem is_open_map.functor_nhds_map {X Y : Top} {f : X ⟶ Y} (h : is_open_map ⇑f) (x : ↥X) (U V : topological_space.open_nhds x) (i : U ⟶ V) :

(h.functor_nhds x).map i = h.functor.map i

def is_open_map.functor_nhds {X Y : Top} {f : X ⟶ Y} (h : is_open_map ⇑f) (x : ↥X) :

topological_space.open_nhds x ⥤ topological_space.open_nhds (⇑f x)

An open map f : X ⟶ Y induces a functor open_nhds x ⥤ open_nhds (f x).

Equations

h.functor_nhds x = {obj := λ (U : topological_space.open_nhds x), {obj := h.functor.obj U.obj, property := _}, map := λ (U V : topological_space.open_nhds x) (i : U ⟶ V), h.functor.map i, map_id' := _, map_comp' := _}

@[simp]

theorem is_open_map.functor_nhds_obj_obj {X Y : Top} {f : X ⟶ Y} (h : is_open_map ⇑f) (x : ↥X) (U : topological_space.open_nhds x) :

((h.functor_nhds x).obj U).obj = h.functor.obj U.obj

def is_open_map.adjunction_nhds {X Y : Top} {f : X ⟶ Y} (h : is_open_map ⇑f) (x : ↥X) :

h.functor_nhds x ⊣ topological_space.open_nhds.map f x

An open map f : X ⟶ Y induces an adjunction between open_nhds x and open_nhds (f x).

Equations

h.adjunction_nhds x = category_theory.adjunction.mk_of_unit_counit {unit := {app := λ (U : topological_space.open_nhds x), category_theory.hom_of_le _, naturality' := _}, counit := {app := λ (V : topological_space.open_nhds (⇑f x)), category_theory.hom_of_le _, naturality' := _}, left_triangle' := _, right_triangle' := _}