Degree bounds for hypersurface equations of linear projections. The degree is bounded by the factorial-normalized leading coefficient of the original quotient's filtered Hilbert polynomial.

theorem CCDN.exists_hypersurface_projection_equation_degree_le {K : Type u_1} {τ : Type u_2} [Field K] [Fintype τ] [LinearOrder τ] {n : ℕ} (I : Ideal (MvPolynomial τ K)) [I.IsPrime] (a : Fin (n + 2) → MvPolynomial τ K) (ha : ∀ (i : Fin (n + 2)), (a i).totalDegree ≤ 1) (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I n d) (b : Fin (n + 1) → MvPolynomial (Fin (n + 2)) K) (hb : ∀ (i : Fin (n + 1)), (b i).totalDegree ≤ 1) (hi : AlgebraicIndependent K fun (i : Fin (n + 1)) => (projectionCoordinateMap I a) (b i)) : ∃ (f : MvPolynomial (Fin (n + 2)) K), Irreducible f ∧ 0 < f.totalDegree ∧ f.totalDegree ≤ d ∧ RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f}

The equation and its degree bound are constructed from the projection.