Documentation

Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal

Maximal spectrum of a commutative ring #

The maximal spectrum of a commutative ring is the type of all maximal ideals. It is naturally a subset of the prime spectrum endowed with the subspace topology.

Main definitions #

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 MaximalSpectrum.toPrimeSpectrum = {x : PrimeSpectrum R | IsClosed {x}}

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
Equations
  • =
theorem MaximalSpectrum.toPrimeSpectrum_continuous {R : Type u} [CommRing R] :
Continuous MaximalSpectrum.toPrimeSpectrum