Theorems · Definition · category theory

TopCat.Presheaf.stalkSpecializes

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X : TopCat} → (F : TopCat.Presheaf C X) → {x y : ↑X} → x ⤳ y → (F.stalk y ⟶ F.stalk x)

If x specializes to y, then there is a natural map F.stalk y ⟶ F.stalk x.

Defined in

Mathlib.Topology.Sheaves.Stalks

Cited by

51 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimits