Theorems · Theorem · commutative algebra

Module.FinitePresentation.exists_basis_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') [inst_5 : 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']
  [IsLocalization S Rₛ] [Module.FinitePresentation R M] {I : Type u_6} [Finite I] (b : Module.Basis I Rₛ M'),
  ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (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.

Defined in

Mathlib.RingTheory.Localization.Free

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleIsLocalizedModuleCommRingAlgebraModuleIsScalarTowerIsLocalizationModule.FinitePresentationFinite