Plane-curve degrees versus finite-field cardinality

This file converts the characteristic bound used in the Corvaja--Zannier argument into the finite-field cardinality bounds required by the local reciprocal-discriminant and canonical Euler estimates.

theorem BGS.CorvajaZannier.prime_le_fintype_card_of_charP {K : Type u_1} [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : p ≤ Fintype.card K

The prime characteristic of a finite field is at most its cardinality.

theorem BGS.CorvajaZannier.planeCurve_coordinateDegrees_lt_char_of_twelve_mul_degrees_lt_char {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {p : ℕ} (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hbound : 12 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f < p) : MvPolynomial.degreeOf 0 f < p ∧ MvPolynomial.degreeOf 1 f < p

If twelve times the product of the two coordinate degrees is smaller than p, and both coordinate partial derivatives are nonzero, then each coordinate degree is smaller than p.

theorem BGS.CorvajaZannier.planeCurve_coordinateDegrees_lt_card_of_twelve_mul_degrees_lt_char {K : Type u_1} [Field K] [Fintype K] {f : MvPolynomial (Fin 2) K} {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hbound : 12 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f < p) : MvPolynomial.degreeOf 0 f < Fintype.card K ∧ MvPolynomial.degreeOf 1 f < Fintype.card K

Under the characteristic-size hypothesis of the Corvaja--Zannier application, both coordinate degrees are strictly smaller than the cardinality of the finite constant field.

theorem BGS.CorvajaZannier.planeCurve_degreeOf_first_lt_card_of_twelve_mul_degrees_lt_char {K : Type u_1} [Field K] [Fintype K] {f : MvPolynomial (Fin 2) K} {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hbound : 12 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f < p) : MvPolynomial.degreeOf 0 f < Fintype.card K

First-coordinate specialization of planeCurve_coordinateDegrees_lt_card_of_twelve_mul_degrees_lt_char.

theorem BGS.CorvajaZannier.planeCurve_degreeOf_second_lt_card_of_twelve_mul_degrees_lt_char {K : Type u_1} [Field K] [Fintype K] {f : MvPolynomial (Fin 2) K} {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hbound : 12 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f < p) : MvPolynomial.degreeOf 1 f < Fintype.card K

Second-coordinate specialization of planeCurve_coordinateDegrees_lt_card_of_twelve_mul_degrees_lt_char.