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₀ V.unop then CategoryTheory.eqToHom (_ : (fun U => if p₀ U.unop then A else ⊤_ C) U = (fun U => if p₀ U.unop then A else ⊤_ C) V) else CategoryTheory.Limits.IsTerminal.from ((_ : (⊤_ C) = if p₀ V.unop then A else ⊤_ C)CategoryTheory.Limits.terminalIsTerminal) ((fun U => if p₀ U.unop 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₀ U.unop then A else ⊤_ 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.

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₀ U.unop then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (if p₀ U.unop then a else ⊤_ C) = a)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom (_ : b = if p₀ U.unop then b else ⊤_ C))) else CategoryTheory.Limits.IsTerminal.from ((_ : (⊤_ C) = if p₀ U.unop then b else ⊤_ C)CategoryTheory.Limits.terminalIsTerminal) ((skyscraperPresheaf p₀ a).obj U)

    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.

    Instances For
      @[simp]

      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.

      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)ᵒᵖ) :
        (skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U = CategoryTheory.eqToHom (_ : (if p₀ U.unop.obj.carrier then A else ⊤_ C) = A)

        The cocone at A for the stalk functor of skyscraper_presheaf p₀ A when y ∈ closure {p₀}

        Instances For

          The cocone at A for the stalk functor of skyscraper_presheaf p₀ A when y ∈ closure {p₀} is a colimit

          Instances For

            If y ∈ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is A.

            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 skyscraper_presheaf p₀ A when y ∉ closure {p₀}

              Instances For

                The cocone at * for the stalk functor of skyscraper_presheaf p₀ A when y ∉ closure {p₀} is a colimit

                Instances For

                  If y ∉ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is isomorphic to a terminal object.

                  Instances For

                    If y ∉ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is a terminal object

                    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.

                      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.

                        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 : TopCat.Presheaf.stalk 𝓕 p₀ c) (U : (TopologicalSpace.Opens X)ᵒᵖ) :
                          (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f).app U = if h : p₀ U.unop then CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ 𝓕 { val := p₀, property := h }) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom (_ : c = if p₀ U.unop then c else ⊤_ C))) else CategoryTheory.Limits.IsTerminal.from ((_ : (⊤_ C) = if p₀ U.unop then c else ⊤_ C)CategoryTheory.Limits.terminalIsTerminal) (𝓕.obj U)

                          If f : 𝓕.stalk p₀ ⟶ c, then a natural transformation 𝓕 ⟶ skyscraper_presheaf 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.

                          Instances For

                            If f : 𝓕 ⟶ skyscraper_presheaf p₀ c is a natural transformation, then there is a morphism 𝓕.stalk p₀ ⟶ c defined as the morphism from colimit to cocone at c.

                            Instances For

                              skyscraper_presheaf_functor is the right adjoint of presheaf.stalk_functor

                              Instances For

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

                                Instances For