Homogeneous interpolation on distinct projective points. The separating polynomials have one common degree, so their classes belong to a single graded coordinate space.
theorem
CCDN.exists_projective_point_separators_degree
{K : Type u_1}
[Field K]
{n M : ℕ}
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
(z : ι → Projectivization K (Fin (n + 1) → K))
(hz : Function.Injective z)
(hM : Fintype.card ι - 1 ≤ M)
:
∃ (h : ι → MvPolynomial (Fin (n + 1)) K),
(∀ (j : ι), (h j).IsHomogeneous M) ∧ ∀ (i j : ι), (MvPolynomial.eval (z i).rep) (h j) = if i = j then 1 else 0
Separators can be raised to any larger common degree without changing their values on the selected representatives.