English
If M has no zero smul divisors, then the support is the entire spectrum.
Русский
Если у модуля нет нулевых делителей по умножению, то опора равна всему спектру.
LaTeX
$$[NoZeroSMulDivisors R M] [Nontrivial M] ⇒ \mathrm{Supp}_R(M) = \operatorname{Spec} R$$
Lean4
theorem support_of_algebra {A : Type*} [Ring A] [Algebra R A] :
Module.support R A = PrimeSpectrum.zeroLocus (RingHom.ker (algebraMap R A)) :=
by
ext p
simp only [mem_support_iff', ne_eq, PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe]
refine ⟨fun ⟨m, hm⟩ x hx ↦ not_not.mp fun hx' ↦ ?_, fun H ↦ ⟨1, fun r hr e ↦ ?_⟩⟩
· simpa [Algebra.smul_def, (show _ = _ from hx)] using hm _ hx'
· exact hr (H ((Algebra.algebraMap_eq_smul_one _).trans e))
