Regular functions with finite image

A regular function on a reduced connected affine scheme of finite type over an algebraically closed field is constant if it takes only finitely many values on rational points. This permits one to turn finiteness of an algebraic action into constancy, without constructing a morphism to a finite constant scheme.

The argument uses Lagrange interpolation to separate one value from the others by an idempotent, followed by point separation and connectedness.

theorem TauCeti.eq_algebraMap_of_finite_range_eval {k : Type u_1} {A : Type u_2} [Field k] [IsAlgClosed k] [CommRing A] [Algebra k A] [Algebra.FiniteType k A] [IsReduced A] [ConnectedSpace (PrimeSpectrum A)] (a : A) (hfinite : (Set.range fun (f : A →ₐ[k] k) => f a).Finite) (f₀ : A →ₐ[k] k) : a = (algebraMap k A) (f₀ a)

A regular function with finite image on rational points of a reduced connected affine scheme is the constant given by its value at any chosen rational point.