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) : Type u

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

Equations

• TopologicalSpace.OpenNhds x = CategoryTheory.FullSubcategory fun (U : TopologicalSpace.Opens ↑X) => x ∈ U

instance TopologicalSpace.OpenNhds.partialOrder {X : TopCat} (x : ↑X) : PartialOrder (TopologicalSpace.OpenNhds x)

Equations

• TopologicalSpace.OpenNhds.partialOrder x = PartialOrder.mk ⋯

instance TopologicalSpace.OpenNhds.instLattice {X : TopCat} (x : ↑X) : Lattice (TopologicalSpace.OpenNhds x)

Equations

• TopologicalSpace.OpenNhds.instLattice x = let __src := TopologicalSpace.OpenNhds.partialOrder x; Lattice.mk ⋯ ⋯ ⋯

instance TopologicalSpace.OpenNhds.instOrderTop {X : TopCat} (x : ↑X) : OrderTop (TopologicalSpace.OpenNhds x)

Equations

• TopologicalSpace.OpenNhds.instOrderTop x = OrderTop.mk ⋯

instance TopologicalSpace.OpenNhds.instInhabited {X : TopCat} (x : ↑X) : Inhabited (TopologicalSpace.OpenNhds x)

Equations

• TopologicalSpace.OpenNhds.instInhabited x = { default := ⊤ }

instance TopologicalSpace.OpenNhds.openNhdsCategory {X : TopCat} (x : ↑X) : CategoryTheory.Category.{u, u} (TopologicalSpace.OpenNhds x)

Equations

• TopologicalSpace.OpenNhds.openNhdsCategory x = inferInstance

instance TopologicalSpace.OpenNhds.opensNhdsHomHasCoeToFun {X : TopCat} {x : ↑X} {U : TopologicalSpace.OpenNhds x} {V : TopologicalSpace.OpenNhds x} : CoeFun (U ⟶ V) fun (x_1 : U ⟶ V) => ↥U.obj → ↥V.obj

Equations

• TopologicalSpace.OpenNhds.opensNhdsHomHasCoeToFun = { coe := fun (f : U ⟶ V) (x_1 : ↥U.obj) => ⟨↑x_1, ⋯⟩ }

def TopologicalSpace.OpenNhds.infLELeft {X : TopCat} {x : ↑X} (U : TopologicalSpace.OpenNhds x) (V : TopologicalSpace.OpenNhds x) : U ⊓ V ⟶ U

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

Equations

• U.infLELeft V = CategoryTheory.homOfLE ⋯

def TopologicalSpace.OpenNhds.infLERight {X : TopCat} {x : ↑X} (U : TopologicalSpace.OpenNhds x) (V : TopologicalSpace.OpenNhds x) : U ⊓ V ⟶ V

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

Equations

• U.infLERight V = CategoryTheory.homOfLE ⋯

def TopologicalSpace.OpenNhds.inclusion {X : TopCat} (x : ↑X) : CategoryTheory.Functor (TopologicalSpace.OpenNhds x) (TopologicalSpace.Opens ↑X)

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

Equations

• TopologicalSpace.OpenNhds.inclusion x = CategoryTheory.fullSubcategoryInclusion fun (U : TopologicalSpace.Opens ↑X) => x ∈ U

@[simp]

theorem TopologicalSpace.OpenNhds.inclusion_obj {X : TopCat} (x : ↑X) (U : TopologicalSpace.Opens ↑X) (p : x ∈ U) : (TopologicalSpace.OpenNhds.inclusion x).obj { obj := U, property := p } = U

theorem TopologicalSpace.OpenNhds.openEmbedding {X : TopCat} {x : ↑X} (U : TopologicalSpace.OpenNhds x) : OpenEmbedding ⇑U.obj.inclusion

def TopologicalSpace.OpenNhds.map {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (x : ↑X) : CategoryTheory.Functor (TopologicalSpace.OpenNhds (f x)) (TopologicalSpace.OpenNhds x)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopologicalSpace.OpenNhds.map_obj {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (x : ↑X) (U : TopologicalSpace.Opens ↑Y) (q : f x ∈ U) : (TopologicalSpace.OpenNhds.map f x).obj { obj := U, property := q } = { obj := (TopologicalSpace.Opens.map f).obj U, property := q }

@[simp]

theorem TopologicalSpace.OpenNhds.map_id_obj {X : TopCat} (x : ↑X) (U : TopologicalSpace.OpenNhds ((CategoryTheory.CategoryStruct.id X) x)) : (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).obj U = U

@[simp]

theorem TopologicalSpace.OpenNhds.map_id_obj' {X : TopCat} (x : ↑X) (U : Set ↑X) (p : IsOpen U) (q : (CategoryTheory.CategoryStruct.id X) x ∈ { carrier := U, is_open' := p }) : (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).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 : (TopologicalSpace.OpenNhds x)ᵒᵖ) : (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).obj (Opposite.unop U) = Opposite.unop U

@[simp]

theorem TopologicalSpace.OpenNhds.op_map_id_obj {X : TopCat} (x : ↑X) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) : (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).op.obj U = U

@[simp]

theorem TopologicalSpace.OpenNhds.inclusionMapIso_hom_app {X : TopCat} {Y : TopCat} (f : X✝ ⟶ Y) (x : ↑X✝) (X : TopologicalSpace.OpenNhds (f x)) : (TopologicalSpace.OpenNhds.inclusionMapIso f x).hom.app X = CategoryTheory.CategoryStruct.id ((TopologicalSpace.Opens.map f).obj ((TopologicalSpace.OpenNhds.inclusion (f x)).obj X))

@[simp]

theorem TopologicalSpace.OpenNhds.inclusionMapIso_inv_app {X : TopCat} {Y : TopCat} (f : X✝ ⟶ Y) (x : ↑X✝) (X : TopologicalSpace.OpenNhds (f x)) : (TopologicalSpace.OpenNhds.inclusionMapIso f x).inv.app X = CategoryTheory.CategoryStruct.id ((TopologicalSpace.OpenNhds.inclusion x).obj ((TopologicalSpace.OpenNhds.map f x).obj X))

def TopologicalSpace.OpenNhds.inclusionMapIso {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (x : ↑X) : (TopologicalSpace.OpenNhds.inclusion (f x)).comp (TopologicalSpace.Opens.map f) ≅ (TopologicalSpace.OpenNhds.map f x).comp (TopologicalSpace.OpenNhds.inclusion x)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopologicalSpace.OpenNhds.inclusionMapIso_hom {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (x : ↑X) : (TopologicalSpace.OpenNhds.inclusionMapIso f x).hom = CategoryTheory.CategoryStruct.id ((TopologicalSpace.OpenNhds.inclusion (f x)).comp (TopologicalSpace.Opens.map f))

@[simp]

theorem TopologicalSpace.OpenNhds.inclusionMapIso_inv {X : TopCat} {Y : TopCat} (f : X ⟶ Y) (x : ↑X) : (TopologicalSpace.OpenNhds.inclusionMapIso f x).inv = CategoryTheory.CategoryStruct.id ((TopologicalSpace.OpenNhds.map f x).comp (TopologicalSpace.OpenNhds.inclusion x))

@[simp]

theorem IsOpenMap.functorNhds_map {X : TopCat} {Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑f) (x : ↑X) : ∀ {X_1 Y_1 : TopologicalSpace.OpenNhds x} (i : X_1 ⟶ Y_1), (h.functorNhds x).map i = h.functor.map i

@[simp]

theorem IsOpenMap.functorNhds_obj_obj {X : TopCat} {Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑f) (x : ↑X) (U : TopologicalSpace.OpenNhds x) : ((h.functorNhds x).obj U).obj = h.functor.obj U.obj

def IsOpenMap.functorNhds {X : TopCat} {Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑f) (x : ↑X) : CategoryTheory.Functor (TopologicalSpace.OpenNhds x) (TopologicalSpace.OpenNhds (f x))

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

Equations

• One or more equations did not get rendered due to their size.

def IsOpenMap.adjunctionNhds {X : TopCat} {Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑f) (x : ↑X) : h.functorNhds x ⊣ TopologicalSpace.OpenNhds.map f x

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

Equations

• One or more equations did not get rendered due to their size.