The Corvaja--Zannier source-to-powered-image index bound

This module transports the Galois stabilizer count from algebraically closed constants back to the original constant field. Absolute irreducibility makes the powered-image degree invariant under this extension of constants, while the semantic non-subtorus hypothesis supplies the rank-two support determinant.

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le_twice_bidegree_of_nonzero_natCast {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hnot : External.TorusCurveNotSubtorusTranslate f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmK : ↑m ≠ 0) (hnK : ↑n ≠ 0) : have hf := ⋯; Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

The exact source-to-powered-image bound, with separability of the two power maps expressed by nonvanishing of the exponent casts.

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le_twice_bidegree {p : ℕ} {K : Type u_1} [Field K] [CharP K p] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hnot : External.TorusCurveNotSubtorusTranslate 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) : have hf := ⋯; Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

Prime-to-characteristic powers satisfy the exact Corvaja--Zannier source-to-powered-image index bound.