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.

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

    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

      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 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โœ Yโœ : C} (f : Xโœ โŸถ Yโœ) :

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

        Equations
        Instances For

          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

            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

              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
                @[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) :

                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

                  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

                    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

                        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

                          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