Theorems · Theorem · commutative algebra

Module.FinitePresentation.exists_free_localizedModule_powers

∀ {R : Type u_4} {M : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  {M' : Type u_1} [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  (Rₛ : Type u_3) [inst_6 : CommRing Rₛ] [inst_7 : Algebra R Rₛ] [inst_8 : 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.Away r M) ∧
      Module.finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away 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.

Defined in

Mathlib.RingTheory.Localization.Free

Cited by

2 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleIsLocalizedModuleCommRingAlgebraModuleIsScalarTowerNontrivialIsLocalizationModule.FinitePresentationModule.Free