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 IsLocalization.smul_mem_finsetIntegerMultiple_span {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (M : Submonoid R) (S' : Type u_4) [CommRing S'] [Algebra S S'] [Algebra R S] [Algebra R S'] [IsScalarTower R S S'] [IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S') (hx : (algebraMap S S') x ∈ Submodule.span R ↑s) : ∃ (m : ↥M), m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Let S be an R-algebra, M a submonoid of R, and S' = M⁻¹S. If the image of some x : S falls in the span of some finite s ⊆ S' over R, then there exists some m : M such that m • x falls in the span of IsLocalization.finsetIntegerMultiple _ s over R.

theorem multiple_mem_span_of_mem_localization_span {R : Type u_1} [CommRing R] (M : Submonoid R) (R' : Type u_3) [CommRing R'] [Algebra R R'] {N : Type u_5} [AddCommMonoid N] [Module R N] [Module R' N] [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N) (hx : x ∈ Submodule.span R' s) : ∃ (t : ↥M), t • x ∈ Submodule.span R s

If M is an R' = S⁻¹R module, and x ∈ span R' s, then t • x ∈ span R s for some t : S.

theorem multiple_mem_adjoin_of_mem_localization_adjoin {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (M : Submonoid R) (R' : Type u_3) [CommRing R'] [Algebra R R'] [Algebra R' S] [Algebra R S] [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S) (x : S) (hx : x ∈ Algebra.adjoin R' s) : ∃ (t : ↥M), t • x ∈ Algebra.adjoin R s

If S is an R' = M⁻¹R algebra, and x ∈ adjoin R' s, then t • x ∈ adjoin R s for some t : M.

theorem Module.Finite.of_isLocalization (R : Type u_3) (S : Type u_4) {Rₚ : Type u_1} {Sₚ : Type u_2} [CommSemiring R] [CommSemiring S] [CommSemiring Rₚ] [CommSemiring Sₚ] [Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] : Module.Finite Rₚ Sₚ

instance Module.Finite.instAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} {S : Type u_2} [CommRing R] {P : Ideal R} [CommRing S] [Algebra R S] [Module.Finite R S] [P.IsPrime] : Module.Finite (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))

instance Module.Finite.instFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors {A : Type u_1} {C : Type u_2} [CommRing A] [CommRing C] [Algebra A C] [Module.Finite A C] : Module.Finite (FractionRing A) (Localization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)))

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ₚ

instance Module.Finite.instLocalizationLocalizedModule {R : Type u} [CommSemiring R] (S : Submonoid R) {M : Type w} [AddCommMonoid M] [Module R M] [Module.Finite R M] : Module.Finite (Localization S) (LocalizedModule S 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ₚ : ↥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)] [∀ (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) [∀ (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 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 : ↥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 : span t = ⊤) (H : ∀ (g : ↑t), (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), (ker (Localization.awayMap f ↑g)).FG) : (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.