Theorems · Definition · category theory

isTerminalSkyscraperSheafObjObjOfNotMem

{X : TopCat} →
  {p₀ : ↑X} →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          {A : C} →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} →
                p₀ ∉ Opposite.unop U → CategoryTheory.Limits.IsTerminal ((skyscraperSheaf p₀ A).obj.obj U)

On an open set not containing p₀, the value of skyscraper sheaf supported at p₀ is a terminal object.

Defined in

Mathlib.Topology.Sheaves.Skyscraper

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableCategoryTheory.CategoryCategoryTheory.Limits.HasTerminal