English
Let e: X ≅ Y be an isomorphism of schemes, y ∈ Y, and z an element of the stalk of Y at y. Then e.inv.stalkMap y (e.hom.stalkMap (e.inv.base y) z) equals the canonical stalk-congruence morphism applied to z, i.e. (Y.presheaf.stalkCongr (.of_eq (by simp))).hom z.
Русский
Пусть e: X ≅ Y — изоморфизм схем, y ∈ Y, и z элемент stalk-объекта Y в y. Тогда e.inv.stalkMap y (e.hom.stalkMap (e.inv.base y) z) равно каноническому гомоморфизму stalk, применённому к z, то есть (Y.presheaf.stalkCongr (.of_eq (by simp))).hom z.
LaTeX
$$$e.inv.stalkMap y (e.hom.stalkMap (e.inv.base y) z) = (Y.presheaf.stalkCongr (.of_eq (by simp))).hom z$$$
Lean4
@[simp]
theorem stalkMap_inv_hom_apply (e : X ≅ Y) (x : X) (y) :
e.hom.stalkMap x (e.inv.stalkMap (e.hom.base x) y) = (X.presheaf.stalkCongr (.of_eq (by simp))).hom y :=
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_inv_hom e x)) y
