Sharp specialization-fiber bounds over a normal base. A single integral linear combination separates a finite set of characteristic-zero points. Its specialized monic minimal polynomial bounds the entire fiber by the fraction-field rank, independently of the number of coordinates.
theorem
CCDN.integral_projection_fiber_card_le_finrank
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[CharZero K]
[Finite σ]
(I : Ideal (MvPolynomial σ K))
[I.IsPrime]
(l : τ → MvPolynomial σ K)
[Algebra (MvPolynomial τ K) (MvPolynomial σ K ⧸ I)]
(hmap : algebraMap (MvPolynomial τ K) (MvPolynomial σ K ⧸ I) = (projectionCoordinateMap I l).toRingHom)
(F : Type u_4)
(E : Type u_5)
[Field F]
[Field E]
[Algebra (MvPolynomial τ K) F]
[IsFractionRing (MvPolynomial τ K) F]
[Algebra (MvPolynomial τ K) E]
[Algebra (MvPolynomial σ K ⧸ I) E]
[Algebra F E]
[IsScalarTower (MvPolynomial τ K) (MvPolynomial σ K ⧸ I) E]
[IsScalarTower (MvPolynomial τ K) F E]
[FiniteDimensional F E]
(hint : (projectionCoordinateMap I l).IsIntegral)
(z : τ → K)
(s : Finset (σ → K))
(hzero : ∀ x ∈ s, x ∈ idealZeroLocus I)
(hproj : ∀ x ∈ s, ∀ (i : τ), (MvPolynomial.eval x) (l i) = z i)
:
In characteristic zero, every fiber of an integral projection of the variety of a prime I
by polynomials l has at most [E : F] points, where F is the fraction field of the polynomial
ring of the target and E is a finite extension of F receiving the coordinate ring of I.