Theorems · Theorem · commutative algebra

Module.exists_localizedMap_surjective_of_surjective

∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FinitePresentation R M] (S : Submonoid R) {Mₚ : Type u_1}
  [inst_6 : AddCommGroup Mₚ] [inst_7 : Module R Mₚ] (f : M →ₗ[R] Mₚ) [inst_8 : IsLocalizedModule S f] {Nₚ : Type u_2}
  [inst_9 : AddCommGroup Nₚ] [inst_10 : Module R Nₚ] (g : N →ₗ[R] Nₚ) [inst_11 : IsLocalizedModule S g]
  {ϕ : Mₚ →ₗ[R] Nₚ},
  Function.Surjective ⇑ϕ →
    ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)

Let M be a finitely presented R-module, N be an R-module, S be a submonoid of R, Mₚ be the localization of M at S, Nₚ be the localization of N at S. Then any surjective linear map ϕ : Mₚ →ₗ[R] Nₚ lifts to a linear map φ : M →ₗ[R] N that is surjective after localization at S.

Defined in

Mathlib.Algebra.Module.FinitePresentation

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleModule.FinitePresentationAddCommGroupModuleIsLocalizedModuleAddCommGroupModuleIsLocalizedModule