Points and sections of schemes

TheoremClosed points of finite-type schemes over algebraically closed fields#✓fully proved

A closed point of a scheme of finite type over an algebraically closed field lifts to a point over the base.

theorem exists_over_hom_base_closedPoint_eq_of_isClosed_singleton
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} (t : X ⟶ Spec (CommRingCat.of k))
    [LocallyOfFiniteType t] (x : X) (hx : IsClosed ({x} : Set X)) :
    ∃ z : Over.mk (𝟙 (Spec (CommRingCat.of k))) ⟶ Over.mk t,
      z.left.base (IsLocalRing.closedPoint k) = x

TheoremPullback points determined by projections given a residue isomorphism#✓fully proved

Two points of a pullback with the same first and second projections are equal, when the residue field map at the second point's first projection is an isomorphism.

theorem AlgebraicGeometry.Scheme.Pullback.eq_of_fst_eq_of_snd_eq_of_isIso_residueFieldMap
    {X Y S : Scheme.{u}} {f : X ⟶ S} {g : Y ⟶ S} {t₁ t₂ : ↥(pullback f g)}
    (h₁ : (pullback.fst f g).base t₁ = (pullback.fst f g).base t₂)
    (h₂ : (pullback.snd f g).base t₁ = (pullback.snd f g).base t₂)
    [IsIso (f.residueFieldMap ((pullback.fst f g).base t₂))] :
    t₁ = t₂

TheoremValuative criterion for factoring sections through an open subscheme#✓fully proved

A section over a valuation ring factors through a universally closed open subscheme exactly when the generic point does.

theorem AlgebraicGeometry.exists_section_comp_eq_iff_factors_of_universallyClosed_of_valuationRing
    (R : Type u) [CommRing R] [IsDomain R] [ValuationRing R]
    (K : Type u) [Field K] [Algebra R K] [IsFractionRing R K]
    {X Xf X' : Scheme.{u}} (g : X ⟶ Spec (.of R))
    (i : Xf ⟶ X) [IsOpenImmersion i] [UniversallyClosed (i ≫ g)]
    (j : X' ⟶ X)
    (hcover : Set.range i ∪ Set.range j = Set.univ)
    (hempty : IsLocalRing.closedPoint R ∉ Set.range (j ≫ g))
    (x : Spec (.of K) ⟶ X) (hx : x ≫ g = Spec.map (CommRingCat.ofHom (algebraMap R K))) :
    (∃ s : Spec (.of R) ⟶ X, s ≫ g = 𝟙 _ ∧
      Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ s = x) ↔
      ∃ xf : Spec (.of K) ⟶ Xf, xf ≫ i = x

TheoremDensity of rational points over an algebraically closed field#✓fully proved

Rational points over an algebraically closed field are dense.

theorem AlgebraicGeometry.dense_setOf_exists_section_of_isAlgClosed
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] :
    Dense {x : X | ∃ s : Spec (.of k) ⟶ X, s ≫ f = 𝟙 _ ∧
      s (IsLocalRing.closedPoint k) = x}

Used by 1

Used bySurjective morphisms of finite type lift rational points

TheoremMorphisms are determined by their values on rational points#✓fully proved

Two morphisms over an algebraically closed field agreeing on all rational points are equal.

theorem AlgebraicGeometry.ext_of_forall_comp_eq_of_isAlgClosed
    {κ : Type u} [Field κ] [IsAlgClosed κ] {X Y : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of κ)) (fY : Y ⟶ Spec (CommRingCat.of κ))
    [LocallyOfFiniteType fX] [IsReduced X] [IsSeparated fY]
    {f g : X ⟶ Y} (hf : f ≫ fY = fX) (hg : g ≫ fY = fX)
    (h : ∀ x : Spec (CommRingCat.of κ) ⟶ X, x ≫ fX = 𝟙 _ → x ≫ f = x ≫ g) :
    f = g

TheoremSurjective morphisms of finite type lift rational points#✓fully proved

A surjective morphism locally of finite type lifts rational points over an algebraically closed field.

theorem AlgebraicGeometry.exists_comp_eq_of_surjective_of_locallyOfFiniteType_of_isAlgClosed
    {K : Type u} [Field K] [IsAlgClosed K] {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [Surjective f] (y : Spec (.of K) ⟶ Y) :
    ∃ x : Spec (.of K) ⟶ X, x ≫ f = y

Uses 1

Proof usesDensity of rational points over an algebraically closed field

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.