Local properties of modules and submodules

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

theorem Submodule.mem_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (m : M) (N : Submodule R M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ Submodule.localized₀ P.primeCompl (f P) N) : m ∈ N

theorem Submodule.le_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M} (h : ∀ (P : Ideal R) [inst : 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₂.

theorem Submodule.eq_of_localization₀_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M} (h : ∀ (P : Ideal R) [inst : 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 equal to the localization of N₂ at P, then N₁ = N₂.

theorem Submodule.eq_bot_of_localization₀_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Submodule.localized₀ P.primeCompl (f P) N = ⊥) : N = ⊥

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

theorem Submodule.eq_top_of_localization₀_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Submodule.localized₀ P.primeCompl (f P) N = ⊤) : N = ⊤

theorem Module.eq_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (m m' : M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = (f P) m') : m = m'

theorem Module.eq_zero_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (m : M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m = 0) : m = 0

theorem LinearMap.eq_of_localization_maximal {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (M₁ₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_6) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (M₁ₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (M₁ₚ P)] (f₁ : (P : Ideal R) → [inst : P.IsMaximal] → M₁ →ₗ[R] M₁ₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f₁ P)] (g g' : M →ₗ[R] M₁) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g = (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g') : g = g'

theorem Module.subsingleton_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)] (f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)) : Subsingleton M

theorem Submodule.eq_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4) [(P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (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_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (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) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] {N₁ N₂ : Submodule R M} (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N₁ = Submodule.localized' (Rₚ P) P.primeCompl (f P) N₂) : N₁ = N₂

theorem Submodule.eq_bot_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4) [(P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (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_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (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) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N = ⊥) : N = ⊥

theorem Submodule.eq_top_of_localization_maximal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4) [(P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (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_5) [(P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (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) [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M) (h : ∀ (P : Ideal R) [inst : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N = ⊤) : N = ⊤