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:

@[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

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

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 {carrier := U, is_open' := p}) :
@[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
@[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) :

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

Equations