localization_unit_isIso — Mathlib

English

The canonical map from R to Localization Away(1) is an isomorphism in the category of commutative rings (since inverting 1 yields no change).

Русский

Каноническое отображение из R в Localization Away(1) является изоморфизмом в категории коммутативных колец.

LaTeX

$$$\mathrm{IsIso}\big(\text{algebraMap } R \; (\mathrm{Localization Away}(1))\big)$$$

Lean4

instance localization_unit_isIso (R : CommRingCat) :
    IsIso (CommRingCat.ofHom <| algebraMap R (Localization.Away (1 : R))) :=
  Iso.isIso_hom (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingCatIso

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