Geometric Proposition 2 for a plane curve #
The powered-image linear-independence theorem and the canonical global Wronskian estimate are assembled here. The source-to-image index remains an explicit premise of the two orientation lemmas; the following endpoint module discharges it from the non-subtorus hypothesis.
theorem
BGS.CorvajaZannier.planeCurvePropositionTwo_natural_of_poweredImageIndexBound
{K : Type u_1}
[Field K]
[Fintype K]
[DecidableEq K]
{p : ℕ}
[Fact (Nat.Prime p)]
[CharP K p]
{f : MvPolynomial (Fin 2) K}
(hf : Irreducible f)
(habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f))
(hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0)
(hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
(hnPrime : ¬p ∣ n)
(hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K)
(hindex :
have this := ⋯;
Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)
:
PropositionTwoNumericalAlternatives (n * MvPolynomial.degreeOf 0 f) (m * MvPolynomial.degreeOf 1 f) p
(2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)
↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond m n)
The natural orientation (u,v)=(x^m,y^n) of the geometric Proposition 2
argument.
theorem
BGS.CorvajaZannier.planeCurvePropositionTwo_swapped_of_poweredImageIndexBound
{K : Type u_1}
[Field K]
[Fintype K]
[DecidableEq K]
{p : ℕ}
[Fact (Nat.Prime p)]
[CharP K p]
{f : MvPolynomial (Fin 2) K}
(hf : Irreducible f)
(habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f))
(hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0)
(hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
(hmPrime : ¬p ∣ m)
(hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K)
(hindex :
have this := ⋯;
Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)
:
PropositionTwoNumericalAlternatives (m * MvPolynomial.degreeOf 1 f) (n * MvPolynomial.degreeOf 0 f) p
(2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)
↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond m n)
The swapped orientation (u,v)=(y^n,x^m) of the geometric Proposition 2
argument.
theorem
BGS.CorvajaZannier.planeCurvePropositionTwo_of_poweredImageIndexBound
{K : Type u_1}
[Field K]
[Finite K]
[DecidableEq K]
{p : ℕ}
[Fact (Nat.Prime p)]
[CharP K p]
{f : MvPolynomial (Fin 2) K}
(hf : Irreducible f)
(habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f))
(hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0)
(hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
(hmPrime : ¬p ∣ m)
(hnPrime : ¬p ∣ n)
(hlarge : 12 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f < p)
(hindex :
have this := ⋯;
Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)
:
PropositionTwoNumericalAlternatives
(planeCurveTorsionLowerDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) m n)
(planeCurveTorsionUpperDegree (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f) m n) p
(2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f)
↑(planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond m n)
The two orientations combine to the actual minimum/maximum degree form needed by the plane-curve endpoint.