of_isIso — Mathlib

English

If f is such that R → S is a localization (Away), then Spec.map (ofHom (algebraMap R S)) is an open immersion.

Русский

Если S — локализация от R вдоль Away, то Spec.map (algebraMap R S) образует открытое вложение.

LaTeX

$$$$ IsOpenImmersion( \operatorname{Spec.map}(\operatorname{ofHom}(\text{algebraMap } R S)) ) $$$$

Lean4

instance (priority := 100) of_isIso [IsIso g] : IsOpenImmersion g :=
  LocallyRingedSpace.IsOpenImmersion.of_isIso _

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