English
The Zariski topology on the prime spectrum of a commutative semiring is discrete if and only if the spectrum is finite and the Krull dimension is at most zero.
Русский
Топология Зари на спектре простых идеалов коммутативного полукольца дискретна тогда и только тогда, когда спектр конечен и размер Крull не превосходит нуль.
LaTeX
$$$\\operatorname{DiscreteTopology}(\\operatorname{PrimeSpectrum}(R)) \\iff \\operatorname{Finite}(\\operatorname{PrimeSpectrum}(R)) \\land \\operatorname{Ring.KrullDimLE} 0\\, R$$$
Lean4
/-- The prime spectrum of a commutative semiring has discrete Zariski topology iff it is finite and
the semiring has Krull dimension zero or is trivial. -/
theorem discreteTopology_iff_finite_and_krullDimLE_zero :
DiscreteTopology (PrimeSpectrum R) ↔ Finite (PrimeSpectrum R) ∧ Ring.KrullDimLE 0 R :=
⟨fun _ ↦
⟨finite_of_compact_of_discrete,
.mk₀ fun I h ↦ isClosed_singleton_iff_isMaximal ⟨I, h⟩ |>.mp <| discreteTopology_iff_forall_isClosed.mp ‹_› _⟩,
fun ⟨_, _⟩ ↦ .of_finite_of_isClosed_singleton fun p ↦ (isClosed_singleton_iff_isMaximal p).mpr inferInstance⟩
