An explicit relation between powered plane-curve coordinates

Let F = L^p, u = x^m, and v = y^n. When n is prime to p, the element v is a primitive element of L / F. Its power basis therefore writes u as a unique polynomial P(v) of degree less than p. This file constructs that polynomial and the linear elimination relation

G(U,V) = U - P(V).

The relation is irreducible over F[V], has exact bidegree (1, degree P), satisfies the coefficient-degree bound used by the Corvaja--Zannier resultant argument, and vanishes at (u,v). The final theorem feeds these facts into Proposition 1 without leaving an unspecified relation polynomial as a hypothesis.

noncomputable def BGS.CorvajaZannier.powerBasisCoordinatePolynomial {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : Polynomial F

The unique bounded-degree coordinate polynomial of u in a chosen power basis generated by v.

Equations

• BGS.CorvajaZannier.powerBasisCoordinatePolynomial pb u = Classical.choose ⋯

theorem BGS.CorvajaZannier.powerBasisCoordinatePolynomial_natDegree_lt {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : (powerBasisCoordinatePolynomial pb u).natDegree < pb.dim

theorem BGS.CorvajaZannier.powerBasisCoordinatePolynomial_aeval {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : u = (Polynomial.aeval pb.gen) (powerBasisCoordinatePolynomial pb u)

theorem BGS.CorvajaZannier.powerBasisCoordinatePolynomial_natDegree_pos_of_not_mem_range {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) (hu : u ∉ Set.range ⇑(algebraMap F L)) : 0 < (powerBasisCoordinatePolynomial pb u).natDegree

noncomputable def BGS.CorvajaZannier.powerBasisEliminationRelation {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : Polynomial (Polynomial F)

The linear elimination relation U - P(V).

Equations

• BGS.CorvajaZannier.powerBasisEliminationRelation pb u = Polynomial.X - Polynomial.C (BGS.CorvajaZannier.powerBasisCoordinatePolynomial pb u)

theorem BGS.CorvajaZannier.powerBasisEliminationRelation_irreducible {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : Irreducible (powerBasisEliminationRelation pb u)

theorem BGS.CorvajaZannier.powerBasisEliminationRelation_natDegree {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : (powerBasisEliminationRelation pb u).natDegree = 1

theorem BGS.CorvajaZannier.transpose_powerBasisEliminationRelation {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : transposeBivariate (powerBasisEliminationRelation pb u) = Polynomial.C Polynomial.X - Polynomial.map Polynomial.C (powerBasisCoordinatePolynomial pb u)

theorem BGS.CorvajaZannier.transpose_powerBasisEliminationRelation_natDegree {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : (transposeBivariate (powerBasisEliminationRelation pb u)).natDegree = (powerBasisCoordinatePolynomial pb u).natDegree

theorem BGS.CorvajaZannier.powerBasisEliminationRelation_coeff_natDegree_le {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) (i : ℕ) : ((powerBasisEliminationRelation pb u).coeff i).natDegree ≤ (powerBasisCoordinatePolynomial pb u).natDegree

theorem BGS.CorvajaZannier.evalBivariate_powerBasisEliminationRelation {F : Type u_1} {L : Type u_2} [Field F] [Field L] [Algebra F L] (pb : PowerBasis F L) (u : L) : evalBivariate pb.gen u (powerBasisEliminationRelation pb u) = 0

noncomputable def BGS.CorvajaZannier.secondPoweredCoordinateFrobeniusPowerBasis {K : Type u_3} [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) : PowerBasis (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (PlaneCurveFunctionField f)

The canonical Frobenius power basis generated by the powered second coordinate of an irreducible plane curve.

Equations

• BGS.CorvajaZannier.secondPoweredCoordinateFrobeniusPowerBasis hf hpartialFirst n hn = PowerBasis.ofAdjoinEqTop ⋯ ⋯

theorem BGS.CorvajaZannier.secondPoweredCoordinateFrobeniusPowerBasis_gen {K : Type u_3} [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) : (secondPoweredCoordinateFrobeniusPowerBasis hf hpartialFirst n hn).gen = planeCurveFunction f 1 ^ n

theorem BGS.CorvajaZannier.secondPoweredCoordinateFrobeniusPowerBasis_dim {K : Type u_3} [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) : (secondPoweredCoordinateFrobeniusPowerBasis hf hpartialFirst n hn).dim = p

noncomputable def BGS.CorvajaZannier.poweredCoordinateExpansionPolynomial {K : Type u_3} [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) : Polynomial ↥(frobeniusSubfield (PlaneCurveFunctionField f) p)

The bounded polynomial in y^n representing x^m over the Frobenius subfield.

Equations

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

theorem BGS.CorvajaZannier.poweredCoordinateExpansionPolynomial_natDegree_lt_char {K : Type u_3} [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) : (poweredCoordinateExpansionPolynomial hf hpartialFirst m n hn).natDegree < p

theorem BGS.CorvajaZannier.poweredCoordinateExpansionPolynomial_aeval {K : Type u_3} [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) : planeCurveFunction f 0 ^ m = (Polynomial.aeval (planeCurveFunction f 1 ^ n)) (poweredCoordinateExpansionPolynomial hf hpartialFirst m n hn)

noncomputable def BGS.CorvajaZannier.poweredCoordinateEliminationRelation {K : Type u_3} [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) : Polynomial (Polynomial ↥(frobeniusSubfield (PlaneCurveFunctionField f) p))

The explicit bivariate elimination relation U - P_{m,n}(V) between x^m and y^n.

Equations

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

theorem BGS.CorvajaZannier.poweredCoordinateEliminationRelation_irreducible {K : Type u_3} [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) : Irreducible (poweredCoordinateEliminationRelation hf hpartialFirst m n hn)

theorem BGS.CorvajaZannier.poweredCoordinateEliminationRelation_natDegree {K : Type u_3} [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) : (poweredCoordinateEliminationRelation hf hpartialFirst m n hn).natDegree = 1

theorem BGS.CorvajaZannier.transpose_poweredCoordinateEliminationRelation_natDegree {K : Type u_3} [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) : (transposeBivariate (poweredCoordinateEliminationRelation hf hpartialFirst m n hn)).natDegree = (poweredCoordinateExpansionPolynomial hf hpartialFirst m n hn).natDegree

theorem BGS.CorvajaZannier.poweredCoordinateEliminationRelation_coeff_natDegree_le {K : Type u_3} [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) (i : ℕ) : ((poweredCoordinateEliminationRelation hf hpartialFirst m n hn).coeff i).natDegree ≤ (poweredCoordinateExpansionPolynomial hf hpartialFirst m n hn).natDegree

theorem BGS.CorvajaZannier.evalBivariate_poweredCoordinateEliminationRelation {K : Type u_3} [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) : evalBivariate (planeCurveFunction f 1 ^ n) (planeCurveFunction f 0 ^ m) (poweredCoordinateEliminationRelation hf hpartialFirst m n hn) = 0

theorem BGS.CorvajaZannier.poweredCoordinateExpansionPolynomial_natDegree_pos {K : Type u_3} [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) : 0 < (poweredCoordinateExpansionPolynomial hf hpartialFirst m n hn).natDegree

If both powered coordinates are separating, the second bidegree of the linear elimination relation is positive as well as strictly below p.

theorem BGS.CorvajaZannier.poweredCoordinates_auxiliaryFamily_linearIndependent_of_elimination {K : Type u_3} [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) (h k : ℕ) (hh : 0 < h) (hk : 0 < k) (hsize : h + (poweredCoordinateExpansionPolynomial hf hpartialFirst m n hn).natDegree * k < p) (hdegree : h < (poweredCoordinateExpansionPolynomial hf hpartialFirst m n hn).natDegree) : LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n) h k)

Proposition 1 for powered plane coordinates with the defining relation constructed internally. The only remaining numerical hypotheses refer to the actual second degree of the canonical elimination polynomial.