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_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)

@[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 ⋯

theorem AlgebraicGeometry.ext_of_apply_closedPoint_eq {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] {f g : Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶ X} (h : X ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [LocallyOfFiniteType h] (hf : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.id (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })) (hg : CategoryTheory.CategoryStruct.comp g h = CategoryTheory.CategoryStruct.id (Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })) (H : f (IsLocalRing.closedPoint K) = g (IsLocalRing.closedPoint K)) : f = g

theorem AlgebraicGeometry.ext_of_apply_eq {X Y : Scheme} {K : Type u} [Field K] [IsAlgClosed K] {f g : X ⟶ Y} (i : Y ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing }) [IsSeparated i] [LocallyOfFiniteType i] [IsReduced X] [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f i)] (S : Set ↥X) (hS : IsLocallyClosed S) (hS' : Dense S) (H : ∀ x ∈ S, IsClosed {x} → f x = g x) (H' : CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i) : f = g

Let X and Y be locally of finite type K-schemes with K algebraically closed and Y separated over K. Suppose X is reduced, then two K-morphisms f g : X ⟶ Y are equal if they are equal on the closed points of a dense locally closed subset of X.