Theorems · Definition · algebraic geometry

AlgebraicGeometry.residueFieldIsoBase

{X : AlgebraicGeometry.Scheme} →
  {K : Type u} →
    [inst : Field K] →
      [IsAlgClosed K] →
        (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) →
          [AlgebraicGeometry.LocallyOfFiniteType f] → (x : ↥X) → IsClosed {x} → (X.residueField x ≅ CommRingCat.of K)

If X is a locally of finite type k-scheme and k is algebraically closed, then the residue field of any closed point of x is isomorphic to k.

Defined in

Mathlib.AlgebraicGeometry.AlgClosed.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

FieldIsAlgClosedAlgebraicGeometry.LocallyOfFiniteType