Local properties of modules and submodules

In this file, we show that several conditions on submodules can be checked on stalks.

theorem Submodule.le_of_localization_maximal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M} (h : ∀ (P : Ideal R) [inst_1 : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N₁ ≤ Submodule.localized' (Rₚ P) 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₂.

theorem Submodule.eq_of_localization_maximal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M} (h : ∀ (P : Ideal R) [inst_1 : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N₁ = Submodule.localized' (Rₚ P) P.primeCompl (f P) N₂) : N₁ = N₂

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 Submodule.eq_bot_of_localization_maximal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N₁ : Submodule R M) (h : ∀ (P : Ideal R) [inst_1 : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N₁ = ⊥) : N₁ = ⊥

A submodule is trivial if its localization at every maximal ideal is trivial.

theorem Submodule.mem_of_localization_maximal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (r : M) (N₁ : Submodule R M) (h : ∀ (P : Ideal R) [inst_1 : P.IsMaximal], (f P) r ∈ Submodule.localized' (Rₚ P) P.primeCompl (f P) N₁) : r ∈ N₁

theorem Module.eq_zero_of_localization_maximal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (r : M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) r = 0) : r = 0

theorem Module.eq_of_localization_maximal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (r s : M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) r = (f P) s) : r = s

theorem Module.subsingleton_of_localization_maximal {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_1) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_2) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)) : Subsingleton M