Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.PlaneAffineFiberBound

Elementary affine plane-curve fiber bounds #

For an irreducible plane curve with positive degree in one coordinate, every fiber in that direction is cut out by a nonzero univariate polynomial. This gives the two elementary bounds

#C(K) ≤ #K * degree_y(f) and #C(K) ≤ #K * degree_x(f).

These estimates handle the large-bidegree branch of the final affine Hasse--Weil theorem, where a trivial fiber count is stronger than carrying normalization error terms.

source
def BGS.HasseWeil.affinePlaneCurvePointEquivSecondCoordinateRoots {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) :
CorvajaZannier.AffinePlaneCurvePoint f ≃ (x : K) × { y : K // Polynomial.eval y (CorvajaZannier.secondCoordinateSpecialization f x) = 0 }

Affine points are the sigma type of their first coordinate and the roots of the corresponding second-coordinate specialization.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGS.HasseWeil.affinePlaneCurvePoint_card_le_card_mul_of_degreeOf_second_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {secondDegree : ℕ} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (hdegreeSecond : MvPolynomial.degreeOf 1 f ≤ secondDegree) :
    Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f) ≤ Fintype.card K * secondDegree

    Counting the roots in every first-coordinate fiber bounds all affine points by the field cardinality times a second-coordinate degree bound.

    source
    theorem BGS.HasseWeil.affinePlaneCurvePoint_card_le_card_mul_secondDegree {K : Type u_1} [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) :
    Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f) ≤ Fintype.card K * secondDegree

    Public bidegree form of the second-coordinate fiber bound.

    source
    def BGS.HasseWeil.affinePlaneCurvePointEquivSwap {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) :
    CorvajaZannier.AffinePlaneCurvePoint f ≃ CorvajaZannier.AffinePlaneCurvePoint (CorvajaZannier.swapPlaneCurveCoordinates f)

    Swapping the two affine coordinates identifies the point sets of f and the coordinate-swapped polynomial.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.HasseWeil.irreducible_swapPlaneCurveCoordinates {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) :
      Irreducible (CorvajaZannier.swapPlaneCurveCoordinates f)

      Coordinate swapping preserves irreducibility.

      source
      theorem BGS.HasseWeil.degreeOf_second_swapPlaneCurveCoordinates {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) :
      MvPolynomial.degreeOf 1 (CorvajaZannier.swapPlaneCurveCoordinates f) = MvPolynomial.degreeOf 0 f

      After swapping, the second-coordinate degree is the original first-coordinate degree.

      source
      theorem BGS.HasseWeil.affinePlaneCurvePoint_card_le_card_mul_firstDegree {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) :
      Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f) ≤ Fintype.card K * firstDegree

      Public bidegree form of the symmetric first-coordinate fiber bound.

      source
      def BGS.HasseWeil.affinePlaneCurveZerosEquivAffinePlaneCurvePoint {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) :
      ↥(External.affinePlaneCurveZeros K f) ≃ CorvajaZannier.AffinePlaneCurvePoint f

      The external finite-set presentation has the same cardinality as the affine-point subtype used by the normalization development.

      Equations
      Instances For
        source
        theorem BGS.HasseWeil.affinePlaneCurveZeros_card_eq_affinePlaneCurvePoint_card {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) :
        (External.affinePlaneCurveZeros K f).card = Fintype.card (CorvajaZannier.AffinePlaneCurvePoint f)