Finiteness properties under localization

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

Main results

• Module.Finite.of_isLocalizedModule: If M is a finite R-module, S is a submonoid of R, Rₚ is the localization of R at S and Mₚ is the localization of M at S, then Mₚ is a finite Rₚ-module.
• Module.Finite.of_localizationSpan_finite: If M is an R-module and { r } is a finite set generating the unit ideal such that Mᵣ is a finite Rᵣ-module for each r, then M is a finite R-module.

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)) : Module.Finite R 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.

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ₚ : ↑t → Type u_1} [(g : ↑t) → AddCommMonoid (Mₚ g)] [(g : ↑t) → Module R (Mₚ g)] {Rₚ : ↑t → Type 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)) : Module.Finite R 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.

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)) : Module.Finite R 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)) : Module.Finite R 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) : (RingHom.ker f).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.