of_isLocalization — Mathlib

English

Localization at a submonoid yields an étale map: localization of R to R_m is étale.

Русский

Локализация по подмоноиду даёт étale отображение: локализация R → R_m является étale.

LaTeX

$$$\text{IsLocalization}(M,R_m) \Rightarrow \text{FormallyEtale}(R,R_m)$$$

Lean4

theorem of_isLocalization : FormallyEtale R Rₘ :=
  FormallyEtale.iff_unramified_and_smooth.mpr
    ⟨FormallyUnramified.of_isLocalization M, FormallySmooth.of_isLocalization M⟩

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