of_isLocalization — Mathlib

English

If S is a localization of R with respect to a multiplicative set M, and S is unramified over R, then the localized extension R → S is unramified.

Русский

Если S является локализацией R по множеству M и S неразветвлено над R, то локализация сохраняет неразветвленность.

LaTeX

$$$[\text{IsLocalization } M \; R' ] \Rightarrow [\text{Unramified } R \; R']$$$

Lean4

/-- This holds in general for epimorphisms. -/
theorem of_isLocalization [IsLocalization M Rₘ] : FormallyUnramified R Rₘ :=
  by
  rw [iff_comp_injective]
  intro Q _ _ I _ f₁ f₂ _
  apply AlgHom.coe_ringHom_injective
  refine IsLocalization.ringHom_ext M ?_
  ext
  simp

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