Schemes over algebraically closed fields

We show that if X is locally of finite type over an algebraically closed field k, then the closed points of X are in bijection with the k-points of X. See AlgebraicGeometry.pointEquivClosedPoint.

def AlgebraicGeometry.residueFieldIsoBase {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : X.residueField x ≅ { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }

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.

@[simp]

theorem AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : Spec.map (residueFieldIsoBase f x hx).inv = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f

theorem AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv_assoc {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) {Z : Scheme} (h : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (residueFieldIsoBase f x hx).inv) h = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) (CategoryTheory.CategoryStruct.comp f h)

noncomputable def AlgebraicGeometry.pointOfClosedPoint {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ X

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

@[simp]

theorem AlgebraicGeometry.pointOfClosedPoint_comp {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : CategoryTheory.CategoryStruct.comp (pointOfClosedPoint f x hx) f = CategoryTheory.CategoryStruct.id (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })

@[simp]

theorem AlgebraicGeometry.pointOfClosedPoint_comp_assoc {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) {Z : Scheme} (h : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ Z) : CategoryTheory.CategoryStruct.comp (pointOfClosedPoint f x hx) (CategoryTheory.CategoryStruct.comp f h) = h

@[simp]

theorem AlgebraicGeometry.pointOfClosedPoint_apply {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) (a : ↥(Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })) : (pointOfClosedPoint f x hx) a = x

def AlgebraicGeometry.pointEquivClosedPoint {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] : { p : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ X // CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.id (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) } ≃ ↑(closedPoints ↥X)

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

@[simp]

theorem AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (x : ↑(closedPoints ↥X)) : ↑((pointEquivClosedPoint f).symm x) = pointOfClosedPoint f ↑x ⋯

@[simp]

theorem AlgebraicGeometry.pointEquivClosedPoint_apply_coe {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType f] (p : { p : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ X // CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.id (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) }) : ↑((pointEquivClosedPoint f) p) = ↑p (IsLocalRing.closedPoint K)