The Zariski topology on the maximal spectrum of a commutative (semi)ring

Implementation notes

The Zariski topology on the maximal spectrum is defined as the subspace topology induced by the natural inclusion into the prime spectrum to avoid API duplication for zero loci.

theorem MaximalSpectrum.toPrimeSpectrum_range {R : Type u} [CommRing R] : Set.range toPrimeSpectrum = {x : PrimeSpectrum R | IsClosed {x}}

@[instance_reducible]

instance MaximalSpectrum.zariskiTopology {R : Type u} [CommRing R] : TopologicalSpace (MaximalSpectrum R)

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.

Equations

• MaximalSpectrum.zariskiTopology = TopologicalSpace.induced MaximalSpectrum.toPrimeSpectrum PrimeSpectrum.zariskiTopology

instance MaximalSpectrum.instT1Space {R : Type u} [CommRing R] : T1Space (MaximalSpectrum R)

theorem MaximalSpectrum.toPrimeSpectrum_continuous {R : Type u} [CommRing R] : Continuous toPrimeSpectrum