Prime-to-characteristic powers of plane-curve coordinates

Corvaja--Zannier's plane torsion corollary applies the function-field theorem to powers of the two coordinate functions. This file makes the algebraic part of that passage explicit. A positive power preserves the geometric nonconstancy of every character. If the exponent is prime to the characteristic, a separating coordinate power generates the function field over its Frobenius subfield, has nonzero differential, and has minimal polynomial of degree exactly the characteristic.

The last theorem applies the already-proved resultant form of Proposition 1 to powered coordinates once an explicit irreducible relation between those powers is supplied. Constructing that elimination relation, and controlling its bidegrees, remains a separate algebraic-geometric step; it is not assumed implicitly here.

def BGS.CorvajaZannier.PoweredTorusCurveNotSubtorusTranslate {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (m n : ℕ) : Prop

No nontrivial character in the powered coordinates is constant on the geometric torus curve.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.CorvajaZannier.poweredTorusCurveNotSubtorusTranslate {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (hnot : External.TorusCurveNotSubtorusTranslate f) : PoweredTorusCurveNotSubtorusTranslate f m n

Positive coordinate powers preserve the source's multiplicative independence-modulo-constants condition.

theorem BGS.CorvajaZannier.adjoin_pow_eq_adjoin_of_coprime {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (z : L) (hz : z ≠ 0) (p m : ℕ) (hcop : m.Coprime p) (hzp : z ^ p ∈ F⟮z ^ m⟯) : F⟮z ^ m⟯ = F⟮z⟯

If m is coprime to p, adjoining z ^ m is the same as adjoining z, provided the p-th power of z is already in the smaller field.

The reverse inclusion is the explicit Bézout identity a * m + b * p = 1, interpreted using integer powers in the ambient field.

theorem BGS.CorvajaZannier.adjoin_frobeniusSubfield_pow_eq_top {L : Type u_1} [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ≠ 0) (m : ℕ) (hm : ¬p ∣ m) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : (↥(frobeniusSubfield L p))⟮z ^ m⟯ = ⊤

A prime-to-characteristic power of a Frobenius-separating generator is again a generator over the Frobenius subfield.

theorem BGS.CorvajaZannier.derivation_pow_ne_zero_of_not_dvd {C : Type u_1} {L : Type u_2} [CommRing C] [Field L] [Algebra C L] {p : ℕ} [CharP L p] (D : Derivation C L L) (z : L) (m : ℕ) (hm : ¬p ∣ m) (hz : z ≠ 0) (hDz : D z ≠ 0) : D (z ^ m) ≠ 0

A prime-to-characteristic power of a function with nonzero derivative again has nonzero derivative.

theorem BGS.CorvajaZannier.exists_derivation_power_ne_zero_with_exact_frobenius_constants {L : Type u_1} [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ≠ 0) (hzNot : z ∉ frobeniusSubfield L p) (m : ℕ) (hm : ¬p ∣ m) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : ∃ (D : Derivation (↥(frobeniusSubfield L p)) L L), D (z ^ m) ≠ 0 ∧ ∀ (w : L), D w = 0 ↔ ∃ (c : ↥(frobeniusSubfield L p)), (algebraMap (↥(frobeniusSubfield L p)) L) c = w

The exact-constants derivation associated to z also detects every prime-to-characteristic power of z.

theorem BGS.CorvajaZannier.frobeniusPower_not_mem {L : Type u_1} [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ≠ 0) (hzNot : z ∉ frobeniusSubfield L p) (m : ℕ) (hm : ¬p ∣ m) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : z ^ m ∉ frobeniusSubfield L p

A prime-to-characteristic power of a Frobenius-separating element is not itself a Frobenius power.

theorem BGS.CorvajaZannier.frobeniusPower_minpoly_natDegree_eq_char {L : Type u_1} [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ≠ 0) (hzNot : z ∉ frobeniusSubfield L p) (m : ℕ) (hm : ¬p ∣ m) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : (minpoly (↥(frobeniusSubfield L p)) (z ^ m)).natDegree = p

The minimal polynomial of a prime-to-characteristic power of a Frobenius-separating element still has degree exactly p over L^p.

theorem BGS.CorvajaZannier.firstCoordinatePow_transcendental {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) {m : ℕ} (hm : 0 < m) : Transcendental K (planeCurveFunction f 0 ^ m)

A positive power of the first coordinate remains transcendental over the constant field.

theorem BGS.CorvajaZannier.secondCoordinatePow_transcendental {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) {n : ℕ} (hn : 0 < n) : Transcendental K (planeCurveFunction f 1 ^ n)

A positive power of the second coordinate remains transcendental over the constant field.

theorem BGS.CorvajaZannier.adjoin_frobeniusSubfield_firstCoordinatePow_eq_top {K : Type u_1} [Field K] [PerfectField K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : ¬p ∣ m) : (↥(frobeniusSubfield (PlaneCurveFunctionField f) p))⟮planeCurveFunction f 0 ^ m⟯ = ⊤

The first powered coordinate alone generates the curve function field over its Frobenius subfield.

theorem BGS.CorvajaZannier.adjoin_frobeniusSubfield_secondCoordinatePow_eq_top {K : Type u_1} [Field K] [PerfectField K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (n : ℕ) (hn : ¬p ∣ n) : (↥(frobeniusSubfield (PlaneCurveFunctionField f) p))⟮planeCurveFunction f 1 ^ n⟯ = ⊤

The second powered coordinate alone generates the curve function field over its Frobenius subfield.

theorem BGS.CorvajaZannier.minpoly_firstCoordinatePow_natDegree_eq_char {K : Type u_1} [Field K] [PerfectField K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : ¬p ∣ m) : (minpoly (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (planeCurveFunction f 0 ^ m)).natDegree = p

Exact Frobenius-subfield degree of the first powered coordinate.

theorem BGS.CorvajaZannier.minpoly_secondCoordinatePow_natDegree_eq_char {K : Type u_1} [Field K] [PerfectField K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (n : ℕ) (hn : ¬p ∣ n) : (minpoly (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (planeCurveFunction f 1 ^ n)).natDegree = p

Exact Frobenius-subfield degree of the second powered coordinate.

theorem BGS.CorvajaZannier.exists_derivation_coordinatePowers_ne_zero {K : Type u_1} [Field K] [PerfectField K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : ¬p ∣ m) (hn : ¬p ∣ n) : ∃ (D : Derivation (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (PlaneCurveFunctionField f) (PlaneCurveFunctionField f)), D (planeCurveFunction f 0 ^ m) ≠ 0 ∧ D (planeCurveFunction f 1 ^ n) ≠ 0 ∧ ∀ (z : PlaneCurveFunctionField f), D z = 0 ↔ ∃ (c : ↥(frobeniusSubfield (PlaneCurveFunctionField f) p)), (algebraMap (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (PlaneCurveFunctionField f)) c = z

One derivation with exact constant field L^p detects both powered plane coordinates. This is the differential hypothesis required by the torsion specialization.

theorem BGS.CorvajaZannier.poweredCoordinates_auxiliaryFamily_linearIndependent_of_relation {K : Type u_1} [Field K] [PerfectField K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (m n : ℕ) (hn : ¬p ∣ n) (g : Polynomial (Polynomial ↥(frobeniusSubfield (PlaneCurveFunctionField f) p))) (a b h k : ℕ) : 0 < a → 0 < h → 0 < k → Irreducible g → g.natDegree = a → (transposeBivariate g).natDegree = b → (∀ (i : ℕ), (g.coeff i).natDegree ≤ b) → evalBivariate (planeCurveFunction f 1 ^ n) (planeCurveFunction f 0 ^ m) g = 0 → a * h + b * k < p → ¬(a ≤ k ∧ b ≤ h) → LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n) h k)

Proposition 1 for powered plane coordinates, with all Frobenius and separability obligations discharged. The remaining polynomial g is an explicit relation between the powers; its irreducibility and bidegrees are kept visible because constructing it is the genuine elimination frontier.