# Documentation

Mathlib.Topology.Category.TopCat.OpenNhds

# The category of open neighborhoods of a point #

Given an object X of the category TopCat of topological spaces and a point x : X, this file builds the type OpenNhds 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 OpenNhds x.

## Main declarations

Besides OpenNhds, the main constructions here are:

• inclusion (x : X): the obvious functor OpenNhds x ⥤ Opens X
• functorNhds: An open map f : X ⟶ Y induces a functor OpenNhds x ⥤ OpenNhds (f x)
• adjunctionNhds: An open map f : X ⟶ Y induces an adjunction between OpenNhds x and OpenNhds (f x).
def TopologicalSpace.OpenNhds {X : TopCat} (x : X) :

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

Instances For
instance TopologicalSpace.OpenNhds.opensNhdsHomHasCoeToFun {X : TopCat} {x : X} {U : } {V : } :
CoeFun (U V) fun x => { x // x U.obj }{ x // x V.obj }
def TopologicalSpace.OpenNhds.infLELeft {X : TopCat} {x : X} (U : ) (V : ) :
U V U

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

Instances For
def TopologicalSpace.OpenNhds.infLERight {X : TopCat} {x : X} (U : ) (V : ) :
U V V

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

Instances For

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

Instances For
@[simp]
theorem TopologicalSpace.OpenNhds.inclusion_obj {X : TopCat} (x : X) (U : ) (p : x U) :
().obj { obj := U, property := p } = U
theorem TopologicalSpace.OpenNhds.openEmbedding {X : TopCat} {x : X} (U : ) :
def TopologicalSpace.OpenNhds.map {X : TopCat} {Y : TopCat} (f : X Y) (x : X) :

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

Instances For
@[simp]
theorem TopologicalSpace.OpenNhds.map_obj {X : TopCat} {Y : TopCat} (f : X Y) (x : X) (U : ) (q : f x U) :
().obj { obj := U, property := q } = { obj := ().obj U, property := q }
@[simp]
theorem TopologicalSpace.OpenNhds.map_id_obj {X : TopCat} (x : X) (U : ) :
= U
@[simp]
theorem TopologicalSpace.OpenNhds.map_id_obj' {X : TopCat} (x : X) (U : Set X) (p : ) (q : { carrier := U, is_open' := p }) :
().obj { obj := { carrier := U, is_open' := p }, property := q } = { obj := { carrier := U, is_open' := p }, property := q }
@[simp]
theorem TopologicalSpace.OpenNhds.map_id_obj_unop {X : TopCat} (x : X) (U : ) :
().obj U.unop = U.unop
@[simp]
theorem TopologicalSpace.OpenNhds.op_map_id_obj {X : TopCat} (x : X) (U : ) :
.obj U = U
def TopologicalSpace.OpenNhds.inclusionMapIso {X : TopCat} {Y : TopCat} (f : X Y) (x : X) :

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

Instances For
@[simp]
theorem TopologicalSpace.OpenNhds.inclusionMapIso_hom {X : TopCat} {Y : TopCat} (f : X Y) (x : X) :
@[simp]
theorem TopologicalSpace.OpenNhds.inclusionMapIso_inv {X : TopCat} {Y : TopCat} (f : X Y) (x : X) :
@[simp]
theorem IsOpenMap.functorNhds_obj_obj {X : TopCat} {Y : TopCat} {f : X Y} (h : ) (x : X) (U : ) :
(().obj U).obj = ().obj U.obj
@[simp]
theorem IsOpenMap.functorNhds_map {X : TopCat} {Y : TopCat} {f : X Y} (h : ) (x : X) :
∀ {X Y : } (i : X Y), ().map i = ().map i
def IsOpenMap.functorNhds {X : TopCat} {Y : TopCat} {f : X Y} (h : ) (x : X) :

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

Instances For
def IsOpenMap.adjunctionNhds {X : TopCat} {Y : TopCat} {f : X Y} (h : ) (x : X) :

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

Instances For