Theorems · Theorem · commutative algebra

Submodule.le_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)] {N₁ N₂ : Submodule R M},
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal],
      Submodule.localized₀ P.primeCompl (f P) N₁ ≤ Submodule.localized₀ P.primeCompl (f P) N₂) →
    N₁ ≤ N₂

Let N₁ N₂ : Submodule R M. If the localization of N₁ at each maximal ideal P is included in the localization of N₂ at P, then N₁ ≤ N₂.

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

CommSemiringAddCommMonoidModuleAddCommMonoidModuleIsLocalizedModule