Density of rational points over an algebraically closed field #
The kernels of points of a finite-type algebra over an algebraically closed field are dense in its prime spectrum, even when the algebra is nonreduced. This allows arguments on open subsets of the spectrum to be tested on rational points.
theorem
TauCeti.denseRange_kernelPoint
{k : Type u_1}
{A : Type u_2}
[Field k]
[IsAlgClosed k]
[CommRing A]
[Algebra k A]
[Algebra.FiniteType k A]
:
Rational points are dense in the spectrum of a finite-type algebra over an algebraically closed field.