English
Let e: X ≅ Y be an isomorphism of schemes, y ∈ Y, and z an element in the stalk of Y at y. Then e.inv.stalkMap y acts on e.hom.stalkMap (e.inv.base y) applied to z to give the canonical stalk-congruence image of z, i.e. (Y.presheaf.stalkCongr (.of_eq (by simp))).hom z.
Русский
Пусть e: X ≅ Y — изоморфизм схем, y ∈ Y, и z элемент локального стэка (столба) Y в точке y. Тогда действие e.inv.stalkMap y на e.hom.stalkMap (e.inv.base y) примененное к z дает каноническое изображение z через stalkCongr, то есть (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_hom_inv_apply (e : X ≅ Y) (y : Y) (z) :
e.inv.stalkMap y (e.hom.stalkMap (e.inv.base y) z) = (Y.presheaf.stalkCongr (.of_eq (by simp))).hom z :=
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_hom_inv e y)) z
