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.

Equations
Instances For
    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.objV.obj
    Equations
    • TopologicalSpace.OpenNhds.opensNhdsHomHasCoeToFun = { coe := fun (f : U V) (x_1 : U.obj) => x_1, }

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

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        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.

          Equations
          • One or more equations did not get rendered due to their size.
          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.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[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

              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.
              Instances For
                def IsOpenMap.adjunctionNhds {X : TopCat} {Y : TopCat} {f : X Y} (h : IsOpenMap f) (x : 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.
                Instances For