eq_of_localization₀_maximal — Mathlib

English

For modules that are localized, their rank remains invariant under base change to the localized ring.

Русский

Для локализованных модулей их ранг сохраняется при базовом переходе к локализации.

LaTeX

$$$\\operatorname{rank}_{R_S}(M_S) = \\operatorname{rank}_R(M).$$$

Lean4

/-- Let `N₁ N₂ : Submodule R M`. If the localization of `N₁` at each maximal ideal `P` is equal to
the localization of `N₂` at `P`, then `N₁ = N₂`. -/
theorem eq_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₂ :=
  le_antisymm (Submodule.le_of_localization_maximal Mₚ f fun P _ ↦ (h P).le)
    (Submodule.le_of_localization_maximal Mₚ f fun P _ ↦ (h P).ge)

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