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 = ⊤

theorem Module.eq_of_isLocalized_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] (x y : M) (h : ∀ (r : ↑s), (f r) x = (f r) y) : x = y

theorem Module.eq_zero_of_isLocalized_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] (x : M) (h : ∀ (r : ↑s), (f r) x = 0) : x = 0

theorem Submodule.mem_of_isLocalized_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {m : M} {N : Submodule R M} (h : ∀ (r : ↑s), (f r) m ∈ Submodule.localized₀ (Submonoid.powers ↑r) (f r) N) : m ∈ N

theorem Submodule.le_of_isLocalized_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {N P : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N ≤ Submodule.localized₀ (Submonoid.powers ↑r) (f r) P) : N ≤ P

theorem Submodule.eq_of_isLocalized₀_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {N P : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = Submodule.localized₀ (Submonoid.powers ↑r) (f r) P) : N = P

theorem Submodule.eq_bot_of_isLocalized₀_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = ⊥) : N = ⊥

theorem Submodule.eq_top_of_isLocalized₀_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = ⊤) : N = ⊤

theorem Submodule.eq_of_isLocalized'_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Rₚ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Rₚ r)] [(r : ↑s) → Algebra R (Rₚ r)] [∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] [(r : ↑s) → Module (Rₚ r) (Mₚ r)] [∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {N P : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) P) : N = P

theorem Submodule.eq_bot_of_isLocalized'_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Rₚ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Rₚ r)] [(r : ↑s) → Algebra R (Rₚ r)] [∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] [(r : ↑s) → Module (Rₚ r) (Mₚ r)] [∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊥) : N = ⊥

theorem Submodule.eq_top_of_isLocalized'_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (span_eq : Ideal.span s = ⊤) (Rₚ : ↑s → Type u_4) [(r : ↑s) → CommSemiring (Rₚ r)] [(r : ↑s) → Algebra R (Rₚ r)] [∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5) [(r : ↑s) → AddCommMonoid (Mₚ r)] [(r : ↑s) → Module R (Mₚ r)] [(r : ↑s) → Module (Rₚ r) (Mₚ r)] [∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)] (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)] {N : Submodule R M} (h : ∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊤) : N = ⊤