English
Let e: X ≅ Y be an isomorphism of schemes and x ∈ X. Then the composition e.inv.stalkMap (e.hom.base x) ≫ e.hom.stalkMap x equals the canonical stalk-congruence morphism (X.presheaf.stalkCongr (.of_eq (by simp))).hom, expressing the compatibility of stalk maps with the inverse and forward maps of the isomorphism.
Русский
Пусть e: X ≅ Y — изоморфизм схем, и x ∈ X. Тогда композиция e.inv.stalkMap (e.hom.base x) ≫ e.hom.stalkMap x равна каноническому гомоморфизму stalk-конгруэнции (X.presheaf.stalkCongr (.of_eq (by simp))).hom, выражая совместимость stalkMap с обратным и прямым отображениями изоморфизма.
LaTeX
$$$e.inv.stalkMap (e.hom.base x) \\;\\gg\\; e.hom.stalkMap x = (X.presheaf.stalkCongr (.of_eq (by \\simp))).hom$$$
Lean4
@[reassoc (attr := simp)]
theorem stalkMap_inv_hom (e : X ≅ Y) (x : X) :
e.inv.stalkMap (e.hom.base x) ≫ e.hom.stalkMap x = (X.presheaf.stalkCongr (.of_eq (by simp))).hom :=
LocallyRingedSpace.stalkMap_inv_hom (forgetToLocallyRingedSpace.mapIso e) x
