instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl

English

If S is finitely generated as an algebra over R (i.e., S is a finite R-module), then for every prime ideal P of R, the localization S localized at P is a finite module over the localization R localized at P.

Русский

Если S является конечной по модулю над R (то есть S — конечно-производимый модуль над R), то для каждого prime-идеала P кольца R локализацией S в P является конечным модулем над локализацией R в P.

LaTeX

$$$\forall \mathfrak p \in \operatorname{Spec}(R),\ S_{\mathfrak p}\ \text{ является конечным } R_{\mathfrak p}\text{-модулем.}$$$

Lean4

instance {R S : Type*} [CommRing R] {P : Ideal R} [CommRing S] [Algebra R S] [Module.Finite R S] [P.IsPrime] :
    Module.Finite (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  .of_isLocalization R S P.primeCompl

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