Separating coordinates are not Frobenius powers

For an irreducible plane curve in characteristic p, a nonzero partial derivative makes the function field separable over the field generated by the opposite coordinate. This file uses that separability to prove that the generating coordinate cannot be a p-th power in the curve function field.

The last step is made explicit in the one-variable rational function field: if (a / b) ^ p = X, then a ^ p = X * b ^ p, whose degrees would satisfy p * degree(a) = 1 + p * degree(b).

theorem BGS.CorvajaZannier.mvPolynomial_variable_not_pow_in_fractionRing {K : Type u_1} {σ : Type u_2} [Field K] (i : σ) (p : ℕ) (hp : 1 < p) : ¬∃ (z : FractionRing (MvPolynomial σ K)), z ^ p = (algebraMap (MvPolynomial σ K) (FractionRing (MvPolynomial σ K))) (MvPolynomial.X i)

A polynomial variable is not a nontrivial power in the fraction field of a multivariate polynomial ring.

theorem BGS.CorvajaZannier.firstCoordinateInSubfield_not_pow {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hsecond : 0 < MvPolynomial.degreeOf 1 f) (p : ℕ) (hp : 1 < p) : ¬∃ (z : ↥(FirstCoordinateSubfield f)), z ^ p = firstCoordinateInSubfield f

The first coordinate has no nontrivial power root in the field it generates over the constant field.

theorem BGS.CorvajaZannier.secondCoordinateInSubfield_not_pow {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hfirst : 0 < MvPolynomial.degreeOf 0 f) (p : ℕ) (hp : 1 < p) : ¬∃ (z : ↥(SecondCoordinateSubfield f)), z ^ p = secondCoordinateInSubfield f

The second coordinate has no nontrivial power root in the field it generates over the constant field.

theorem BGS.CorvajaZannier.firstCoordinate_not_mem_frobeniusSubfield {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : planeCurveFunction f 0 ∉ frobeniusSubfield (PlaneCurveFunctionField f) p

A first coordinate that is separating (equivalently here, the other partial derivative is nonzero) is not a p-th power in the plane-curve function field.

theorem BGS.CorvajaZannier.secondCoordinate_not_mem_frobeniusSubfield {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) : planeCurveFunction f 1 ∉ frobeniusSubfield (PlaneCurveFunctionField f) p

A second coordinate that is separating (equivalently here, the other partial derivative is nonzero) is not a p-th power in the plane-curve function field.