instIsLocalizedModuleCarrierOfStalkTildeInModuleCatPrimeComplAsIdealHomToStalk

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]

Похожие утверждения