A primitive plane coordinate gives a lower bound for the image equation's degree. Combined with the filtered upper bound, a parameter of full field degree forces a linear projection to preserve the affine Hilbert degree.
theorem
CCDN.plane_projection_degree_eq_of_full_parameter
{K : Type u_1}
{R : Type u_2}
{F : Type u_3}
{τ : Type u_4}
[Field K]
[Field R]
[Field F]
[Algebra K R]
[Algebra R F]
[Algebra K F]
[IsScalarTower K R F]
[Module.Finite R F]
[Finite τ]
(I : Ideal (MvPolynomial τ K))
(a : Fin 2 → MvPolynomial τ K)
(ha : ∀ (i : Fin 2), (a i).totalDegree ≤ 1)
(d : ℕ)
(hdegree : HasFilteredCurveDegree I d)
(φ : MvPolynomial τ K ⧸ I →ₐ[K] F)
(f : MvPolynomial (Fin 2) K)
(hf : f ≠ 0)
(hker : RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f})
(j k : Fin 2)
(u : R)
(hu : Transcendental K u)
(he : φ ((Ideal.Quotient.mk I) (a j)) = (algebraMap R F) u)
(hprim : R⟮φ ((Ideal.Quotient.mk I) (a k))⟯ = ⊤)
(hrank : Module.finrank R F = d)
:
Once the linear parameter has full field degree and the other coordinate is primitive, the irreducible image equation preserves degree.