English
For every x on the spectrum, the localized module to Stalk provides an IsLocalizedModule structure with the stalk map to the localization.
Русский
Для каждого x на спектре задана структура IsLocalizedModule для stalk с картой локализации.
LaTeX
$$IsLocalizedModule \\ x.asIdeal.primeCompl (toStalk M x).hom$$
Lean4
instance (x : PrimeSpectrum.Top R) : IsLocalizedModule x.asIdeal.primeCompl (toStalk M x).hom :=
by
convert
IsLocalizedModule.of_linearEquiv (hf := localizedModuleIsLocalizedModule (M := M) x.asIdeal.primeCompl) (e :=
(stalkIso M x).symm.toLinearEquiv)
ext
simp only [of_coe, show (stalkIso M x).symm.toLinearEquiv.toLinearMap = (stalkIso M x).inv.hom by rfl]
erw [LocalizedModule.lift_comp]