Theorems · Theorem · commutative algebra

Submodule.mem_of_localization_maximal

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (m : M) (N : Submodule R M),
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal], (f P) m ∈ Submodule.localized₀ P.primeCompl (f P) N) → m ∈ N

Defined in

Mathlib.RingTheory.LocalProperties.Submodule

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleIsLocalizedModule