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 = { U : TopologicalSpace.Opens ↑X // x ∈ U }

@[implicit_reducible]

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

Equations

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

theorem TopologicalSpace.OpenNhds.le_def {X : TopCat} {x : ↑X} (U V : OpenNhds x) : U ≤ V ↔ ↑U ≤ ↑V

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• TopologicalSpace.OpenNhds.instOrderTop x = { top := ⟨⊤, trivial⟩, le_top := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance TopologicalSpace.OpenNhds.opensNhds.instFunLike {X : TopCat} {x : ↑X} {U V : OpenNhds x} : FunLike (U ⟶ V) ↥↑U ↥↑V

Equations

• TopologicalSpace.OpenNhds.opensNhds.instFunLike = { coe := fun (f : U ⟶ V) => Set.inclusion ⋯, coe_injective' := ⋯ }

@[simp]

theorem TopologicalSpace.OpenNhds.apply_mk {X : TopCat} {x : ↑X} {U V : OpenNhds x} (f : U ⟶ V) (y : ↑X) (hy : y ∈ ↑U) : f ⟨y, hy⟩ = ⟨y, ⋯⟩

@[simp]

theorem TopologicalSpace.OpenNhds.val_apply {X : TopCat} {x : ↑X} {U V : OpenNhds x} (f : U ⟶ V) (y : ↥↑U) : ↑(f y) = ↑y

@[simp]

theorem TopologicalSpace.OpenNhds.coe_id {X : TopCat} {x : ↑X} {U : OpenNhds x} (f : U ⟶ U) : ⇑f = id

theorem TopologicalSpace.OpenNhds.id_apply {X : TopCat} {x : ↑X} {U : OpenNhds x} (f : U ⟶ U) (y : ↥↑U) : f y = y

@[simp]

theorem TopologicalSpace.OpenNhds.comp_apply {X : TopCat} {x : ↑X} {U V W : OpenNhds x} (f : U ⟶ V) (g : V ⟶ W) (x✝ : ↥↑U) : (CategoryTheory.CategoryStruct.comp f g) x✝ = g (f x✝)

def TopologicalSpace.OpenNhds.infLELeft {X : TopCat} {x : ↑X} (U V : 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 V : 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 (OpenNhds x) (Opens ↑X)

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

Equations

• TopologicalSpace.OpenNhds.inclusion x = ⋯.functor

@[simp]

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

theorem TopologicalSpace.OpenNhds.isOpenEmbedding {X : TopCat} {x : ↑X} (U : OpenNhds x) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (↑U).inclusion')

def TopologicalSpace.OpenNhds.map {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) : CategoryTheory.Functor (OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x)) (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 Y : TopCat} (f : X ⟶ Y) (x : ↑X) (U : Opens ↑Y) (q : (CategoryTheory.ConcreteCategory.hom f) x ∈ U) : (map f x).obj ⟨U, q⟩ = ⟨(Opens.map f).obj U, q⟩

@[simp]

theorem TopologicalSpace.OpenNhds.map_id_obj {X : TopCat} (x : ↑X) (U : OpenNhds ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x)) : (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.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x ∈ { carrier := U, is_open' := p }) : (map (CategoryTheory.CategoryStruct.id X) x).obj ⟨{ carrier := U, is_open' := p }, q⟩ = ⟨{ carrier := U, is_open' := p }, q⟩

@[simp]

theorem TopologicalSpace.OpenNhds.map_id_obj_unop {X : TopCat} (x : ↑X) (U : (OpenNhds x)ᵒᵖ) : (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 : (OpenNhds x)ᵒᵖ) : (map (CategoryTheory.CategoryStruct.id X) x).op.obj U = U

def TopologicalSpace.OpenNhds.inclusionMapIso {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) : (inclusion ((CategoryTheory.ConcreteCategory.hom f) x)).comp (Opens.map f) ≅ (map f x).comp (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_inv_app {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) (X✝ : OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x)) : (inclusionMapIso f x).inv.app X✝ = CategoryTheory.CategoryStruct.id ((inclusion x).obj ((map f x).obj X✝))

@[simp]

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

@[simp]

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

@[simp]

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

def IsOpenMap.functorNhds {X Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) : CategoryTheory.Functor (TopologicalSpace.OpenNhds x) (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom 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.

@[simp]

theorem IsOpenMap.functorNhds_map {X Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) {X✝ Y✝ : TopologicalSpace.OpenNhds x} (i : X✝ ⟶ Y✝) : (h.functorNhds x).map i = h.functor.map i

@[simp]

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

def IsOpenMap.adjunctionNhds {X Y : TopCat} {f : X ⟶ Y} (h : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom 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.

@[reducible, inline]

abbrev Topology.IsOpenEmbedding.functorNhds {X Y : TopCat} {f : X ⟶ Y} (h : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) : CategoryTheory.Functor (TopologicalSpace.OpenNhds x) (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x))

An open embedding f : X ⟶ Y induces a functor OpenNhds x ⥤ OpenNhds (f x). We define IsOpenEmbedding.functorNhds as IsOpenEmbedding.isOpenMap.functorNds, so it won't default to IsInducing.functorNhds (which is equal but not defeq).

Equations

• h.functorNhds x = ⋯.functorNhds x

@[reducible, inline]

abbrev Topology.IsOpenEmbedding.adjunctionNhds {X Y : TopCat} {f : X ⟶ Y} (h : IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) : ⋯.functorNhds x ⊣ TopologicalSpace.OpenNhds.map f x

An open embedding f : X ⟶ Y induces an adjunction between OpenNhds x and OpenNhds (f x). We define IsOpenEmbedding.adjunctionNhds as IsOpenEmbedding.isOpenMap.adjunctionNds, so it won't default to IsInducing.adjunctionNhds, which is an adjunction in the other direction.

Equations

• h.adjunctionNhds x = ⋯.adjunctionNhds x

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

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

Equations

• h.functorNhds x = { obj := fun (U : TopologicalSpace.OpenNhds x) => ⟨h.functor.obj ↑U, ⋯⟩, map := fun {X_1 Y_1 : TopologicalSpace.OpenNhds x} => h.functor.map, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Topology.IsInducing.functorNhds_obj_coe {X Y : TopCat} {f : X ⟶ Y} (h : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) (U : TopologicalSpace.OpenNhds x) : ↑((h.functorNhds x).obj U) = h.functor.obj ↑U

@[simp]

theorem Topology.IsInducing.functorNhds_map {X Y : TopCat} {f : X ⟶ Y} (h : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) {X✝ Y✝ : TopologicalSpace.OpenNhds x} (a✝ : (fun (a : { U : TopologicalSpace.Opens ↑X // x ∈ U }) => ↑a) X✝ ⟶ (fun (a : { U : TopologicalSpace.Opens ↑X // x ∈ U }) => ↑a) Y✝) : (h.functorNhds x).map a✝ = h.functor.map a✝

def Topology.IsInducing.adjunctionNhds {X Y : TopCat} {f : X ⟶ Y} (h : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) : TopologicalSpace.OpenNhds.map f x ⊣ h.functorNhds x

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

Equations

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