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 Mathlib/RingTheory/Spectrum/Prime/Module.lean 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 ∈ support R M ↔ Nontrivial (LocalizedModule p.asIdeal.primeCompl M)

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

theorem Module.notMem_support_iff' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : PrimeSpectrum R} : p ∉ 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 ∈ 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 ∈ support R M ↔ ∃ (m : M), (R ∙ m).annihilator ≤ p.asIdeal

theorem Module.mem_support_mono {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p q : PrimeSpectrum R} (H : p ≤ q) (hp : p ∈ support R M) : q ∈ support R M

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 ∈ support R M ↔ ∃ m ∈ s, (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 ∈ support R M) : 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.Away 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] : support R M = ∅ ↔ Subsingleton M

theorem Module.nonempty_support_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : (support R M).Nonempty ↔ Nontrivial M

theorem Module.nonempty_support_of_nontrivial {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] : (support R M).Nonempty

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

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

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

@[deprecated Module.support_of_isTorsionFree (since := "2026-07-27")]

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

Alias of Module.support_of_isTorsionFree.

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) : support R M ⊆ support R N

Stacks Tag 00L3 ((2))

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) : support R N ⊆ support R M

Stacks Tag 00L3 ((3))

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) : support R N = support R M ∪ 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.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 ∈ support R M ↔ annihilator R M ≤ p.asIdeal

theorem Module.support_eq_zeroLocus {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : support R M = PrimeSpectrum.zeroLocus ↑(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.Away 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).

theorem IsLocalizedModule.exists_subsingleton_away {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] {M' : Type u_5} [AddCommMonoid M'] [Module R M'] (l : M →ₗ[R] M') (p : Ideal R) [p.IsPrime] [IsLocalizedModule p.primeCompl l] [Subsingleton M'] : ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

theorem Module.exists_localizedMap_away_surjective_of_localizedMap_atPrime_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] [Module.Finite R M] (p : Ideal R) [p.IsPrime] (φ : N →ₗ[R] M) (hφ : Function.Surjective ⇑((LocalizedModule.map p.primeCompl) φ)) : ∃ a ∉ p, Function.Surjective ⇑((LocalizedModule.map (Submonoid.powers a)) φ)

theorem Module.support_quotient {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) : support R (M ⧸ I • ⊤) = support R M ∩ PrimeSpectrum.zeroLocus ↑I

Supp(M/IM) = Supp(M) ∩ Z(I).

@[simp]

theorem Module.support_quotSMulTop {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (x : R) : support R (QuotSMulTop x M) = support R M ∩ PrimeSpectrum.zeroLocus {x}