English
Let R be a commutative semiring. The Zariski topology on the spectrum is discrete if and only if there are finitely many maximal ideals and their intersection is contained in the nilradical.
Русский
Пусть R — коммутативное полукольцо. Зари топология на спектре дискретна тогда и только тогда, когда максимальных идеалов конечное число и их пересечение содержится в нильрадикале.
LaTeX
$$$\\operatorname{DiscreteTopology}(\\operatorname{PrimeSpectrum}(R)) \\iff \\operatorname{Finite}(s) \\land sInf(s) \\le \\nilradical(R)$, where $s = \\{ I : I \\text{ maximal} \\}$.$$
Lean4
/-- The prime spectrum of a semiring has discrete Zariski topology iff there are only
finitely many maximal ideals and their intersection is contained in the nilradical. -/
theorem discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical :
letI s := {I : Ideal R | I.IsMaximal}
DiscreteTopology (PrimeSpectrum R) ↔ Finite s ∧ sInf s ≤ nilradical R :=
by
rw [discreteTopology_iff_finite_and_krullDimLE_zero, Ring.krullDimLE_zero_iff, (equivSubtype R).finite_iff, ←
Set.coe_setOf, Set.finite_coe_iff, Set.finite_coe_iff]
refine ⟨fun h ↦ ⟨h.1.subset fun _ h ↦ h.isPrime, nilradical_eq_sInf R ▸ sInf_le_sInf h.2⟩, fun ⟨fin, le⟩ ↦ ?_⟩
have hpm (I : Ideal R) (hI : I.IsPrime) : I.IsMaximal :=
by
replace le := le.trans (nilradical_le_prime I)
rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le
have ⟨M, hM, hMI⟩ := le
rw [fin.mem_toFinset] at hM
rwa [← hM.eq_of_le hI.1 hMI]
exact ⟨fin.subset hpm, hpm⟩
