Theorems · Theorem · commutative algebra

Module.FinitePresentation.exists_notMem_bijective

∀ {R : Type u_5} {M : Type u_6} {N : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R M] [Module.FinitePresentation R N] (f : M →ₗ[R] N)
  (p : Ideal R) [inst_7 : p.IsPrime] {Mₚ : Type u_3} {Nₚ : Type u_4} [inst_8 : AddCommGroup Mₚ]
  [inst_9 : AddCommGroup Nₚ] [inst_10 : Module R Mₚ] [inst_11 : Module R Nₚ] (fM : M →ₗ[R] Mₚ) (fN : N →ₗ[R] Nₚ)
  [inst_12 : IsLocalizedModule p.primeCompl fM] [inst_13 : IsLocalizedModule p.primeCompl fN],
  Function.Bijective ⇑((IsLocalizedModule.map p.primeCompl fM fN) f) →
    ∃ g ∉ p, Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers g)) f)

Let M be a finite R-module and N be a finitely presented R-module. If f : M →ₗ[R] N is a linear map whose localization at a prime ideal p is bijective, then there exists g ∉ p such that f is already bijective under the localization away from g.

Defined in

Mathlib.Algebra.Module.FinitePresentation

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleModule.FiniteModule.FinitePresentationIdeal.IsPrimeAddCommGroupAddCommGroupModuleModuleIsLocalizedModuleIsLocalizedModule