Dominance, injectivity and density on prime spectra

An injective homomorphism of commutative semirings induces a dense map on prime spectra. For a reduced source ring, the converse holds. These facts supply the coordinate-ring criterion for dominance used in dominant affine group quotients.

A subset of the prime spectrum containing every minimal prime is dense. This is how generic properties, such as freeness of a module at the minimal primes of a reduced ring, are turned into dense subsets of the spectrum.

theorem RingHom.denseRange_comap_of_injective {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Injective ⇑f) : DenseRange (PrimeSpectrum.comap f)

An injective homomorphism of commutative semirings induces a dense map on prime spectra.

theorem RingHom.denseRange_comap_iff_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommSemiring S] [IsReduced R] (f : R →+* S) : DenseRange (PrimeSpectrum.comap f) ↔ Function.Injective ⇑f

A ring homomorphism from a reduced ring is injective exactly when its spectral comap has dense range.

theorem PrimeSpectrum.dense_of_forall_mem_minimalPrimes {R : Type u_1} [CommSemiring R] {s : Set (PrimeSpectrum R)} (hs : ∀ (p : Ideal R) (hp : p ∈ minimalPrimes R), { asIdeal := p, isPrime := ⋯ } ∈ s) : Dense s

A subset of the prime spectrum containing every minimal prime is dense: every nonempty open set contains a minimal prime, namely a generization of any of its points.