Theorems · Theorem · commutative algebra

bijective_of_isLocalized_maximal

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_6 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_7 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_7 : ∀ (P : Ideal R) [inst_7 : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)]
  (Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7) [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
  [inst_9 : (P : Ideal R) → [inst_9 : P.IsMaximal] → Module R (Nₚ P)]
  (g : (P : Ideal R) → [inst_10 : P.IsMaximal] → N →ₗ[R] Nₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (F : M →ₗ[R] N),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal], Function.Bijective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)) →
    Function.Bijective ⇑F

Defined in

Mathlib.RingTheory.LocalProperties.Exactness

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModuleIsLocalizedModule.AtPrimeAddCommMonoidModuleIsLocalizedModule.AtPrime