finitePresentation_holdsForLocalizationAway

English

Localization at a single element (Away) preserves finite presentation: the localized ring obtained by inverting that element remains finitely presented over the localized base.

Русский

Локализация по одному элементу, инвертирующему его, сохраняет конечнопредставление: полученное локализованное кольцо остается конечнопредставленным над локализованной базой.

LaTeX

$$$\text{Away localization preserves finite presentation:}$ if $f$ is the localization map at a single element, then $f$-target is FP over the base.$$

Lean4

/-- If `R` is a ring, then `Rᵣ` is `R`-finitely-presented for any `r : R`. -/
theorem finitePresentation_holdsForLocalizationAway : HoldsForLocalizationAway @FinitePresentation :=
  by
  introv R _
  rw [finitePresentation_algebraMap]
  exact IsLocalization.Away.finitePresentation r

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