Theorems · Definition · category theory

skyscraperPresheafFunctor

{X : TopCat} →
  (p₀ : ↑X) →
    [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst : CategoryTheory.Category.{w, v} C] →
          [CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Functor C (TopCat.Presheaf C X)

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.

Defined in

Mathlib.Topology.Sheaves.Skyscraper

Cited by

4 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableCategoryTheory.CategoryCategoryTheory.Limits.HasTerminal