Documentation

ModuleLocalProperties.FinitePresentation

theorem submodule.of_localizationSpan_finite {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (s : Finset R) (spn : Ideal.span s = ) (H : ∀ (g : { x : R // x s }), (Submodule.localized (Submonoid.powers g) N).FG) :
N.FG
theorem finitepresented_of_localization_fintespan {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (s : Finset R) (spn : Ideal.span s = ) (h : ∀ (r : { x : R // x s }), Module.FinitePresentation (Localization.Away r) (LocalizedModule.Away (↑r) M)) :
theorem isNoetherian_of_localization_finitespan {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (s : Finset R) (spn : Ideal.span s = ) (h : ∀ (r : { x : R // x s }), IsNoetherian (Localization.Away r) (LocalizedModule.Away (↑r) M)) :
theorem isNoetherianRing_of_localization_finitespan {R : Type u_1} [CommRing R] (s : Finset R) (spn : Ideal.span s = ) (h : ∀ (r : { x : R // x s }), IsNoetherianRing (Localization.Away r)) :
theorem Submodule.localized'_of_finite {R : Type u_1} {M : Type u_2} {S_M : Type u_3} (S_R : Type u_4) [CommRing R] [CommRing S_R] [Algebra R S_R] [AddCommGroup M] [Module R M] [AddCommGroup S_M] [Module R S_M] [Module S_R S_M] [IsScalarTower R S_R S_M] (S : Submonoid R) [IsLocalization S S_R] (f : M →ₗ[R] S_M) [IsLocalizedModule S f] {p : Submodule R M} (h : p.FG) :
(Submodule.localized' S_R S f p).FG
theorem Submodule.localized_of_finite {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (S : Submonoid R) {p : Submodule R M} (h : p.FG) :