Closed Frobenius reduction for affine plane curves

This module conjugates first-coordinate deflation by the coordinate swap and thereby handles either inseparable coordinate. An absolutely irreducible plane equation over a finite field either has an absent coordinate, in which case its affine point count is exactly the field cardinality, or it admits a same-count equation with both coordinate partial derivatives nonzero and no larger supplied bidegree bounds.

noncomputable def BGS.HasseWeil.planeSwapAlgEquiv (R : Type u_1) [CommRing R] : MvPolynomial (Fin 2) R ≃ₐ[R] MvPolynomial (Fin 2) R

Swap the two variables of a plane polynomial.

Equations

• BGS.HasseWeil.planeSwapAlgEquiv R = MvPolynomial.renameEquiv R (Equiv.swap 0 1)

@[simp]

theorem BGS.HasseWeil.planeSwapAlgEquiv_apply (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (planeSwapAlgEquiv R) f = (MvPolynomial.rename ⇑(Equiv.swap 0 1)) f

theorem BGS.HasseWeil.pderiv_zero_planeSwapAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (MvPolynomial.pderiv 0) ((planeSwapAlgEquiv R) f) = (planeSwapAlgEquiv R) ((MvPolynomial.pderiv 1) f)

theorem BGS.HasseWeil.pderiv_one_planeSwapAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (MvPolynomial.pderiv 1) ((planeSwapAlgEquiv R) f) = (planeSwapAlgEquiv R) ((MvPolynomial.pderiv 0) f)

theorem BGS.HasseWeil.pderiv_zero_planeSwapAlgEquiv_ne_zero (R : Type u_1) [CommRing R] {f : MvPolynomial (Fin 2) R} (hf : (MvPolynomial.pderiv 1) f ≠ 0) : (MvPolynomial.pderiv 0) ((planeSwapAlgEquiv R) f) ≠ 0

theorem BGS.HasseWeil.pderiv_one_planeSwapAlgEquiv_ne_zero (R : Type u_1) [CommRing R] {f : MvPolynomial (Fin 2) R} (hf : (MvPolynomial.pderiv 0) f ≠ 0) : (MvPolynomial.pderiv 1) ((planeSwapAlgEquiv R) f) ≠ 0

theorem BGS.HasseWeil.degreeOf_zero_planeSwapAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : MvPolynomial.degreeOf 0 ((planeSwapAlgEquiv R) f) = MvPolynomial.degreeOf 1 f

theorem BGS.HasseWeil.hasBidegreeAtMost_planeSwapAlgEquiv (R : Type u_1) [CommRing R] {f : MvPolynomial (Fin 2) R} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : External.HasBidegreeAtMost ((planeSwapAlgEquiv R) f) secondDegree firstDegree

theorem BGS.HasseWeil.map_planeSwapAlgEquiv (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) (f : MvPolynomial (Fin 2) R) : (MvPolynomial.map φ) ((planeSwapAlgEquiv R) f) = (planeSwapAlgEquiv S) ((MvPolynomial.map φ) f)

theorem BGS.HasseWeil.absolutelyIrreducible_planeSwapAlgEquiv {K : Type u_2} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) ((planeSwapAlgEquiv K) f))

theorem BGS.HasseWeil.eval_planeSwapAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) (x y : R) : (MvPolynomial.eval ![y, x]) ((planeSwapAlgEquiv R) f) = (MvPolynomial.eval ![x, y]) f

def BGS.HasseWeil.planeSwapAffineZeroEquiv (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : ↥(External.affinePlaneCurveZeros K ((planeSwapAlgEquiv K) f)) ≃ ↥(External.affinePlaneCurveZeros K f)

The affine equivalence swapping the two plane coordinates at the zero fiber.

Equations

• BGS.HasseWeil.planeSwapAffineZeroEquiv K f = (Equiv.prodComm K K).subtypeEquiv ⋯

theorem BGS.HasseWeil.card_affinePlaneCurveZeros_planeSwapAlgEquiv (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : (External.affinePlaneCurveZeros K ((planeSwapAlgEquiv K) f)).card = (External.affinePlaneCurveZeros K f).card

theorem BGS.HasseWeil.separatingFrobeniusDeflation_or_exactPointCount (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : (External.affinePlaneCurveZeros K f).card = Fintype.card K ∨ ∃ (g : MvPolynomial (Fin 2) K), External.HasBidegreeAtMost g firstDegree secondDegree ∧ Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) g) ∧ (MvPolynomial.pderiv 0) g ≠ 0 ∧ (MvPolynomial.pderiv 1) g ≠ 0 ∧ (External.affinePlaneCurveZeros K g).card = (External.affinePlaneCurveZeros K f).card

Frobenius deflation in whichever coordinate is inseparable. The only alternative to a same-count separating equation is the exact univariate point count.

theorem BGS.HasseWeil.abs_affinePlaneCurveZeros_card_sub_card_le_of_separating_case (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hseparating : ∀ (g : MvPolynomial (Fin 2) K), External.HasBidegreeAtMost g firstDegree secondDegree → Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) g) → (MvPolynomial.pderiv 0) g ≠ 0 → (MvPolynomial.pderiv 1) g ≠ 0 → |↑(External.affinePlaneCurveZeros K g).card - ↑(Fintype.card K)| ≤ 8 * √↑(Fintype.card K) * ↑firstDegree * ↑secondDegree) : |↑(External.affinePlaneCurveZeros K f).card - ↑(Fintype.card K)| ≤ 8 * √↑(Fintype.card K) * ↑firstDegree * ↑secondDegree

Any coefficient-8 affine Hasse bound proved for separating equations extends to every absolutely irreducible plane equation. This theorem is the composition boundary between Frobenius reduction and the zeta/spectral argument.