English
The Zariski topology on the maximal spectrum of a commutative ring R is defined as the subspace topology induced by the natural inclusion into the prime spectrum.
Русский
Зарискина топология на максимальном спектре кольца R задаётся как подпространственная топология, порождаемая естественным включением в простой спектр.
LaTeX
$$$\\operatorname{zariskiTopology}_{\\operatorname{MaximalSpectrum}(R)} = \\left( \\operatorname{zariskiTopology}_{\\operatorname{PrimeSpectrum}(R)} \\right)_{\\text{induced by } \\mathrm{toPrimeSpectrum}}$$$
Lean4
/-- The Zariski topology on the maximal spectrum of a commutative ring is defined as the subspace
topology induced by the natural inclusion into the prime spectrum. -/
instance zariskiTopology : TopologicalSpace <| MaximalSpectrum R :=
PrimeSpectrum.zariskiTopology.induced toPrimeSpectrum
