finitePresentation — Mathlib

English

If S is the away localization of R at r, then S has a finite presentation as an R-algebra.

Русский

Если S — away-локализация R в точке r, то S имеет конечную презентацию как R-алгебра.

LaTeX

$$Algebra.FinitePresentation R S$$

Lean4

theorem finitePresentation (r : R) {S} [CommRing S] [Algebra R S] [IsLocalization.Away r S] :
    Algebra.FinitePresentation R S :=
  (AdjoinRoot.finitePresentation _).equiv <|
    (Localization.awayEquivAdjoin r).symm.trans <| IsLocalization.algEquiv (Submonoid.powers r) _ _

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