A homogeneous linear projection with a nonzero conductor preserves Hilbert multiplicity. The conductor shifts the filtration by a fixed amount, which leaves the leading coefficient of the Hilbert polynomial unchanged.
theorem
CCDN.homogeneous_projection_leadingCoeff_eq
{K : Type u_1}
{σ : Type u_2}
{τ : Type u_3}
[Field K]
[Fintype σ]
[Fintype τ]
[LinearOrder σ]
[LinearOrder τ]
(I : Ideal (MvPolynomial τ K))
[I.IsPrime]
(hI : IsHomogeneousIdeal I)
(a : σ → MvPolynomial τ K)
(ha : ∀ (i : σ), (a i).IsHomogeneous 1)
(hd :
(filteredHilbertPolynomial (RingHom.ker (projectionCoordinateMap I a))).natDegree = (filteredHilbertPolynomial I).natDegree)
(c : MvPolynomial τ K)
(hc : (Ideal.Quotient.mk I) c ≠ 0)
(hconductor :
∀ (x : MvPolynomial τ K ⧸ I), ∃ (p : MvPolynomial σ K), (projectionCoordinateMap I a) p = (Ideal.Quotient.mk I) c * x)
:
A nonzero conductor yields equality of Hilbert multiplicities for a homogeneous linear birational projection.