A plane projection of a curve has a nonzero kernel. If one coordinate is transcendental, that kernel is generated by a single irreducible equation.
theorem
CCDN.exists_plane_projection_equation
{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 ∧ RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f}
A linear plane projection with a transcendental coordinate has a principal prime kernel with an irreducible generator.