Local properties for semilocal rings

This file proves some local properties for a semilocal ring R (a ring with finitely many maximal ideals).

Main results

• Module.Finite.of_isLocalized_maximal: A module M over a semilocal ring R is finite if its localization at every maximal ideal is finite.
• IsNoetherianRing.of_isLocalization_maximal: A semilocal ring R is Noetherian if its localization at every maximal ideal is a Noetherian ring.
• isPrincipalIdealRing_of_isPrincipalIdealRing_isLocalization_maximal: A semilocal integral domain A is a PID if its localization at every maximal ideal is a PID.

theorem Module.Finite.of_isLocalized_maximal {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [AddCommMonoid M] [Module R M] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3) [(P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (H : ∀ (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.

theorem Submodule.fg_of_isLocalized_maximal {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] {M : Type u_2} [AddCommMonoid M] [Module R M] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3) [(P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M) (H : ∀ (P : Ideal R) [inst : P.IsMaximal], (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.

theorem Module.Finite.of_localized_maximal {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] (M : Type u_2) [AddCommMonoid M] [Module R M] (H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Localization P.primeCompl) (LocalizedModule P.primeCompl M)) : Module.Finite R M

theorem Submodule.fg_of_localized_maximal {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] {M : Type u_2} [AddCommMonoid M] [Module R M] (N : Submodule R M) (H : ∀ (P : Ideal R) [inst : P.IsMaximal], (localized P.primeCompl N).FG) : N.FG

theorem IsNoetherianRing.of_isLocalization_maximal {R : Type u_1} [CommSemiring R] [Finite (MaximalSpectrum R)] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3) [(P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (H : ∀ (P : Ideal R) [inst : P.IsMaximal], IsNoetherianRing (Rₚ P)) : IsNoetherianRing R

A semilocal ring R is Noetherian if its localization at every maximal ideal is a Noetherian ring.

theorem isPrincipalIdealRing_of_isPrincipalIdealRing_isLocalization_maximal {R : Type u_1} [CommRing R] [Finite (MaximalSpectrum R)] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] [IsDomain R] (hpid : ∀ (P : Ideal R) [inst : P.IsMaximal], IsPrincipalIdealRing (Rₚ P)) : IsPrincipalIdealRing R

A semilocal integral domain A is a PID if its localization at every maximal ideal is a PID.