Spec_map_localization_isIso — Mathlib

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

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