Theorems · Theorem · algebraic geometry

PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable

∀ (k : Type u_1) (K : Type u_2) (R : Type u_3) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  [inst_3 : CommRing R] [inst_4 : Algebra k R] [IsPurelyInseparable k K],
  IsHomeomorph (PrimeSpectrum.comap (algebraMap R (TensorProduct k R K)))

Purely inseparable field extensions are universal homeomorphisms.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraCommRingAlgebraIsPurelyInseparable