English
The prime spectrum has discrete Zariski topology if and only if there are finitely many maximal ideals and their intersection is contained in the nilradical.
Русский
Спектр простых идеалов имеет дискретную топологию Зари тогда и только тогда, когда максимумов конечное число и их пересечение содержится в нильрадикале.
LaTeX
$$$\\operatorname{DiscreteTopology}(\\operatorname{PrimeSpectrum}(R)) \\iff \\operatorname{Finite}(s) \\land sInf(s) \\le \\nilradical(R)$ with $s = \\{ I : I \\text{ maximal}\\}.$$$
Lean4
/-- The continuous function between prime spectra of commutative (semi)rings induced by a ring
homomorphism. -/
def comap (f : R →+* S) : C(PrimeSpectrum S, PrimeSpectrum R)
where
toFun := f.specComap
continuous_toFun := by
simp only [continuous_iff_isClosed, isClosed_iff_zeroLocus]
rintro _ ⟨s, rfl⟩
exact ⟨_, preimage_specComap_zeroLocus_aux f s⟩
