theorem
eq_zero_of_localization_module
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
(h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (LocalizedModule.mkLinearMap J.primeCompl M) x = 0)
:
x = 0
theorem
module_eq_zero_of_localization
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Subsingleton (LocalizedModule.AtPrime J M))
:
theorem
submodule_le_of_localization
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(P : Submodule R M)
(h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Submodule.localized J.primeCompl N ≤ Submodule.localized J.primeCompl P)
:
N ≤ P
theorem
submodule_eq_of_localization
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(P : Submodule R M)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Submodule.localized J.primeCompl N = Submodule.localized J.primeCompl P)
:
N = P
theorem
submodule_eq_bot_of_localization
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Submodule.localized J.primeCompl N = ⊥)
:
theorem
submodule_eq_top_of_localization
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(h : ∀ (J : Ideal R) (x : J.IsMaximal), Submodule.localized J.primeCompl N = ⊤)
:
theorem
exact_of_localization
{R : Type u_1}
{M₀ : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[CommRing R]
[AddCommGroup M₀]
[Module R M₀]
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
(f : M₀ →ₗ[R] M₁)
(g : M₁ →ₗ[R] M₂)
(h : ∀ (J : Ideal R) (hJ : J.IsMaximal),
Function.Exact ⇑((LocalizedModule.map J.primeCompl) f) ⇑((LocalizedModule.map J.primeCompl) g))
:
Function.Exact ⇑f ⇑g
theorem
eq_zero_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(x : M)
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(h : ∀ (r : { x : R // x ∈ s }), (LocalizedModule.mkLinearMap (Submonoid.powers ↑r) M) x = 0)
:
x = 0
theorem
submodule_le_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(P : Submodule R M)
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(h : ∀ (r : { x : R // x ∈ s }), Submodule.localized (Submonoid.powers ↑r) N ≤ Submodule.localized (Submonoid.powers ↑r) P)
:
N ≤ P
theorem
submodule_eq_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(P : Submodule R M)
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(h : ∀ (r : { x : R // x ∈ s }), Submodule.localized (Submonoid.powers ↑r) N = Submodule.localized (Submonoid.powers ↑r) P)
:
N = P
theorem
submodule_eq_bot_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(h : ∀ (r : { x : R // x ∈ s }), Submodule.localized (Submonoid.powers ↑r) N = ⊥)
:
theorem
submodule_eq_top_of_localization_finitespan
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(h : ∀ (r : { x : R // x ∈ s }), Submodule.localized (Submonoid.powers ↑r) N = ⊤)
:
theorem
exact_of_localization_finitespan
{R : Type u_1}
{M₀ : Type u_2}
{M₁ : Type u_3}
{M₂ : Type u_4}
[CommRing R]
[AddCommGroup M₀]
[Module R M₀]
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
(s : Finset R)
(spn : Ideal.span ↑s = ⊤)
(f : M₀ →ₗ[R] M₁)
(g : M₁ →ₗ[R] M₂)
(h : ∀ (r : { x : R // x ∈ s }),
Function.Exact ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f) ⇑((LocalizedModule.map (Submonoid.powers ↑r)) g))
:
Function.Exact ⇑f ⇑g