Support of a module

Main results

• Module.support: The support of an R-module as a subset of Spec R.
• Module.mem_support_iff_exists_annihilator: p ∈ Supp M ↔ ∃ m, Ann(m) ≤ p.
• Module.support_eq_empty_iff: Supp M = ∅ ↔ M = 0
• Module.support_of_exact: Supp N = Supp M ∪ Supp P for an exact sequence 0 → M → N → P → 0.
• Module.support_eq_zeroLocus: If M is R-finite, then Supp M = Z(Ann(M)).
• LocalizedModule.exists_subsingleton_away: If M is R-finite and Mₚ = 0, then M[1/f] = 0 for some p ∈ D(f).

Also see AlgebraicGeometry/PrimeSpectrum/Module for other results depending on the zariski topology.

TODO

• Connect to associated primes once we have them in mathlib.
• Given an R-algebra f : R → A and a finite R-module M, Supp_A (A ⊗ M) = f♯ ⁻¹ Supp M where f♯ : Spec A → Spec R. (stacks#0BUR)

def Module.support (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : Set (PrimeSpectrum R)

The support of a module, defined as the set of primes p such that Mₚ ≠ 0.

Equations

• Module.support R M = {p : PrimeSpectrum R | Nontrivial (LocalizedModule p.asIdeal.primeCompl M)}

theorem Module.mem_support_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} : p ∈ Module.support R M ↔ Nontrivial (LocalizedModule p.asIdeal.primeCompl M)

theorem Module.not_mem_support_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} : p ∉ Module.support R M ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

theorem Module.not_mem_support_iff' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} : p ∉ Module.support R M ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0

theorem Module.mem_support_iff' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} : p ∈ Module.support R M ↔ ∃ (m : M), ∀ r ∉ p.asIdeal, r • m ≠ 0

theorem Module.mem_support_iff_exists_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} : p ∈ Module.support R M ↔ ∃ (m : M), (Submodule.span R {m}).annihilator ≤ p.asIdeal

theorem Module.mem_support_iff_of_span_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} {s : Set M} (hs : Submodule.span R s = ⊤) : p ∈ Module.support R M ↔ ∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal

theorem Module.annihilator_le_of_mem_support {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} (hp : p ∈ Module.support R M) : Module.annihilator R M ≤ p.asIdeal

theorem LocalizedModule.subsingleton_iff_support_subset {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : R} : Subsingleton (LocalizedModule (Submonoid.powers f) M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

theorem Module.support_eq_empty_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : Module.support R M = ∅ ↔ Subsingleton M

theorem Module.support_eq_empty {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Subsingleton M] : Module.support R M = ∅

theorem Module.support_of_algebra {R : Type u_1} [CommRing R] {A : Type u_3} [Ring A] [Algebra R A] : Module.support R A = PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))

theorem Module.support_of_noZeroSMulDivisors {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [Nontrivial M] : Module.support R M = Set.univ

theorem Module.mem_support_iff_of_finite {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} [Module.Finite R M] : p ∈ Module.support R M ↔ Module.annihilator R M ≤ p.asIdeal

theorem Module.support_subset_of_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) : Module.support R M ⊆ Module.support R N

theorem Module.support_subset_of_surjective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) : Module.support R N ⊆ Module.support R M

theorem Module.support_of_exact {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_3} {P : Type u_4} [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Module.support R N = Module.support R M ∪ Module.support R P

Given an exact sequence 0 → M → N → P → 0 of R-modules, Supp N = Supp M ∪ Supp P.

theorem LinearEquiv.support_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Module.support R M = Module.support R N

theorem Module.support_eq_zeroLocus {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.support R M = PrimeSpectrum.zeroLocus ↑(Module.annihilator R M)

If M is R-finite, then Supp M = Z(Ann(M)).

theorem LocalizedModule.exists_subsingleton_away {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (p : Ideal R) [p.IsPrime] [Subsingleton (LocalizedModule p.primeCompl M)] : ∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)

If M is a finite module such that Mₚ = 0 for some p, then M[1/f] = 0 for some p ∈ D(f).