isIso_toBasicOpen — Mathlib

English

The composition localizationToStalk ≫ stalkToFiberRingHom is the identity on the stalk, reflecting the adjunction of localization and stalk.

Русский

Компоновка localizationToStalk ≫ stalkToFiberRingHom является тождением на stalk.

LaTeX

$$$stalkToFiberRingHom\\_localizationToStalk (x) = \\mathrm{Id}$$$

Lean4

instance isIso_toBasicOpen (f : R) : IsIso (CommRingCat.ofHom (toBasicOpen R f)) :=
  haveI : IsIso ((forget CommRingCat).map (CommRingCat.ofHom (toBasicOpen R f))) :=
    (isIso_iff_bijective _).mpr ⟨toBasicOpen_injective R f, toBasicOpen_surjective R f⟩
  isIso_of_reflects_iso _ (forget CommRingCat)

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