Theorems · Definition · category theory

TopCat.Presheaf.stalk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasColimits C] → {X : TopCat} → TopCat.Presheaf C X → ↑X → C

The stalk of a presheaf F at a point x is calculated as the colimit of the functor nbhds x ⥤ opens F.X ⥤ C

Defined in

Mathlib.Topology.Sheaves.Stalks

Cited by

407 results in Mathlib

Foundations

Depth 37 from the axioms, rests on 252 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimits