The homogeneous degree of a plane equation agrees with its projective Hilbert degree, giving sharp projective plane intersection bounds.
theorem
CCDN.principal_plane_hasProjectiveCurveDegree
{K : Type u_1}
[Field K]
(f : MvPolynomial (Fin 3) K)
{d : ℕ}
(hf : f.IsHomogeneous d)
(hf0 : f ≠ 0)
:
The ideal generated by a nonzero ternary form of degree d defines a projective plane curve of
degree d, in the sense of its Hilbert polynomial.
theorem
CCDN.projectiveIdealZeroLocus_span_singleton
{K : Type u_1}
[Field K]
{n d : ℕ}
(f : MvPolynomial (Fin (n + 1)) K)
(hf : f.IsHomogeneous d)
:
The projective zero locus of the ideal generated by a homogeneous polynomial f is the
projective zero locus of f.
theorem
CCDN.projective_plane_common_zeros_card_le
{K : Type u_1}
[Field K]
{d m : ℕ}
{ι : Type u_2}
[Fintype ι]
(f g : MvPolynomial (Fin 3) K)
(hf : f.IsHomogeneous d)
(hir : Irreducible f)
(hg : g.IsHomogeneous m)
(hfg : ¬f ∣ g)
(z : ι → Projectivization K (Fin 3 → K))
(hz : Function.Injective z)
(hzf : ∀ (i : ι), z i ∈ projectiveZeroLocus f)
(hzg : ∀ (i : ι), z i ∈ projectiveZeroLocus g)
:
Sharp projective Bézout over any field for an irreducible plane equation and a homogeneous polynomial not divisible by it, including points at infinity.