def
Top.presheaf.stalk_functor
(C : Type u)
[𝒞 : category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top} :
↥X → Top.presheaf C X ⥤ C
Stalks are functorial with respect to morphisms of presheaves over a fixed X.
def
Top.presheaf.stalk
{C : Type u}
[𝒞 : category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top} :
Top.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
Equations
- ℱ.stalk x = (Top.presheaf.stalk_functor C x).obj ℱ
@[simp]
theorem
Top.presheaf.stalk_functor_obj
{C : Type u}
[𝒞 : category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(ℱ : Top.presheaf C X)
(x : ↥X) :
(Top.presheaf.stalk_functor C x).obj ℱ = ℱ.stalk x
def
Top.presheaf.stalk_pushforward
(C : Type u)
[𝒞 : category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C X)
(x : ↥X) :
Equations
- Top.presheaf.stalk_pushforward C f ℱ x = category_theory.limits.colim.map (category_theory.whisker_right (category_theory.nat_trans.op (topological_space.open_nhds.inclusion_map_iso f x).inv) ℱ) ≫ category_theory.limits.colimit.pre (((category_theory.whiskering_left (topological_space.open_nhds x)ᵒᵖ (topological_space.opens ↥X)ᵒᵖ C).obj (topological_space.open_nhds.inclusion x).op).obj ℱ) (topological_space.open_nhds.map f x).op
@[simp]
theorem
Top.presheaf.stalk_pushforward.id
(C : Type u)
[𝒞 : category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(ℱ : Top.presheaf C X)
(x : ↥X) :
Top.presheaf.stalk_pushforward C (𝟙 X) ℱ x = (Top.presheaf.stalk_functor C x).map (Top.presheaf.pushforward.id ℱ).hom
@[simp]
theorem
Top.presheaf.stalk_pushforward.comp
(C : Type u)
[𝒞 : category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y Z : Top}
(ℱ : Top.presheaf C X)
(f : X ⟶ Y)
(g : Y ⟶ Z)
(x : ↥X) :
Top.presheaf.stalk_pushforward C (f ≫ g) ℱ x = Top.presheaf.stalk_pushforward C g (f _* ℱ) (⇑f x) ≫ Top.presheaf.stalk_pushforward C f ℱ x