English
If y specializes from x via h, the localization to the stalk at y composed with stalkSpecializes equals the stalk map at x composed with the localization map along h.
Русский
Если y специализируется из x через h, тогда локализация к стэку в y после stalkSpecializes равна stalkToFiber в x после локализации вдоль h.
LaTeX
$$$StructureSheaf.localizationToStalk R y \\;\\gg\\; (structureSheaf R).presheaf.stalkSpecializes(h) = (StructureSheaf.localizationToStalk R x) \\gg (CommRingCat.ofHom(PrimeSpectrum.localizationMapOfSpecializes h))$$$
Lean4
@[simp, reassoc, elementwise nosimp]
theorem localizationToStalk_stalkSpecializes {R : Type*} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) :
StructureSheaf.localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h =
CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ StructureSheaf.localizationToStalk R x :=
by
ext : 1
apply IsLocalization.ringHom_ext (S := Localization.AtPrime y.asIdeal) y.asIdeal.primeCompl
rw [CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_comp, RingHom.comp_assoc]
dsimp [localizationToStalk, PrimeSpectrum.localizationMapOfSpecializes]
rw [IsLocalization.lift_comp, IsLocalization.lift_comp, IsLocalization.lift_comp]
exact CommRingCat.hom_ext_iff.mp (toStalk_stalkSpecializes h)
