Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.TorsionBidegreeCount

Bidegree bounds for finite torus-curve intersections #

For an irreducible bivariate curve with positive degree in both coordinates, every coordinate fiber is cut out by a nonzero univariate polynomial. Counting roots in each fiber gives the sharp elementary estimates firstOrder * secondDegree and secondOrder * firstDegree; their minimum is the elementary divisor bound used at the Corvaja--Zannier endpoint.

The irreducibility and positive-coordinate-degree hypotheses are essential: a polynomial with a vertical or horizontal component can contain an entire row or column of the torsion grid.

source
noncomputable def BGS.CorvajaZannier.secondCoordinateSpecialization {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (x : K) :
Polynomial K

Specialize the first coordinate of a bivariate polynomial, leaving a univariate polynomial in the second coordinate.

Equations
Instances For
    source
    @[simp]
    theorem BGS.CorvajaZannier.secondCoordinateSpecialization_eval {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (x y : K) :
    Polynomial.eval y (secondCoordinateSpecialization f x) = (MvPolynomial.eval ![x, y]) f
    source
    theorem BGS.CorvajaZannier.secondCoordinateSpecialization_ne_zero_of_irreducible {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (x : K) :
    secondCoordinateSpecialization f x ≠ 0

    An irreducible curve of positive second-coordinate degree has no identically zero fiber over a fixed first coordinate.

    source
    theorem BGS.CorvajaZannier.secondCoordinateSpecialization_natDegree_le {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (x : K) :
    (secondCoordinateSpecialization f x).natDegree ≤ secondDegree

    A support-wise bidegree bound controls every specialized fiber degree.

    source
    theorem BGS.CorvajaZannier.secondCoordinateSpecialization_natDegree_le_degreeOf_second {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (x : K) :
    (secondCoordinateSpecialization f x).natDegree ≤ MvPolynomial.degreeOf 1 f

    Specialization cannot increase the second-coordinate degree.

    source
    theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_card_le_firstOrder_mul_of_degreeOf_second_le {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (secondDegree firstOrder secondOrder : ℕ) (hdegreeSecond : MvPolynomial.degreeOf 1 f ≤ secondDegree) (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (hfirstOrder : 0 < firstOrder) :
    (External.torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ firstOrder * secondDegree

    Fiber counting over first-coordinate roots of unity, stated using an explicit second-coordinate degree bound.

    source
    theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_card_le_firstOrder_mul_secondDegree {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (hfirstOrder : 0 < firstOrder) :
    (External.torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ firstOrder * secondDegree

    The torsion intersection has at most firstOrder * secondDegree points.

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

    Swap the two coordinates of a bivariate polynomial.

    Equations
    Instances For
      source
      @[simp]
      theorem BGS.CorvajaZannier.eval_swapPlaneCurveCoordinates {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (x y : K) :
      (MvPolynomial.eval ![y, x]) (swapPlaneCurveCoordinates f) = (MvPolynomial.eval ![x, y]) f
      source
      def BGS.CorvajaZannier.torusCurveTorsionIntersectionSwapEquiv {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) :
      ↥(External.torusCurveTorsionIntersection K f firstOrder secondOrder) ≃ ↥(External.torusCurveTorsionIntersection K (swapPlaneCurveCoordinates f) secondOrder firstOrder)

      Swapping both curve coordinates and torsion orders preserves the torsion intersection.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_card_swap {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstOrder secondOrder : ℕ) :
        (External.torusCurveTorsionIntersection K f firstOrder secondOrder).card = (External.torusCurveTorsionIntersection K (swapPlaneCurveCoordinates f) secondOrder firstOrder).card

        Coordinate swapping preserves the torsion-intersection cardinality.

        source
        theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_card_le_secondOrder_mul_firstDegree {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hfirst : 0 < MvPolynomial.degreeOf 0 f) (hsecondOrder : 0 < secondOrder) :
        (External.torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ secondOrder * firstDegree

        The torsion intersection has at most secondOrder * firstDegree points.

        source
        theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_card_le_min_bidegree_order_of_irreducible {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hf : Irreducible f) (hfirst : 0 < MvPolynomial.degreeOf 0 f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) :
        (External.torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ min (firstOrder * secondDegree) (secondOrder * firstDegree)

        The sharp elementary bidegree/order bound under the precise algebraic hypotheses needed for fiber counting.

        source
        theorem BGS.CorvajaZannier.torusCurveTorsionIntersection_card_le_min_bidegree_order {K : Type u_2} [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree firstOrder secondOrder : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (hcurve : External.IsCorvajaZannierPlaneCurve f) (hfirstOrder : 0 < firstOrder) (hsecondOrder : 0 < secondOrder) :
        (External.torusCurveTorsionIntersection K f firstOrder secondOrder).card ≤ min (firstOrder * secondDegree) (secondOrder * firstDegree)

        The sharp elementary bidegree/order bound for an admissible torus curve.