Rational-point fibers of an integral polynomial projection. Evaluation on the quotient constructs the specialization homomorphisms.

theorem CCDN.exists_projection_fiber_specialization {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] (I : Ideal (MvPolynomial σ K)) (l : τ → MvPolynomial σ K) [Algebra (MvPolynomial τ K) (MvPolynomial σ K ⧸ I)] (hmap : algebraMap (MvPolynomial τ K) (MvPolynomial σ K ⧸ I) = (projectionCoordinateMap I l).toRingHom) (z : τ → K) (x : σ → K) (hzero : x ∈ idealZeroLocus I) (hproj : ∀ (i : τ), (MvPolynomial.eval x) (l i) = z i) : ∃ (ψ : MvPolynomial σ K ⧸ I →ₐ[MvPolynomial τ K] K), ∀ (i : σ), ψ ((Ideal.Quotient.mk I) (MvPolynomial.X i)) = x i

A rational point of the fiber over z gives a specialization of the quotient algebra over the parameter ring, sending each coordinate function to the corresponding coordinate.