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.

noncomputable def AlgebraicGeometry.residueFieldIsoBase {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType f] (x : ↥X) (hx : 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.

Equations

• AlgebraicGeometry.residueFieldIsoBase f x hx = (CategoryTheory.asIso (AlgebraicGeometry.Spec.preimage (CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f))).symm

@[simp]

theorem AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec (CommRingCat.of K)) [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 (CommRingCat.of K)) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) {Z : Scheme} (h : Spec (CommRingCat.of K) ⟶ 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 (CommRingCat.of K)) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) : Spec (CommRingCat.of K) ⟶ X

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

Equations

• AlgebraicGeometry.pointOfClosedPoint f x hx = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.residueFieldIsoBase f x hx).hom) (X.fromSpecResidueField x)

@[simp]

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

@[simp]

theorem AlgebraicGeometry.pointOfClosedPoint_comp_assoc {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) {Z : Scheme} (h : Spec (CommRingCat.of K) ⟶ 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 (CommRingCat.of K)) [LocallyOfFiniteType f] (x : ↥X) (hx : IsClosed {x}) (a : ↥(Spec (CommRingCat.of K))) : (pointOfClosedPoint f x hx) a = x

noncomputable def AlgebraicGeometry.pointEquivClosedPoint {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType f] : { p : Spec (CommRingCat.of K) ⟶ X // CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.id (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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.pointEquivClosedPoint_apply_coe {X : Scheme} {K : Type u} [Field K] [IsAlgClosed K] (f : X ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType f] (p : { p : Spec (CommRingCat.of K) ⟶ X // CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.id (Spec (CommRingCat.of K)) }) : ↑((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 (CommRingCat.of K)) [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 (CommRingCat.of K) ⟶ X} (h : X ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType h] (hf : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.id (Spec (CommRingCat.of K))) (hg : CategoryTheory.CategoryStruct.comp g h = CategoryTheory.CategoryStruct.id (Spec (CommRingCat.of K))) (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 (CommRingCat.of K)) [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.