Documentation

Mathlib.RingTheory.Localization.Finiteness

Finiteness properties under localization #

In this file we establish behaviour of Module.Finite under localizations.

Main results #

theorem Module.Finite.of_isLocalizedModule {R : Type u} [CommSemiring R] (S : Submonoid R) {Rₚ : Type v} [CommSemiring Rₚ] [Algebra R Rₚ] [IsLocalization S Rₚ] {M : Type w} [AddCommMonoid M] [Module R M] {Mₚ : Type t} [AddCommMonoid Mₚ] [Module R Mₚ] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] (f : M →ₗ[R] Mₚ) [IsLocalizedModule S f] [Module.Finite R M] :
Module.Finite Rₚ Mₚ
theorem Module.Finite.of_localizationSpan_finite' {R : Type u} [CommRing R] {M : Type w} [AddCommMonoid M] [Module R M] (t : Finset R) (ht : Ideal.span t = ) {Mₚ : { x : R // x t }Type u_1} [(g : { x : R // x t }) → AddCommMonoid (Mₚ g)] [(g : { x : R // x t }) → Module R (Mₚ g)] {Rₚ : { x : R // x t }Type u} [(g : { x : R // x t }) → CommRing (Rₚ g)] [(g : { x : R // x t }) → Algebra R (Rₚ g)] [∀ (g : { x : R // x t }), IsLocalization.Away (↑g) (Rₚ g)] [(g : { x : R // x t }) → Module (Rₚ g) (Mₚ g)] [∀ (g : { x : R // x t }), IsScalarTower R (Rₚ g) (Mₚ g)] (f : (g : { x : R // x t }) → M →ₗ[R] Mₚ g) [∀ (g : { x : R // x t }), IsLocalizedModule (Submonoid.powers g) (f g)] (H : ∀ (g : { x : R // x t }), Module.Finite (Rₚ g) (Mₚ g)) :

If there exists a finite set { r } of R such that Mᵣ is Rᵣ-finite for each r, then M is a finite R-module.

General version for any modules Mᵣ and rings Rᵣ satisfying the correct universal properties. See Module.Finite.of_localizationSpan_finite for the specialized version.

See of_localizationSpan' for a version without the finite set assumption.

theorem Module.Finite.of_localizationSpan' {R : Type u} [CommRing R] {M : Type w} [AddCommMonoid M] [Module R M] (t : Set R) (ht : Ideal.span t = ) {Mₚ : tType u_1} [(g : t) → AddCommMonoid (Mₚ g)] [(g : t) → Module R (Mₚ g)] {Rₚ : tType u} [(g : t) → CommRing (Rₚ g)] [(g : t) → Algebra R (Rₚ g)] [h₁ : ∀ (g : t), IsLocalization.Away (↑g) (Rₚ g)] [(g : t) → Module (Rₚ g) (Mₚ g)] [∀ (g : t), IsScalarTower R (Rₚ g) (Mₚ g)] (f : (g : t) → M →ₗ[R] Mₚ g) [h₂ : ∀ (g : t), IsLocalizedModule (Submonoid.powers g) (f g)] (H : ∀ (g : t), Module.Finite (Rₚ g) (Mₚ g)) :

If there exists a set { r } of R such that Mᵣ is Rᵣ-finite for each r, then M is a finite R-module.

General version for any modules Mᵣ and rings Rᵣ satisfying the correct universal properties. See Module.Finite.of_localizationSpan_finite for the specialized version.

theorem Module.Finite.of_localizationSpan_finite {R : Type u} [CommRing R] {M : Type w} [AddCommMonoid M] [Module R M] (t : Finset R) (ht : Ideal.span t = ) (H : ∀ (g : { x : R // x t }), Module.Finite (Localization.Away g) (LocalizedModule (Submonoid.powers g) M)) :

If there exists a finite set { r } of R such that Mᵣ is Rᵣ-finite for each r, then M is a finite R-module.

See of_localizationSpan for a version without the finite set assumption.

theorem Module.Finite.of_localizationSpan {R : Type u} [CommRing R] {M : Type w} [AddCommMonoid M] [Module R M] (t : Set R) (ht : Ideal.span t = ) (H : ∀ (g : t), Module.Finite (Localization.Away g) (LocalizedModule (Submonoid.powers g) M)) :

If there exists a set { r } of R such that Mᵣ is Rᵣ-finite for each r, then M is a finite R-module.

theorem Ideal.fg_of_localizationSpan {R : Type u} [CommRing R] {I : Ideal R} (t : Set R) (ht : Ideal.span t = ) (H : ∀ (g : t), (Ideal.map (algebraMap R (Localization.Away g)) I).FG) :
I.FG

If I is an ideal such that there exists a set { r } of R such that the image of I in Rᵣ is finitely generated for each r, then I is finitely generated.

theorem RingHom.ker_fg_of_localizationSpan {R : Type u} [CommRing R] {S : Type v} [CommRing S] {f : R →+* S} (t : Set R) (ht : Ideal.span t = ) (H : ∀ (g : t), (RingHom.ker (Localization.awayMap f g)).FG) :

To check that the kernel of a ring homomorphism is finitely generated, it suffices to check this after localizing at a spanning set of the source.