A coarse affine singular-point bound for plane curves

For a bivariate polynomial f, write it as a polynomial F in the second coordinate with coefficients in the first-coordinate polynomial ring. We eliminate the second coordinate from F and F.derivative by their ordinary resultant, with the two degree parameters fixed before specialization.

Fixing those parameters is essential: specializing the first coordinate can lower the degree, so neither a default resultant whose parameters are chosen after specialization nor a specialized discriminant is the correct object. The fixed resultant nevertheless vanishes at the first coordinate of every common zero of f and its second partial derivative. Irreducibility and a nonzero second partial derivative make the resultant nonzero, and elementary root and fiber counts then bound all affine singular points by ((2 * secondDegree - 1) * firstDegree) * secondDegree.

theorem BGS.HasseWeil.planeCurvePolynomialInSecondCoordinate_derivative {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Polynomial.derivative (CorvajaZannier.planeCurvePolynomialInSecondCoordinate f) = CorvajaZannier.planeCurvePolynomialInSecondCoordinate ((MvPolynomial.pderiv 1) f)

noncomputable def BGS.HasseWeil.secondCoordinateCriticalResultant {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Polynomial K

The first-coordinate eliminant of the equation and its derivative in the second coordinate.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.HasseWeil.secondCoordinateCriticalResultant_natDegree_le {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : (secondCoordinateCriticalResultant f).natDegree ≤ (2 * secondDegree - 1) * firstDegree

theorem BGS.HasseWeil.secondCoordinateCriticalResultant_eval_eq_zero_of_common_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (x y : K) (hfxy : (MvPolynomial.eval ![x, y]) f = 0) (hderivxy : (MvPolynomial.eval ![x, y]) ((MvPolynomial.pderiv 1) f) = 0) : Polynomial.eval x (secondCoordinateCriticalResultant f) = 0

theorem BGS.HasseWeil.secondCoordinateCriticalResultant_ne_zero {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : secondCoordinateCriticalResultant f ≠ 0

noncomputable def BGS.HasseWeil.affineSecondCoordinateCriticalPoints (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : Finset (K × K)

Affine points where the curve equation and its second-coordinate derivative vanish. This set contains every affine singular point.

Equations

• BGS.HasseWeil.affineSecondCoordinateCriticalPoints K f = {z : K × K | (MvPolynomial.eval ![z.1, z.2]) f = 0 ∧ (MvPolynomial.eval ![z.1, z.2]) ((MvPolynomial.pderiv 1) f) = 0}

@[simp]

theorem BGS.HasseWeil.mem_affineSecondCoordinateCriticalPoints_iff {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {z : K × K} : z ∈ affineSecondCoordinateCriticalPoints K f ↔ (MvPolynomial.eval ![z.1, z.2]) f = 0 ∧ (MvPolynomial.eval ![z.1, z.2]) ((MvPolynomial.pderiv 1) f) = 0

noncomputable def BGS.HasseWeil.affinePlaneCurveSingularPoints (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : Finset (K × K)

Affine singular points: the equation and both coordinate partial derivatives vanish.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.HasseWeil.mem_affinePlaneCurveSingularPoints_iff {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {z : K × K} : z ∈ affinePlaneCurveSingularPoints K f ↔ (MvPolynomial.eval ![z.1, z.2]) f = 0 ∧ (MvPolynomial.eval ![z.1, z.2]) ((MvPolynomial.pderiv 0) f) = 0 ∧ (MvPolynomial.eval ![z.1, z.2]) ((MvPolynomial.pderiv 1) f) = 0

theorem BGS.HasseWeil.polynomialEvalZeroSubtype_card_le_natDegree {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (P : Polynomial K) (hP : P ≠ 0) : Fintype.card { x : K // Polynomial.eval x P = 0 } ≤ P.natDegree

theorem BGS.HasseWeil.affineSecondCoordinateCriticalPoints_card_le {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : (affineSecondCoordinateCriticalPoints K f).card ≤ (2 * secondDegree - 1) * firstDegree * secondDegree

theorem BGS.HasseWeil.affinePlaneCurveSingularPoints_card_le {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : (affinePlaneCurveSingularPoints K f).card ≤ (2 * secondDegree - 1) * firstDegree * secondDegree

A coarse bidegree bound for the number of affine singular points of an irreducible separating plane curve.