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:

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 : TopologicalSpace.OpenNhds x} {V : TopologicalSpace.OpenNhds x} :
    CoeFun (U V) fun x => { x // x U.obj }{ x // x V.obj }

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

    Instances For

      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 : TopologicalSpace.Opens X) (p : x U) :
          (TopologicalSpace.OpenNhds.inclusion x).obj { obj := U, property := p } = U

          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 : 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 : 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 }

            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 IsOpenMap.functorNhds_obj_obj {X : TopCat} {Y : TopCat} {f : X Y} (h : IsOpenMap f) (x : X) (U : TopologicalSpace.OpenNhds x) :
              ((IsOpenMap.functorNhds h x).obj U).obj = (IsOpenMap.functor h).obj U.obj
              @[simp]
              theorem IsOpenMap.functorNhds_map {X : TopCat} {Y : TopCat} {f : X Y} (h : IsOpenMap f) (x : X) :
              ∀ {X Y : TopologicalSpace.OpenNhds x} (i : X Y), (IsOpenMap.functorNhds h x).map i = (IsOpenMap.functor h).map i

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

              Instances For

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

                Instances For