Module.FinitePresentation is a local property

In this file, we prove that Module.FinitePresentation is a local property.

Main results

• Module.FinitePresentation.of_localizationSpan : If there exists a set { r } of R that generates the unit ideal and such that Mᵣ is a finitely presented Rᵣ-module for each r, then M is a finitely presented R-module.

theorem Module.FinitePresentation.of_localizationSpan' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (s : Set R) (hs : Ideal.span s = ⊤) {Mₚ : ↑s → Type u_3} [(g : ↑s) → AddCommGroup (Mₚ g)] [(g : ↑s) → Module R (Mₚ g)] {Rₚ : ↑s → Type u_4} [(g : ↑s) → CommRing (Rₚ g)] [(g : ↑s) → Algebra R (Rₚ g)] [∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)] [(g : ↑s) → Module (Rₚ g) (Mₚ g)] [∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)] (ϕ : (g : ↑s) → M →ₗ[R] Mₚ g) [∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)] (h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)) : FinitePresentation R M

theorem Module.FinitePresentation.of_localizationSpan {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (s : Set R) (hs : Ideal.span s = ⊤) (h : ∀ (g : ↑s), FinitePresentation (Localization.Away ↑g) (LocalizedModule.Away (↑g) M)) : FinitePresentation R M

If there exists a set { r } of R that generates the unit ideal and such that Mᵣ is a finitely presented Rᵣ-module for each r, then M is a finitely presented R-module.