of_isLocalization_Away — Mathlib

English

If r ∈ R and A is unramified over R, then the localization Away r preserves unramifiedness.

Русский

Если r ∈ R и A неразветвлено над R, локализация Away r сохраняет неразветвленность.

LaTeX

$$$[\text{Unramified } R A] \Rightarrow [\text{Unramified } R A_{(r)}]$$$

Lean4

/-- Localization at an element is unramified. -/
theorem of_isLocalization_Away (r : R) [IsLocalization.Away r A] : Unramified R A
    where
  formallyUnramified := Algebra.FormallyUnramified.of_isLocalization (Submonoid.powers r)
  finiteType :=
    haveI : FinitePresentation R A := IsLocalization.Away.finitePresentation r
    inferInstance

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