Documentation

Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Purely inseparable extensions are universal homeomorphisms #

If K is a purely inseparable extension of k, the induced map Spec K ⟶ Spec k is a universal homeomorphism, i.e. it stays a homeomorphism after arbitrary base change.

Main results #

theorem PrimeSpectrum.isHomeomorph_comap {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (H : ∀ (x : S), n > 0, x ^ n f.range) (hker : RingHom.ker f nilradical R) :

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 ℤ.

Stacks Tag 0BR8 (Homeomorphism part)

Purely inseparable field extensions are universal homeomorphisms.

Stacks Tag 0BRA (Special case for purely inseparable field extensions)

If L is a purely inseparable extension of K over R and S is an R-algebra, the induced map Spec (L ⊗[R] S) ⟶ Spec (K ⊗[R] S) is a homeomorphism.