Theorems · Theorem · commutative algebra

Module.Finite.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)]
  [∀ (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)]
  [∀ (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)
  [∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)],
  (∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)) → Module.Finite R M

A module M over a semilocal ring R is finite if its localization at every maximal ideal is finite.

Defined in

Mathlib.RingTheory.LocalProperties.Semilocal

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringFiniteAddCommMonoidModuleCommSemiringAlgebraIsLocalization.AtPrimeAddCommMonoidModuleModuleIsScalarTowerIsLocalizedModule