Theorems · Theorem · algebraic geometry

PrimeSpectrum.isHomeomorph_comap

∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  (∀ (x : S), ∃ n > 0, x ^ n ∈ f.range) → RingHom.ker f ≤ nilradical R → IsHomeomorph (PrimeSpectrum.comap f)

If the kernel of f : R →+* S consists of nilpotent elements and for every x : S, there exists n > 0 such that x ^ n is in the range of f, then Spec f is a homeomorphism. Note: This does not hold for semirings, because ℕ →+* ℤ satisfies these conditions, but Spec ℕ has one more point than Spec ℤ.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Cited by

1 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRing