of_isLocalization — Mathlib

English

If S is the localization of R with respect to a multiplicative set M, then the induced Spec.map from Spec S to Spec R is a preimmersion.

Русский

Если S — локализация R по отношению к умножимому множеству M, то индуцированный отображение Spec.map: Spec S → Spec R является предиммерсией.

LaTeX

$$$[\text{IsLocalization } M \ S] \Rightarrow \operatorname{IsPreimmersion}(\operatorname{Spec.map}(\operatorname{CommRingCat.ofHom}(\text{algebraMap } R\ S)))$$$

Lean4

theorem of_isLocalization {R S : Type u} [CommRing R] (M : Submonoid R) [CommRing S] [Algebra R S]
    [IsLocalization M S] : IsPreimmersion (Spec.map (CommRingCat.ofHom <| algebraMap R S)) :=
  IsPreimmersion.mk_Spec_map (PrimeSpectrum.localization_comap_isEmbedding (R := R) S M)
    (RingHom.surjectiveOnStalks_of_isLocalization (M := M) S)

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