Subsets of prime spectra related to modules

Main results

• LocalizedModule.subsingleton_iff_disjoint : M[1/f] = 0 ↔ D(f) ∩ Supp M = 0.
• Module.isClosed_support : If M is a finite R-module, then Supp M is closed.

TODO

• If M is finitely presented, the complement of Supp M is quasi-compact. (stacks#051B)

theorem IsLocalRing.closedPoint_mem_support (R : Type u_1) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Nontrivial M] : closedPoint R ∈ Module.support R M

theorem LocalizedModule.subsingleton_iff_disjoint {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {f : R} : Subsingleton (LocalizedModule.Away f M) ↔ Disjoint (↑(PrimeSpectrum.basicOpen f)) (Module.support R M)

M[1/f] = 0 if and only if D(f) ∩ Supp M = 0.

theorem Module.stableUnderSpecialization_support {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : StableUnderSpecialization (support R M)

theorem Module.isClosed_support {R : Type u_1} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : IsClosed (support R M)

theorem Module.support_subset_preimage_comap {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [CommRing A] [Algebra R A] [Module A M] [IsScalarTower R A M] : support A M ⊆ PrimeSpectrum.comap (algebraMap R A) ⁻¹' support R M