Rational points in images of scheme morphisms

Over an algebraically closed field, a rational point lies in the topological image of a morphism between locally finite-type schemes exactly when it lifts to a rational point. This compares the full scheme image, which can contain nonclosed points, with the image on rational points. No reducedness, smoothness or separability hypothesis is needed.

Constructible subsets of a locally finite-type scheme are determined by their rational points; in particular a nonempty locally closed subset contains a rational point. For morphisms between finite-type schemes, Chevalley's theorem therefore detects image inclusions and surjectivity on rational points. These comparisons allow rational orbit calculations to control the full constructible image of an algebraic orbit morphism.

The proofs use Mathlib's pointEquivClosedPoint, pointOfClosedPoint and Chevalley theorem, and Scheme.Hom.image_closedPoints_eq_range_inter_closedPoints for closed-point lifting.

References

• J. S. Milne, Algebraic Groups (2017), §7.c, the comparison of geometric orbits with rational-point orbits.

theorem AlgebraicGeometry.Scheme.Hom.exists_comp_eq_iff_mem_range {k : Type u} [Field k] [IsAlgClosed k] {X Y : Scheme} (f : X ⟶ Y) (π : Y ⟶ Spec ↧k) [LocallyOfFiniteType π] [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f π)] (p : Spec ↧k ⟶ Y) (hp : CategoryTheory.CategoryStruct.comp p π = CategoryTheory.CategoryStruct.id (Spec ↧k)) : (∃ (q : Spec ↧k ⟶ X), CategoryTheory.CategoryStruct.comp q f = p) ↔ p (IsLocalRing.closedPoint k) ∈ Set.range ⇑f

A rational point in the image of a morphism between locally finite-type schemes over an algebraically closed field lifts to a rational point. Any lift is automatically over the base, since its composite with the morphism is the specified rational point.

theorem Topology.IsConstructible.subset_iff_forall_rationalPoint {k : Type u} [Field k] [IsAlgClosed k] {Y : AlgebraicGeometry.Scheme} {s t : Set ↥Y} (hs : IsConstructible s) (π : Y ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType π] (ht : IsConstructible t) : s ⊆ t ↔ ∀ (p : AlgebraicGeometry.Spec ↧k ⟶ Y), CategoryTheory.CategoryStruct.comp p π = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧k) → p (IsLocalRing.closedPoint k) ∈ s → p (IsLocalRing.closedPoint k) ∈ t

Inclusion between constructible subsets of a locally finite-type scheme over an algebraically closed field can be tested on rational points.

theorem Topology.IsConstructible.eq_iff_forall_rationalPoint {k : Type u} [Field k] [IsAlgClosed k] {Y : AlgebraicGeometry.Scheme} {s t : Set ↥Y} (hs : IsConstructible s) (π : Y ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType π] (ht : IsConstructible t) : s = t ↔ ∀ (p : AlgebraicGeometry.Spec ↧k ⟶ Y), CategoryTheory.CategoryStruct.comp p π = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧k) → (p (IsLocalRing.closedPoint k) ∈ s ↔ p (IsLocalRing.closedPoint k) ∈ t)

Constructible subsets of a locally finite-type scheme over an algebraically closed field are equal exactly when they have the same rational points.

theorem IsLocallyClosed.exists_rationalPoint_mem {k : Type u} [Field k] [IsAlgClosed k] {Y : AlgebraicGeometry.Scheme} {s : Set ↥Y} (hs : IsLocallyClosed s) (π : Y ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.LocallyOfFiniteType π] (hne : s.Nonempty) : ∃ (p : AlgebraicGeometry.Spec ↧k ⟶ Y), CategoryTheory.CategoryStruct.comp p π = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧k) ∧ p (IsLocalRing.closedPoint k) ∈ s

A nonempty locally closed subset of a locally finite-type scheme over an algebraically closed field contains a rational point.

theorem AlgebraicGeometry.Scheme.Hom.range_subset_range_iff_forall_rationalPoint {k : Type u} [Field k] [IsAlgClosed k] {X Y Z : Scheme} (f : X ⟶ Y) (π : Y ⟶ Spec ↧k) [LocallyOfFiniteType π] [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f π)] [CompactSpace ↥X] [CompactSpace ↥Y] (g : Z ⟶ Y) [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp g π)] [CompactSpace ↥Z] : Set.range ⇑f ⊆ Set.range ⇑g ↔ ∀ (p : Spec ↧k ⟶ Y), CategoryTheory.CategoryStruct.comp p π = CategoryTheory.CategoryStruct.id (Spec ↧k) → (∃ (q : Spec ↧k ⟶ X), CategoryTheory.CategoryStruct.comp q f = p) → ∃ (r : Spec ↧k ⟶ Z), CategoryTheory.CategoryStruct.comp r g = p

Inclusions between the full images of morphisms of finite-type schemes over an algebraically closed field can be tested by lifting rational points.

theorem AlgebraicGeometry.Scheme.Hom.surjective_iff_forall_rationalPoint {k : Type u} [Field k] [IsAlgClosed k] {X Y : Scheme} (f : X ⟶ Y) (π : Y ⟶ Spec ↧k) [LocallyOfFiniteType π] [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f π)] [CompactSpace ↥X] [CompactSpace ↥Y] : Function.Surjective ⇑f ↔ ∀ (p : Spec ↧k ⟶ Y), CategoryTheory.CategoryStruct.comp p π = CategoryTheory.CategoryStruct.id (Spec ↧k) → ∃ (q : Spec ↧k ⟶ X), CategoryTheory.CategoryStruct.comp q f = p

A morphism between finite-type schemes over an algebraically closed field is surjective on all scheme points exactly when every rational point has a rational lift.