stalkSpecializes_stalkMap — Mathlib

English

The specialization relation between points is compatible with stalk maps: composing a stalk specialization with a stalk map equals the corresponding stalk map after applying the specialization to the domain.

Русский

Специализация между точками совместима с stalk‑переходами: композиция stalkSpecializes с stalkMap равна stalkMap после применения специализации к области определения.

LaTeX

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

Lean4

@[reassoc]
theorem stalkSpecializes_stalkMap (x x' : X) (h : x ⤳ x') :
    Y.presheaf.stalkSpecializes (f.base.hom.map_specializes h) ≫ f.stalkMap x =
      f.stalkMap x' ≫ X.presheaf.stalkSpecializes h :=
  PresheafedSpace.stalkMap.stalkSpecializes_stalkMap f.toShHom h

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