Theorems · Definition · algebraic geometry

AlgebraicGeometry.pointOfClosedPoint

{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} → (AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X)

If k is algebraically closed, this is the k-point of X associated to a closed point.

Defined in

Mathlib.AlgebraicGeometry.AlgClosed.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

FieldIsAlgClosedAlgebraicGeometry.LocallyOfFiniteType