The zero-coordinate-degree case of Frobenius reduction

An absolutely irreducible plane polynomial with zero degree in one coordinate is a univariate polynomial in the other coordinate. After extension to an algebraic closure, irreducibility forces that univariate polynomial to have degree one. Consequently it has one rational root over the original field and its affine plane zero set has exactly one point above each value of the absent coordinate.

theorem BGS.HasseWeil.natDegree_uniqueAlgEquiv_fin_one {R : Type u_1} [CommRing R] (q : MvPolynomial (Fin 1) R) : ((MvPolynomial.uniqueAlgEquiv R (Fin 1)) q).natDegree = MvPolynomial.degreeOf 0 q

noncomputable def BGS.HasseWeil.secondPolynomialOfFirstDegreeZero {R : Type u_1} [CommRing R] (f : MvPolynomial (Fin 2) R) : Polynomial R

The polynomial obtained by specializing the first variable when its degree is zero.

Equations

• BGS.HasseWeil.secondPolynomialOfFirstDegreeZero f = (MvPolynomial.uniqueAlgEquiv R (Fin 1)) (((MvPolynomial.finSuccEquiv R 1) f).coeff 0)

theorem BGS.HasseWeil.finSuccEquiv_eq_C_coeff_zero_of_degreeOf_zero {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} (hdegree : MvPolynomial.degreeOf 0 f = 0) : (MvPolynomial.finSuccEquiv R 1) f = Polynomial.C (((MvPolynomial.finSuccEquiv R 1) f).coeff 0)

theorem BGS.HasseWeil.degreeOf_one_eq_natDegree_secondPolynomialOfFirstDegreeZero {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} (hdegree : MvPolynomial.degreeOf 0 f = 0) : MvPolynomial.degreeOf 1 f = (secondPolynomialOfFirstDegreeZero f).natDegree

theorem BGS.HasseWeil.degreeOf_map_eq_of_injective_local {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) (hφ : Function.Injective ⇑φ) (i : Fin 2) (f : MvPolynomial (Fin 2) R) : MvPolynomial.degreeOf i ((MvPolynomial.map φ) f) = MvPolynomial.degreeOf i f

theorem BGS.HasseWeil.degreeOf_one_eq_one_of_absolutelyIrreducible_degreeOf_zero {K : Type u_2} [Field K] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hdegree : MvPolynomial.degreeOf 0 f = 0) : MvPolynomial.degreeOf 1 f = 1

theorem BGS.HasseWeil.eval_eq_secondPolynomialOfFirstDegreeZero {R : Type u_1} [CommRing R] {f : MvPolynomial (Fin 2) R} (hdegree : MvPolynomial.degreeOf 0 f = 0) (x y : R) : (MvPolynomial.eval ![x, y]) f = Polynomial.eval y (secondPolynomialOfFirstDegreeZero f)

theorem BGS.HasseWeil.card_affinePlaneCurveZeros_eq_card_of_degreeOf_zero (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hdegree : MvPolynomial.degreeOf 0 f = 0) : (External.affinePlaneCurveZeros K f).card = Fintype.card K