Theorems · Theorem · commutative algebra

LinearMap.eq_of_localization_maximal

∀ {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5)
  [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 P.primeCompl (f P)]
  (M₁ₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (M₁ₚ P)]
  [inst_9 : (P : Ideal R) → [inst_9 : P.IsMaximal] → Module R (M₁ₚ P)]
  (f₁ : (P : Ideal R) → [inst_10 : P.IsMaximal] → M₁ →ₗ[R] M₁ₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule P.primeCompl (f₁ P)] (g g' : M →ₗ[R] M₁),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal],
      (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g = (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g') →
    g = g'

Defined in

Mathlib.RingTheory.LocalProperties.Submodule

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleAddCommMonoidModuleIsLocalizedModuleAddCommMonoidModuleIsLocalizedModule