noncomputable def LinearEquiv.extendScalarsOfIsLocalization {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M ≃ₗ[R] N) : M ≃ₗ[A] N

Equations

• LinearEquiv.extendScalarsOfIsLocalization S A f = LinearEquiv.ofBijective (LinearMap.extendScalarsOfIsLocalization S A ↑f) ⋯

noncomputable def submodule_localization_equiv {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M) (S : Submonoid R) : ↥(Submodule.localized S N) ≃ₗ[Localization S] LocalizedModule S ↥N

Equations

• submodule_localization_equiv N S = LinearEquiv.extendScalarsOfIsLocalization S (Localization S) (IsLocalizedModule.iso S (Submodule.toLocalized S N)).symm

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)) : Module.FinitePresentation 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)) : IsNoetherian 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)) : IsNoetherianRing 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) : (Submodule.localized S p).FG