Free modules and localization

Main result

• Module.FinitePresentation.exists_free_localizedModule_powers: If M is a finitely presented R-module such that Mₛ is free over Rₛ for some S : Submonoid R, then Mᵣ is already free over Rᵣ for some r ∈ S.

In the file Mathlib.RingTheory.Spectrum.Prime.FreeLocus, we deduce that the free locus of a finitely presented module is open and its rank is locally constant.

theorem Module.FinitePresentation.exists_basis_localizedModule_powers {R : Type u_4} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (S : Submonoid R) {M' : Type u_1} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (Rₛ : Type u_3) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [IsScalarTower R Rₛ M'] [IsLocalization S Rₛ] [FinitePresentation R M] {I : Type u_6} [Finite I] (b : Basis I Rₛ M') : ∃ (r : R) (hr : r ∈ S) (b' : Basis I (Localization (Submonoid.powers r)) (LocalizedModule.Away r M)), ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i

If M is a finitely presented R-module, then any Rₛ-basis of Mₛ for some S : Submonoid R can be lifted to a Rᵣ-basis of Mᵣ for some r ∈ S.

theorem Module.FinitePresentation.exists_free_localizedModule_powers {R : Type u_4} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (S : Submonoid R) {M' : Type u_1} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (Rₛ : Type u_3) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [IsScalarTower R Rₛ M'] [Nontrivial Rₛ] [IsLocalization S Rₛ] [FinitePresentation R M] [Free Rₛ M'] : ∃ r ∈ S, Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧ finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'

If M is a finitely presented R-module such that Mₛ is free over Rₛ for some S : Submonoid R, then Mᵣ is already free over Rᵣ for some r ∈ S.