The source-to-powered-image index over algebraically closed constants

When the power exponents are nonzero in the constant field, the source function field is a Galois extension of the field generated by the two powered coordinates. Its automorphisms act diagonally on the two coordinates. The resulting pair of roots of unity lies in the support-character stabilizer, so a rank-two support determinant bounds the extension degree.

theorem BGS.CorvajaZannier.poweredCoordinateImageField_adjoin_coordinates_eq_top_and_ne_zero {F : Type u_1} [Field F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) : let L := PlaneCurveFunctionField f; let B := PoweredCoordinateImageField f m n; (↥B)⟮planeCurveFunction f 0, planeCurveFunction f 1⟯ = ⊤ ∧ planeCurveFunction f 0 ≠ 0 ∧ planeCurveFunction f 1 ≠ 0

theorem BGS.CorvajaZannier.finiteDimensional_poweredCoordinateImageField {F : Type u_1} [Field F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) : have this := ⋯; FiniteDimensional (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f)

theorem BGS.CorvajaZannier.firstCoordinate_isSeparable_over_poweredCoordinateImageField {F : Type u_1} [Field F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hmF : ↑m ≠ 0) : IsSeparable (↥(PoweredCoordinateImageField f m n)) (planeCurveFunction f 0)

theorem BGS.CorvajaZannier.firstCoordinate_minpoly_splits_over_poweredCoordinateImageField {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (m n : ℕ) (hm : 0 < m) (hmF : ↑m ≠ 0) : (Polynomial.map (algebraMap (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f)) (minpoly (↥(PoweredCoordinateImageField f m n)) (planeCurveFunction f 0))).Splits

theorem BGS.CorvajaZannier.secondCoordinate_isSeparable_over_poweredCoordinateImageField {F : Type u_1} [Field F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (m n : ℕ) (hnF : ↑n ≠ 0) : IsSeparable (↥(PoweredCoordinateImageField f m n)) (planeCurveFunction f 1)

theorem BGS.CorvajaZannier.secondCoordinate_minpoly_splits_over_poweredCoordinateImageField {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (m n : ℕ) (hn : 0 < n) (hnF : ↑n ≠ 0) : (Polynomial.map (algebraMap (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f)) (minpoly (↥(PoweredCoordinateImageField f m n)) (planeCurveFunction f 1))).Splits

theorem BGS.CorvajaZannier.isGalois_over_poweredCoordinateImageField {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmF : ↑m ≠ 0) (hnF : ↑n ≠ 0) : IsGalois (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f)

theorem BGS.CorvajaZannier.exists_support_stabilizer_scaling_of_poweredImage_aut {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmF : ↑m ≠ 0) (hnF : ↑n ≠ 0) (σ : PlaneCurveFunctionField f ≃ₐ[↥(PoweredCoordinateImageField f m n)] PlaneCurveFunctionField f) : ∃ (z : Fˣ × Fˣ), (algebraMap F (PlaneCurveFunctionField f)) ↑z.1 * planeCurveFunction f 0 = σ (planeCurveFunction f 0) ∧ (algebraMap F (PlaneCurveFunctionField f)) ↑z.2 * planeCurveFunction f 1 = σ (planeCurveFunction f 1) ∧ ∀ r ∈ f.support, ∀ s ∈ f.support, z.1 ^ (↑(s 0) - ↑(r 0)) * z.2 ^ (↑(s 1) - ↑(r 1)) = 1

theorem BGS.CorvajaZannier.finrank_poweredCoordinateImageField_le_twice_bidegree_isAlgClosed {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hrank : PlaneCurveSupportHasRankTwo f) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmF : ↑m ≠ 0) (hnF : ↑n ≠ 0) : Module.finrank (↥(PoweredCoordinateImageField f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

theorem BGS.CorvajaZannier.finrank_poweredImageOverFirst_le_twice_bidegree_isAlgClosed {F : Type u_1} [Field F] [IsAlgClosed F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hrank : PlaneCurveSupportHasRankTwo f) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hmF : ↑m ≠ 0) (hnF : ↑n ≠ 0) : Module.finrank (↥(PoweredImageOverFirst f m n)) (PlaneCurveFunctionField f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

The same algebraically closed bound in the first-coordinate presentation used by the Corvaja--Zannier endpoint.