Theorems · Definition · algebraic geometry

CommAlgCat.FiniteEtale.fiberIsoComp

(R : Type u) →
  [inst : CommRing R] →
    (Ω : Type w) →
      [inst_1 : Field Ω] →
        [inst_2 : Algebra R Ω] →
          [IsSepClosed Ω] →
            CommAlgCat.FiniteEtale.fiber R Ω ≅
              (CommAlgCat.FiniteEtale.baseChange R Ω).op.comp (CommAlgCat.FiniteEtale.finiteSpec Ω)

If Ω is separably closed, the fiber S →ₐ[R] Ω is isomorphic to the prime spectrum of the base change Ω ⊗[R] S.

Defined in

Mathlib.RingTheory.Etale.Finite

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsSepClosed