English
For any ring R, submonoid M, and point x in Spec Localization M, the stalk map induced by localization is an isomorphism.
Русский
Для кольца R, подмоноида M и точки x в Spec Localization M отображение стока от локализации является изоморфин.
LaTeX
$$$\IsIso\bigl( (\Spec.toPresheafedSpace.map (\mathrm{ofHom}(\mathrm{algebraMap}\,R\,\mathrm{Localization} M)).op).stalkMap\, x \bigr).$$$
Lean4
/-- The stalk map of `Spec M⁻¹R ⟶ Spec R` is an iso for each `p : Spec M⁻¹R`. -/
theorem Spec_map_localization_isIso (R : CommRingCat.{u}) (M : Submonoid R) (x : PrimeSpectrum (Localization M)) :
IsIso ((Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap R (Localization M))).op).stalkMap x) :=
by
dsimp only [Spec.toPresheafedSpace_map, Quiver.Hom.unop_op]
rw [← localRingHom_comp_stalkIso]
refine
IsIso.comp_isIso' inferInstance
(IsIso.comp_isIso' ?_ inferInstance)
/- I do not know why this is defeq to the goal, but I'm happy to accept that it is. -/
change
IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom
infer_instance