The powered-image auxiliary family with exchanged coordinates

The existing powered-image theorem orients the auxiliary family as (x^m,y^n). Proposition 2 is applied with the smaller source height first, so this module supplies the equally canonical orientation (y^n,x^m). It uses the untransposed powered-image equation and the first-coordinate Frobenius power basis.

theorem BGS.CorvajaZannier.poweredCoordinateFrobeniusImage_auxiliaryFamily_linearIndependent_swapped {K : Type u_1} [Field K] [PerfectField K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmPrime : ¬p ∣ m) (h k : ℕ) (hh : 0 < h) (hk : 0 < k) (hsize : let F := frobeniusSubfield (PlaneCurveFunctionField f) p; have ι := perfectConstantsToFrobeniusSubfield; have g := Polynomial.map (Polynomial.mapRingHom ι) (poweredCoordinateImageRelation hf hpartialSecond m hm n); g.natDegree * h + (transposeBivariate g).natDegree * k < p) (hexcluded : let F := frobeniusSubfield (PlaneCurveFunctionField f) p; have ι := perfectConstantsToFrobeniusSubfield; have g := Polynomial.map (Polynomial.mapRingHom ι) (poweredCoordinateImageRelation hf hpartialSecond m hm n); ¬(g.natDegree ≤ k ∧ (transposeBivariate g).natDegree ≤ h)) : LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 1 ^ n) (planeCurveFunction f 0 ^ m) h k)

Proposition 1 for the powered coordinates in the exchanged orientation. The relation degrees are those of the untransposed powered-image equation.