le_of_localization_maximal — Mathlib

English

If a localized module is complete over the localized ring, the same holds globally.

Русский

Если локализованный модуль полно завершается над локализованным кольцом, то и глобально полно завершен.

LaTeX

$$$M_S \\cong (R_S)^n$ implies $M$ is free of rank n (locally).$$$

Lean4

/-- 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₂`. -/
theorem le_of_localization_maximal {N₁ N₂ : Submodule R M}
    (h : ∀ (P : Ideal R) [P.IsMaximal], N₁.localized₀ P.primeCompl (f P) ≤ N₂.localized₀ P.primeCompl (f P)) :
    N₁ ≤ N₂ := fun m hm ↦ mem_of_localization_maximal _ f _ _ fun P hP ↦ h P ⟨m, hm, 1, by simp⟩

Похожие утверждения