stalkMap_comp — Mathlib

English

For f: X ⟶ Y and x ⤳ x' (x specializes to x'), the composition of stalkSpecializes and stalkMap commutes with the base map and stalkMap.

Русский

Для f: X ⟶ Y и x ⤳ x', композиция stalkSpecializes и stalkMap удовлетворяет совместимости с базовой картой и stalkMap.

LaTeX

$$$Y.presheaf.stalkSpecializes (f.base.hom.map_specializes h) \; \gg \; f.stalkMap x = f.stalkMap x' \; \gg \; X.presheaf.stalkSpecializes h$$

Lean4

theorem stalkMap_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g : X ⟶ Z).stalkMap x = g.stalkMap (f.base x) ≫ f.stalkMap x :=
  PresheafedSpace.stalkMap.comp f.toPshHom g.toPshHom x

Похожие утверждения