Absolute irreducibility forces rank-two torus support

This file proves the support-lattice bridge needed by the diagonal-stabilizer route to the Corvaja--Zannier powered-image index bound. A collinear finite support lies in a translate of a cyclic subgroup of ℤ²; the corresponding plane polynomial is a monomial times a directional homogenization of a univariate polynomial. Over an algebraically closed field, irreducibility forces that univariate polynomial to have degree one, so a nonzero torus character is constant on the curve. This contradicts the semantic TorusCurveNotSubtorusTranslate hypothesis.

def BGS.CorvajaZannier.planeExponentDifference (r s : Fin 2 →₀ ℕ) : Fin 2 → ℤ

The signed coordinate difference between two plane monomial exponents.

Equations

• BGS.CorvajaZannier.planeExponentDifference r s i = ↑(s i) - ↑(r i)

theorem BGS.CorvajaZannier.exists_support_direction_of_not_rankTwo {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {r : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hnrank : ¬PlaneCurveSupportHasRankTwo f) (hnonsingleton : ∃ s ∈ f.support, s ≠ r) : ∃ (v : Fin 2 → ℤ), v ≠ 0 ∧ ∀ s ∈ f.support, ∃ (k : ℤ), planeExponentDifference r s = k • v

theorem BGS.CorvajaZannier.planeCurveSupportHasRankTwo_of_absoluteIrreducible_notSubtorusTranslate {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hirr : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hnot : External.TorusCurveNotSubtorusTranslate f) : PlaneCurveSupportHasRankTwo f

Absolute irreducibility and the semantic non-subtorus condition force the support lattice of a plane torus curve to have rank two.

theorem BGS.CorvajaZannier.planeCurveSupportHasRankTwo_map_of_injective {K : Type u_1} {E : Type u_2} [Field K] [Field E] (ι : K →+* E) (hι : Function.Injective ⇑ι) {f : MvPolynomial (Fin 2) K} (hrank : PlaneCurveSupportHasRankTwo f) : PlaneCurveSupportHasRankTwo ((MvPolynomial.map ι) f)

Injective extension of coefficients preserves a rank-two support certificate.