Theorems · Theorem · commutative algebra

Submodule.fg_of_isLocalized_maximal

∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] {M : Type u_2} [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3)
  [inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_5 : (P : Ideal R) → [inst_5 : P.IsMaximal] → Algebra R (Rₚ P)]
  [inst_6 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst_8 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_11 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_11 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M),
  (∀ (P : Ideal R) [inst_12 : P.IsMaximal], (Submodule.localized' (Rₚ P) P.primeCompl (f P) N).FG) → N.FG

A submodule N of a module M over a semilocal ring R is finitely generated if its localization at every maximal ideal is finitely generated.

Defined in

Mathlib.RingTheory.LocalProperties.Semilocal

Cited by

2 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFiniteAddCommMonoidModuleCommSemiringAlgebraIsLocalization.AtPrimeAddCommMonoidModuleModuleIsScalarTowerIsLocalizedModule