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

• PrimeSpectrum.isHomeomorph_comap: if f : R →+* S is a ring map with locally nilpotent kernel such that for every x : S, there exists n > 0 such that x ^ n is in the image of f, Spec f is a homeomorphism.
• PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable: Spec K ⟶ Spec k is a universal homeomorphism for a purely inseparable field extension K over k.

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) : IsHomeomorph ⇑(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 ℤ.

theorem PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable (k : Type u_1) (K : Type u_2) (R : Type u_3) [Field k] [Field K] [Algebra k K] [CommRing R] [Algebra k R] [IsPurelyInseparable k K] : IsHomeomorph ⇑(comap (algebraMap R (TensorProduct k R K)))

Purely inseparable field extensions are universal homeomorphisms.

theorem PrimeSpectrum.isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable (K : Type u_2) (R : Type u_3) (S : Type u_4) [Field K] [CommRing R] [CommRing S] [Algebra R K] [Algebra R S] (L : Type u_5) [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L] [IsPurelyInseparable K L] : IsHomeomorph ⇑(comap (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S)).toRingHom)

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.