stalkMap_hom_inv_apply — Mathlib

English

For an isomorphism e: X ≅ Y, the inverse stalk map followed by the forward stalk map equals the specialization map from X to Y.

Русский

Для изоморфизма e: X ≅ Y обратная stalkMap затем прямая stalkMap дают отображение специализации от X к Y.

LaTeX

$$$$e.inv.stalkMap \\circ e.hom.stalkMap = \\text{ specialization map }.$$$$

Lean4

@[simp]
theorem stalkMap_hom_inv_apply (e : X ≅ Y) (y : Y) (z) :
    e.inv.stalkMap y (e.hom.stalkMap (e.inv.base y) z) = Y.presheaf.stalkSpecializes (specializes_of_eq <| by simp) z :=
  DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_hom_inv e y)) z

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