Free modules and localization #
Main result #
Module.FinitePresentation.exists_free_localizedModule_powers: IfMis a finitely presentedR-module such thatMₛis free overRₛfor someS : Submonoid R, thenMᵣis already free overRᵣfor somer ∈ S.
Future projects #
- Show that a finitely presented flat module has locally constant dimension.
- Show that the flat locus of a finitely presented module is open.
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ₛ]
[Module.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 (Submonoid.powers 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ₛ]
[Module.FinitePresentation R M]
[Module.Free Rₛ M']
:
∃ r ∈ S,
Module.Free (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) ∧ Module.finrank (Localization (Submonoid.powers r)) (LocalizedModule (Submonoid.powers r) M) = Module.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.