stalkSpecializes_stalkMap — Mathlib

English

Given f: X ⟶ Y, x, x' with x ⤳ x', and y in the corresponding stalk, the equality of two complicated expressions reduces to the same in coordinates after applying the functorial construction.

Русский

При x ⤳ x', y в stalk, равенство двух сложных выражений сохраняется после применения конструкций.

LaTeX

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

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.toPshHom h

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