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:

source
๐Ÿ”ธ coverage
def TopologicalSpace.OpenNhds {X : TopCat} (x : โ†‘X) :
Type u

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

Instances For
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance TopologicalSpace.OpenNhds.partialOrder {X : TopCat} (x : โ†‘X) :
    PartialOrder (OpenNhds x)
    source
    ๐Ÿ“ coverage
    theorem TopologicalSpace.OpenNhds.le_def {X : TopCat} {x : โ†‘X} (U V : OpenNhds x) :
    U โ‰ค V โ†” โ†‘U โ‰ค โ†‘V
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance TopologicalSpace.OpenNhds.instLattice {X : TopCat} (x : โ†‘X) :
    Lattice (OpenNhds x)
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance TopologicalSpace.OpenNhds.instOrderTop {X : TopCat} (x : โ†‘X) :
    OrderTop (OpenNhds x)
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance TopologicalSpace.OpenNhds.instInhabited {X : TopCat} (x : โ†‘X) :
    Inhabited (OpenNhds x)
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance TopologicalSpace.OpenNhds.opensNhds.instFunLike {X : TopCat} {x : โ†‘X} {U V : OpenNhds x} :
    FunLike (U โŸถ V) โ†ฅโ†‘U โ†ฅโ†‘V
    source
    ๐Ÿ“ coverage
    @[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, โ‹ฏโŸฉ
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem TopologicalSpace.OpenNhds.val_apply {X : TopCat} {x : โ†‘X} {U V : OpenNhds x} (f : U โŸถ V) (y : โ†ฅโ†‘U) :
    โ†‘(f y) = โ†‘y
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem TopologicalSpace.OpenNhds.coe_id {X : TopCat} {x : โ†‘X} {U : OpenNhds x} (f : U โŸถ U) :
    โ‡‘f = id
    source
    ๐Ÿ“ coverage
    theorem TopologicalSpace.OpenNhds.id_apply {X : TopCat} {x : โ†‘X} {U : OpenNhds x} (f : U โŸถ U) (y : โ†ฅโ†‘U) :
    f y = y
    source
    ๐Ÿ“ coverage
    @[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โœ)
    source
    ๐Ÿ”ธ coverage
    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.

    Instances For
      source
      ๐Ÿ”ธ coverage
      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.

      Instances For
        source
        ๐Ÿ”ธ coverage
        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.

        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem TopologicalSpace.OpenNhds.inclusion_obj {X : TopCat} (x : โ†‘X) (U : Opens โ†‘X) (p : x โˆˆ U) :
          (inclusion x).obj โŸจU, pโŸฉ = U
          source
          ๐Ÿ“ coverage
          theorem TopologicalSpace.OpenNhds.isOpenEmbedding {X : TopCat} {x : โ†‘X} (U : OpenNhds x) :
          Topology.IsOpenEmbedding โ‡‘(CategoryTheory.ConcreteCategory.hom (โ†‘U).inclusion')
          source
          ๐Ÿ”ธ coverage
          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.

          Instances For
            source
            ๐Ÿ“ coverage
            @[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โŸฉ
            source
            ๐Ÿ“ coverage
            @[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
            source
            ๐Ÿ“ coverage
            @[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โŸฉ
            source
            ๐Ÿ“ coverage
            @[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
            source
            ๐Ÿ“ coverage
            @[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
            source
            ๐Ÿ”ธ coverage
            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.

            Instances For
              source
              ๐Ÿ“ coverage
              @[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โœ))
              source
              ๐Ÿ“ coverage
              @[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โœ))
              source
              ๐Ÿ“ coverage
              @[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))
              source
              ๐Ÿ“ coverage
              @[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))
              source
              ๐Ÿ”ธ coverage
              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).

              Instances For
                source
                ๐Ÿ“ coverage
                @[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
                source
                ๐Ÿ“ coverage
                @[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
                source
                ๐Ÿ”ธ coverage
                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).

                Instances For
                  source
                  ๐Ÿ”ธ coverage
                  @[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).

                  Instances For
                    source
                    ๐Ÿ”ธ coverage
                    @[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.

                    Instances For
                      source
                      ๐Ÿ”ธ coverage
                      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).

                      Instances For
                        source
                        ๐Ÿ“ coverage
                        @[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โœ
                        source
                        ๐Ÿ“ coverage
                        @[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
                        source
                        ๐Ÿ”ธ coverage
                        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.

                        Instances For