of_localized_maximal — Mathlib

English

A semilocal module is finite if its localized components at maximal ideals are finite.

Русский

Полусемилокальный модуль конечно порожден, если локализованные компоненты по максимумам конечны.

LaTeX

$$$N.FG$ corresponds to finite localized pieces; hence finite overall.$$

Lean4

theorem of_localized_maximal
    (H : ∀ (P : Ideal R) [P.IsMaximal], Module.Finite (Localization P.primeCompl) (LocalizedModule P.primeCompl M)) :
    Module.Finite R M :=
  .of_isLocalized_maximal M _ _ (fun _ _ ↦ LocalizedModule.mkLinearMap _ _) H

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