mathlib documentation

algebraic_geometry.stalks

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 : ↥X) :

C

The stalk at x of a PresheafedSpace.

Equations

X.stalk x = X.presheaf.stalk x

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) :

Y.stalk (⇑(α.base) x) ⟶ X.stalk x

A morphism of presheafed spaces induces a morphism of stalks.

Equations

algebraic_geometry.PresheafedSpace.stalk_map α x = (Top.presheaf.stalk_functor C (⇑(α.base) x)).map α.c ≫ Top.presheaf.stalk_pushforward C α.base X.presheaf 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) :

algebraic_geometry.PresheafedSpace.stalk_map (α ≫ β) x = algebraic_geometry.PresheafedSpace.stalk_map β (⇑(α.base) x) ≫ algebraic_geometry.PresheafedSpace.stalk_map α x