Documentation

Mathlib.Topology.Sheaves.Skyscraper

Skyscraper (pre)sheaves #

A skyscraper (pre)sheaf ๐“• : (Pre)Sheaf C X is the (pre)sheaf with value A at point pโ‚€ that is supported only at open sets contain pโ‚€, i.e. ๐“•(U) = A if pโ‚€ โˆˆ U and ๐“•(U) = * if pโ‚€ โˆ‰ U where * is a terminal object of C. In terms of stalks, ๐“• is supported at all specializations of pโ‚€, i.e. if pโ‚€ โคณ x then ๐“•โ‚“ โ‰… A and if ยฌ pโ‚€ โคณ x then ๐“•โ‚“ โ‰… *.

Main definitions #

Main statements #

TODO: generalize universe level when calculating stalks, after generalizing universe level of stalk.

@[simp]
theorem skyscraperPresheaf_map {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) {U : (TopologicalSpace.Opens โ†‘X)แต’แต–} {V : (TopologicalSpace.Opens โ†‘X)แต’แต–} (i : U โŸถ V) :
(skyscraperPresheaf pโ‚€ A).map i = if h : pโ‚€ โˆˆ Opposite.unop V then CategoryTheory.eqToHom โ‹ฏ else (โ‹ฏ โ–ธ CategoryTheory.Limits.terminalIsTerminal).from ((fun (U : (TopologicalSpace.Opens โ†‘X)แต’แต–) => if pโ‚€ โˆˆ Opposite.unop U then A else โŠค_ C) U)
@[simp]
theorem skyscraperPresheaf_obj {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) (U : (TopologicalSpace.Opens โ†‘X)แต’แต–) :
(skyscraperPresheaf pโ‚€ A).obj U = if pโ‚€ โˆˆ Opposite.unop U then A else โŠค_ C
def skyscraperPresheaf {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) :

A skyscraper presheaf is a presheaf supported at a single point: if pโ‚€ โˆˆ X is a specified point, then the skyscraper presheaf ๐“• with value A is defined by U โ†ฆ A if pโ‚€ โˆˆ U and U โ†ฆ * if pโ‚€ โˆ‰ A where * is some terminal object.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem SkyscraperPresheafFunctor.map'_app {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {a : C} {b : C} (f : a โŸถ b) (U : (TopologicalSpace.Opens โ†‘X)แต’แต–) :
    (SkyscraperPresheafFunctor.map' pโ‚€ f).app U = if h : pโ‚€ โˆˆ Opposite.unop U then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom โ‹ฏ) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom โ‹ฏ)) else (โ‹ฏ โ–ธ CategoryTheory.Limits.terminalIsTerminal).from ((skyscraperPresheaf pโ‚€ a).obj U)
    def SkyscraperPresheafFunctor.map' {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {a : C} {b : C} (f : a โŸถ b) :

    Taking skyscraper presheaf at a point is functorial: c โ†ฆ skyscraper pโ‚€ c defines a functor by sending every f : a โŸถ b to the natural transformation ฮฑ defined as: ฮฑ(U) = f : a โŸถ b if pโ‚€ โˆˆ U and the unique morphism to a terminal object in C if pโ‚€ โˆ‰ U.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem skyscraperPresheafFunctor_map {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] :
      โˆ€ {X_1 Y : C} (f : X_1 โŸถ Y), (skyscraperPresheafFunctor pโ‚€).map f = SkyscraperPresheafFunctor.map' pโ‚€ f
      @[simp]
      theorem skyscraperPresheafFunctor_obj {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) :
      (skyscraperPresheafFunctor pโ‚€).obj A = skyscraperPresheaf pโ‚€ A

      Taking skyscraper presheaf at a point is functorial: c โ†ฆ skyscraper pโ‚€ c defines a functor by sending every f : a โŸถ b to the natural transformation ฮฑ defined as: ฮฑ(U) = f : a โŸถ b if pโ‚€ โˆˆ U and the unique morphism to a terminal object in C if pโ‚€ โˆ‰ U.

      Equations
      Instances For
        @[simp]
        theorem skyscraperPresheafCoconeOfSpecializes_pt {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : โ†‘X} (h : pโ‚€ โคณ y) :
        @[simp]
        theorem skyscraperPresheafCoconeOfSpecializes_ฮน_app {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : โ†‘X} (h : pโ‚€ โคณ y) (U : (TopologicalSpace.OpenNhds y)แต’แต–) :
        def skyscraperPresheafCoconeOfSpecializes {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : โ†‘X} (h : pโ‚€ โคณ y) :

        The cocone at A for the stalk functor of skyscraperPresheaf pโ‚€ A when y โˆˆ closure {pโ‚€}

        Equations
        Instances For
          noncomputable def skyscraperPresheafCoconeIsColimitOfSpecializes {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : โ†‘X} (h : pโ‚€ โคณ y) :

          The cocone at A for the stalk functor of skyscraperPresheaf pโ‚€ A when y โˆˆ closure {pโ‚€} is a colimit

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable def skyscraperPresheafStalkOfSpecializes {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : โ†‘X} (h : pโ‚€ โคณ y) :
            (skyscraperPresheaf pโ‚€ A).stalk y โ‰… A

            If y โˆˆ closure {pโ‚€}, then the stalk of skyscraperPresheaf pโ‚€ A at y is A.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem skyscraperPresheafCocone_ฮน_app {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] (y : โ†‘X) :
              @[simp]
              theorem skyscraperPresheafCocone_pt {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] (y : โ†‘X) :
              def skyscraperPresheafCocone {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] (y : โ†‘X) :

              The cocone at * for the stalk functor of skyscraperPresheaf pโ‚€ A when y โˆ‰ closure {pโ‚€}

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def skyscraperPresheafCoconeIsColimitOfNotSpecializes {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : โ†‘X} (h : ยฌpโ‚€ โคณ y) :

                The cocone at * for the stalk functor of skyscraperPresheaf pโ‚€ A when y โˆ‰ closure {pโ‚€} is a colimit

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  noncomputable def skyscraperPresheafStalkOfNotSpecializes {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : โ†‘X} (h : ยฌpโ‚€ โคณ y) :
                  (skyscraperPresheaf pโ‚€ A).stalk y โ‰… โŠค_ C

                  If y โˆ‰ closure {pโ‚€}, then the stalk of skyscraperPresheaf pโ‚€ A at y is isomorphic to a terminal object.

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

                    If y โˆ‰ closure {pโ‚€}, then the stalk of skyscraperPresheaf pโ‚€ A at y is a terminal object

                    Equations
                    Instances For
                      theorem skyscraperPresheaf_isSheaf {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] :
                      (skyscraperPresheaf pโ‚€ A).IsSheaf
                      def skyscraperSheaf {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] :

                      The skyscraper presheaf supported at pโ‚€ with value A is the sheaf that assigns A to all opens U that contain pโ‚€ and assigns * otherwise.

                      Equations
                      Instances For

                        Taking skyscraper sheaf at a point is functorial: c โ†ฆ skyscraper pโ‚€ c defines a functor by sending every f : a โŸถ b to the natural transformation ฮฑ defined as: ฮฑ(U) = f : a โŸถ b if pโ‚€ โˆˆ U and the unique morphism to a terminal object in C if pโ‚€ โˆ‰ U.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {๐“• : TopCat.Presheaf C X} {c : C} (f : ๐“•.stalk pโ‚€ โŸถ c) (U : (TopologicalSpace.Opens โ†‘X)แต’แต–) :
                          (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf pโ‚€ f).app U = if h : pโ‚€ โˆˆ Opposite.unop U then CategoryTheory.CategoryStruct.comp (๐“•.germ โŸจpโ‚€, hโŸฉ) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom โ‹ฏ)) else (โ‹ฏ โ–ธ CategoryTheory.Limits.terminalIsTerminal).from (๐“•.obj U)
                          def StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {๐“• : TopCat.Presheaf C X} {c : C} (f : ๐“•.stalk pโ‚€ โŸถ c) :
                          ๐“• โŸถ skyscraperPresheaf pโ‚€ c

                          If f : ๐“•.stalk pโ‚€ โŸถ c, then a natural transformation ๐“• โŸถ skyscraperPresheaf pโ‚€ c can be defined by: ๐“•.germ pโ‚€ โ‰ซ f : ๐“•(U) โŸถ c if pโ‚€ โˆˆ U and the unique morphism to a terminal object if pโ‚€ โˆ‰ U.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def StalkSkyscraperPresheafAdjunctionAuxs.fromStalk {X : TopCat} (pโ‚€ : โ†‘X) [(U : TopologicalSpace.Opens โ†‘X) โ†’ Decidable (pโ‚€ โˆˆ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {๐“• : TopCat.Presheaf C X} {c : C} (f : ๐“• โŸถ skyscraperPresheaf pโ‚€ c) :
                            ๐“•.stalk pโ‚€ โŸถ c

                            If f : ๐“• โŸถ skyscraperPresheaf pโ‚€ c is a natural transformation, then there is a morphism ๐“•.stalk pโ‚€ โŸถ c defined as the morphism from colimit to cocone at c.

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

                              The unit in Presheaf.stalkFunctor โŠฃ skyscraperPresheafFunctor

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

                                The counit in Presheaf.stalkFunctor โŠฃ skyscraperPresheafFunctor

                                Equations
                                Instances For

                                  skyscraperPresheafFunctor is the right adjoint of Presheaf.stalkFunctor

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

                                    Taking stalks of a sheaf is the left adjoint functor to skyscraperSheafFunctor

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • โ‹ฏ = โ‹ฏ