Theorems · Definition · field theory

Algebra.FormallyEtale.equivPiOfIsSepClosed

(K : Type u_1) →
  (A : Type u) →
    [inst : Field K] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra K A] →
          [Algebra.EssFiniteType K A] → [Algebra.FormallyEtale K A] → [IsSepClosed K] → A ≃ₐ[K] PrimeSpectrum A → K

If R is an étale k-algebra over a separably closed field k, it is isomorphic to the (finite) product of copies of k indexed by the prime spectrum of R.

Defined in

Mathlib.RingTheory.Etale.Field

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldCommRingAlgebraAlgebra.EssFiniteTypeAlgebra.FormallyEtaleIsSepClosed