Closed points in the image of a finite-type morphism

A morphism locally of finite type into a Jacobson scheme maps closed points to closed points. Conversely, every closed point in its image lifts to a closed point of the source: the nonempty closed fiber contains a closed point in the Jacobson source. Thus its image on closed points is exactly the closed-point part of its full topological image.

This complements Mathlib's Scheme.Hom.closedPoints_subset_preimage_closedPoints with the lifting direction, needed to compare rational and topological orbit images.

References

• The Stacks Project, Tag 01TB, morphisms locally of finite type into Jacobson schemes.

theorem AlgebraicGeometry.Scheme.Hom.image_closedPoints_eq_range_inter_closedPoints {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y] : ⇑f '' closedPoints ↥X = Set.range ⇑f ∩ closedPoints ↥Y

The image on closed points is exactly the intersection of the full image with the closed points of the target.