stalkSpecializes_stalkMap_apply — Mathlib

English

If f = g, then the stalk maps at a given point are related by a canonical conjugation via the stalkCongr isomorphism.

Русский

Если f = g, то stalkMap на точке связаны канонической конъигурацией через stalkCongr.

LaTeX

$$f.stalkMap x = (Y.presheaf.stalkCongr (.of_eq h)).hom ≫ g.stalkMap x$$

Lean4

theorem stalkSpecializes_stalkMap_apply (x x' : X) (h : x ⤳ x') (y) :
    f.stalkMap x (Y.presheaf.stalkSpecializes (f.base.hom.map_specializes h) y) =
      (X.presheaf.stalkSpecializes h (f.stalkMap x' y)) :=
  DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkSpecializes_stalkMap f x x' h)) y

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