instIsOpenImmersionMapOfHomAwayAlgebraMap

English

If R is a commutative ring and f ∈ R, then Spec map from the localization away f is an open immersion: Spec map (ofHom (algebraMap R (Localization.Away f))).

Русский

Если R — коммутативное кольцо и f ∈ R, то отображение Spec локализации Away f является открытым вложением.

LaTeX

$$$$ \operatorname{Spec}(R) \to \operatorname{Spec}(R_f) \text{ is an open immersion} $$$$

Lean4

instance {R} [CommRing R] (f : R) :
    IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))) :=
  basic_open_isOpenImmersion (R := .of R) f

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