holdsForLocalizationAway — Mathlib

English

Localization away preserves the formally unramified property: if f: R → S is formally unramified, then the localization away map Localization.awayMap f r is also formally unramified for any r ∈ R.

Русский

Локализация away сохраняет свойство формально немрамированности: если f: R→S формально немрамирован, то Localization.awayMap f r также формально немрамирован для любого r ∈ R.

LaTeX

$$$\\forall R,S,f,r,\\ \\mathrm{IsLocalization.Away}\\ r\\,\\mathcal R'\\quad\\Rightarrow\\quad \\mathrm{FrmUnramified}(\\mathrm{Localization.awayMap}\\, f\\, r)$$$

Lean4

theorem holdsForLocalizationAway : HoldsForLocalizationAway FormallyUnramified :=
  by
  intro R S _ _ _ r _
  rw [formallyUnramified_algebraMap]
  exact .of_isLocalization (.powers r)

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