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
: iff : R →+* S
is a ring map with locally nilpotent kernel such that for everyx : S
, there existsn > 0
such thatx ^ n
is in the image off
,Spec f
is a homeomorphism.PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable
:Spec K ⟶ Spec k
is a universal homeomorphism for a purely inseparable field extensionK
overk
.
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.