Stalks for presheaved spaces
This file lifts constructions of stalks and pushforwards of stalks to work with the category of presheafed spaces.
def
algebraic_geometry.PresheafedSpace.stalk
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
(X : algebraic_geometry.PresheafedSpace C) :
↥X → C
def
algebraic_geometry.PresheafedSpace.stalk_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : algebraic_geometry.PresheafedSpace C}
(α : X ⟶ Y)
(x : ↥X) :
Equations
- algebraic_geometry.PresheafedSpace.stalk_map α x = (Top.presheaf.stalk_functor C (⇑(α.base) x)).map α.c ≫ Top.presheaf.stalk_pushforward C α.base X.𝒪 x
@[simp]
theorem
algebraic_geometry.PresheafedSpace.stalk_map.id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
(X : algebraic_geometry.PresheafedSpace C)
(x : ↥X) :
algebraic_geometry.PresheafedSpace.stalk_map (𝟙 X) x = 𝟙 (X.stalk x)
@[simp]
theorem
algebraic_geometry.PresheafedSpace.stalk_map.comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y Z : algebraic_geometry.PresheafedSpace C}
(α : X ⟶ Y)
(β : Y ⟶ Z)
(x : ↥X) :