mathlib documentation

topology.category.Top.open_nhds

The category of open neighborhoods of a point #

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:

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

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

Equations
Instances for topological_space.open_nhds
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations

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

Equations

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

Equations
@[simp]
@[simp]
theorem topological_space.open_nhds.map_id_obj' {X : Top} (x : X) (U : set X) (p : is_open U) (q : (𝟙 X) x U, p⟩) :
(topological_space.open_nhds.map (𝟙 X) x).obj U, p⟩, q⟩ = U, p⟩, q⟩
@[simp]
theorem is_open_map.functor_nhds_obj_coe {X Y : Top} {f : X Y} (h : is_open_map f) (x : X) (U : topological_space.open_nhds 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) :

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

Equations

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

Equations