The irreducible image equation has degree at most the original affine Hilbert degree. This is an upper bound; the degree need not be preserved.
theorem
CCDN.plane_projection_equation_degree_le
{K : Type u_1}
{τ : Type u_2}
[Field K]
[Finite τ]
(I : Ideal (MvPolynomial τ K))
(a : Fin 2 → MvPolynomial τ K)
(ha : ∀ (i : Fin 2), (a i).totalDegree ≤ 1)
(d : ℕ)
(hdegree : HasFilteredCurveDegree I d)
(f : MvPolynomial (Fin 2) K)
(hf : f ≠ 0)
(hker : RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f})
:
A principal image equation of a linear projection has degree at most the source's affine Hilbert degree.
theorem
CCDN.exists_plane_projection_equation_degree_le
{K : Type u_1}
{τ : Type u_2}
[Field K]
[Finite τ]
(I : Ideal (MvPolynomial τ K))
[I.IsPrime]
(a : Fin 2 → MvPolynomial τ K)
(ha : ∀ (i : Fin 2), (a i).totalDegree ≤ 1)
(d : ℕ)
(hdegree : HasFilteredCurveDegree I d)
(j : Fin 2)
(hj : Transcendental K ((Ideal.Quotient.mk I) (a j)))
:
∃ (f : MvPolynomial (Fin 2) K),
Irreducible f ∧ 0 < f.totalDegree ∧ f.totalDegree ≤ d ∧ ∀ (g : MvPolynomial (Fin 2) K), (MvPolynomial.aeval a) g ∈ I ↔ f ∣ g
A linear plane projection with a transcendental coordinate has an irreducible equation of positive degree at most d and no extra kernel relations.