Theorems · Definition · category theory

skyscraperPresheaf

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

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.

Defined in

Mathlib.Topology.Sheaves.Skyscraper

Cited by

23 results in Mathlib

Foundations

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

Assumes

DecidableCategoryTheory.CategoryCategoryTheory.Limits.HasTerminal