English
Let e: X ≅ Y be an isomorphism of schemes and y ∈ Y. Then the composite map on stalks e.hom.stalkMap (e.inv.base y) ≫ e.inv.stalkMap y equals the canonical stalk-congruence morphism on Y at y, i.e. the hom part of Y.presheaf.stalkCongr induced by the equality e.inv.base y = y.
Русский
Пусть e: X ≅ Y — изоморфизм схем, и y ∈ Y. Тогда композиция на stalk-объектах e.hom.stalkMap (e.inv.base y) затем e.inv.stalkMap y равна каноническому гомоморфизму конгруэнций stalk для Y в точке y, то есть гомоморфности stalkCongr, индуцированной равенству e.inv.base y = y.
LaTeX
$$$e.hom.stalkMap (e.inv.base\, y) \\;\\gg\\; e.inv.stalkMap\\, y = (Y.presheaf.stalkCongr (.of_eq (by\\simp))).hom$$$
Lean4
@[reassoc (attr := simp)]
theorem stalkMap_hom_inv (e : X ≅ Y) (y : Y) :
e.hom.stalkMap (e.inv.base y) ≫ e.inv.stalkMap y = (Y.presheaf.stalkCongr (.of_eq (by simp))).hom :=
LocallyRingedSpace.stalkMap_hom_inv (forgetToLocallyRingedSpace.mapIso e) y
