Finite affine fibers of a linear map exclude a projective base point. Projective fibers inject into affine fibers after choosing a fixed nonzero representative in the target.

theorem CCDN.projective_linear_image_ne_zero_of_finite_zero_fiber {n r : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) (L : (Fin (n + 1) → ℚ) →ₗ[ℚ] Fin r → ℚ) (M : ℕ) (hfinite : ∀ (s : Finset (Fin (n + 1) → ℚ)), (∀ z ∈ s, z ∈ idealZeroLocus I) → (∀ z ∈ s, L z = 0) → s.card ≤ M) (x : ProjectivePoint n) (hx : x ∈ projectiveIdealZeroLocus I) : L (Projectivization.rep x) ≠ 0

If the zeros of I in ℚ^(n+1) killed by the linear map L form a set of at most M elements, then L does not vanish on the representative of any point of the projective zero locus of I.

theorem CCDN.projective_linear_fiber_card_le {n m : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) ℚ)) (L : (Fin (n + 1) → ℚ) →ₗ[ℚ] Fin (m + 1) → ℚ) (s : Finset (ProjectivePoint n)) (hs : ∀ x ∈ s, x ∈ projectiveIdealZeroLocus I) (hL : ∀ x ∈ s, L (Projectivization.rep x) ≠ 0) (y : ProjectivePoint m) (he : ∀ (x : ProjectivePoint n) (hx : x ∈ s), Projectivization.mk ℚ (L (Projectivization.rep x)) ⋯ = y) (M : ℕ) (hfinite : ∀ (t : Finset (Fin (n + 1) → ℚ)), (∀ z ∈ t, z ∈ idealZeroLocus I) → (∀ z ∈ t, L z = Projectivization.rep y) → t.card ≤ M) : s.card ≤ M

Let s be a finite set of points of the projective zero locus of I on which the linear map L is nonzero and which L sends to the single projective point y. If at most M zeros of I in ℚ^(n+1) are sent by L to the representative of y, then s has at most M elements.