Theorems · Definition · algebraic geometry

AlgebraicGeometry.pointEquivClosedPoint

{X : AlgebraicGeometry.Scheme} →
  {K : Type u} →
    [inst : Field K] →
      [IsAlgClosed K] →
        (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) →
          [AlgebraicGeometry.LocallyOfFiniteType f] →
            { p //
                CategoryTheory.CategoryStruct.comp p f =
                  CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)) } ≃
              ↑(closedPoints ↥X)

If k is algebraically closed, then the closed points of X are in bijection with the k-points of X.

Defined in

Mathlib.AlgebraicGeometry.AlgClosed.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldIsAlgClosedAlgebraicGeometry.LocallyOfFiniteType