The plane-curve auxiliary family over the Frobenius subfield

This file specializes the algebraic resultant argument in BivariateGauss.lean to the function field of an irreducible affine plane curve over a perfect field of prime characteristic. Constants are embedded in the Frobenius subfield L^p, and separability over a coordinate rational subfield is promoted to separability over L^p adjoined with that coordinate.

The only irreducibility hypothesis retained at the final boundary is the literal base change of the defining equation from the constant field to L^p. This is the precise consequence of absolute irreducibility used in Corvaja--Zannier's Proposition 1; it is not replaced by an unrelated typeclass or by an axiom.

Source provenance: published pages 1933--1934; checked semantic reconstruction Papers/CorvajaZannier2013/CorvajaZannier2013.tex, lines 486--571. The specialization with Frobenius exponent p and no auxiliary twists is the linear-independence input cited on published page 1940.

noncomputable def BGS.CorvajaZannier.planeCurveToBivariate (K : Type u_1) [Field K] : MvPolynomial (Fin 2) K ≃ₐ[K] Polynomial (Polynomial K)

View a polynomial in affine coordinates 0,1 as a polynomial in coordinate 0 whose coefficients are ordinary polynomials in coordinate 1.

Equations

• BGS.CorvajaZannier.planeCurveToBivariate K = (MvPolynomial.finSuccEquiv K 1).trans (Polynomial.mapAlgEquiv (MvPolynomial.uniqueAlgEquiv K (Fin 1)))

@[simp]

theorem BGS.CorvajaZannier.planeCurveToBivariate_X_zero (K : Type u_1) [Field K] : (planeCurveToBivariate K) (MvPolynomial.X 0) = Polynomial.X

@[simp]

theorem BGS.CorvajaZannier.planeCurveToBivariate_X_one (K : Type u_1) [Field K] : (planeCurveToBivariate K) (MvPolynomial.X 1) = Polynomial.C Polynomial.X

@[simp]

theorem BGS.CorvajaZannier.planeCurveToBivariate_C (K : Type u_1) [Field K] (c : K) : (planeCurveToBivariate K) (MvPolynomial.C c) = Polynomial.C (Polynomial.C c)

theorem BGS.CorvajaZannier.planeCurveToBivariate_natDegree_eq_degreeOf_zero (K : Type u_1) [Field K] (f : MvPolynomial (Fin 2) K) : ((planeCurveToBivariate K) f).natDegree = MvPolynomial.degreeOf 0 f

The outer degree of the source-oriented iterated presentation is exactly the degree in coordinate 0.

theorem BGS.CorvajaZannier.transposeBivariate_planeCurveToBivariate (K : Type u_1) [Field K] (f : MvPolynomial (Fin 2) K) : transposeBivariate ((planeCurveToBivariate K) f) = (Polynomial.Bivariate.equivMvPolynomial K).symm f

Transposing the source-oriented iterated presentation gives the standard bivariate-polynomial presentation.

theorem BGS.CorvajaZannier.bivariateEquiv_symm_natDegree_eq_degreeOf_one (K : Type u_1) [Field K] (f : MvPolynomial (Fin 2) K) : ((Polynomial.Bivariate.equivMvPolynomial K).symm f).natDegree = MvPolynomial.degreeOf 1 f

The outer degree in the standard bivariate presentation is exactly the degree in coordinate 1.

theorem BGS.CorvajaZannier.degreeOf_map_eq_of_injective {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] (ι : R →+* S) (hι : Function.Injective ⇑ι) (i : σ) (f : MvPolynomial σ R) : MvPolynomial.degreeOf i ((MvPolynomial.map ι) f) = MvPolynomial.degreeOf i f

An injective change of coefficients preserves every coordinate degree.

noncomputable def BGS.CorvajaZannier.planeCurveFrobeniusRelation {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (f : MvPolynomial (Fin 2) K) : Polynomial (Polynomial ↥(frobeniusSubfield L p))

The defining plane equation after extension of constants from K to the Frobenius subfield L^p, in the iterated-polynomial orientation used by the resultant proof.

Equations

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

theorem BGS.CorvajaZannier.planeCurveFrobeniusRelation_natDegree {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (f : MvPolynomial (Fin 2) K) : (planeCurveFrobeniusRelation f).natDegree = MvPolynomial.degreeOf 0 f

The first exact bidegree of the Frobenius-base-changed relation.

theorem BGS.CorvajaZannier.transposeBivariate_planeCurveFrobeniusRelation_natDegree {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (f : MvPolynomial (Fin 2) K) : (transposeBivariate (planeCurveFrobeniusRelation f)).natDegree = MvPolynomial.degreeOf 1 f

The second exact bidegree of the Frobenius-base-changed relation.

theorem BGS.CorvajaZannier.evalBivariate_planeCurveFrobeniusRelation {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (f : MvPolynomial (Fin 2) K) (x y : L) : evalBivariate y x (planeCurveFrobeniusRelation f) = MvPolynomial.eval₂ (algebraMap K L) ![x, y] f

Evaluation of the Frobenius-base-changed relation agrees with direct evaluation of the original plane equation.

theorem BGS.CorvajaZannier.planeCurveFrobeniusRelation_irreducible {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] {f : MvPolynomial (Fin 2) K} (hbaseChange : Irreducible ((MvPolynomial.map perfectConstantsToFrobeniusSubfield) f)) : Irreducible (planeCurveFrobeniusRelation f)

Irreducibility after the precise constant-field extension to L^p implies irreducibility in the iterated-polynomial presentation.

theorem BGS.CorvajaZannier.isSeparable_over_frobeniusAdjoin_of_isSeparable_over_constantAdjoin {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (z : L) [Algebra.IsSeparable (↥K⟮z⟯) L] : Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L

Extending the base from the perfect constant field to the Frobenius subfield preserves separability of the remaining top extension.

theorem BGS.CorvajaZannier.minpoly_natDegree_over_frobeniusSubfield_eq_char {L : Type u_2} [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ∉ frobeniusSubfield L p) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : (minpoly (↥(frobeniusSubfield L p)) z).natDegree = p

A separating element has minimal polynomial of exact degree p over the Frobenius subfield.

theorem BGS.CorvajaZannier.planeCurve_auxiliaryFamily_linearIndependent {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (_hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (a b h k : ℕ) : 0 < a → 0 < h → 0 < k → Irreducible ((MvPolynomial.map perfectConstantsToFrobeniusSubfield) f) → (planeCurveFrobeniusRelation f).natDegree = a → (transposeBivariate (planeCurveFrobeniusRelation f)).natDegree = b → planeCurveFunction f 1 ∉ frobeniusSubfield (PlaneCurveFunctionField f) p → a * h + b * k < p → ¬(a ≤ k ∧ b ≤ h) → LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0) (planeCurveFunction f 1) h k)

Plane-curve form of the Corvaja--Zannier auxiliary-family linear-independence proposition (the q = p, z = w = 1 specialization).

The two nonzero partial derivatives are the source's two separating-coordinate hypotheses. For the displayed orientation, separability over the field generated by coordinate 1 is the one used to prove that this coordinate has minimal-polynomial degree p over L^p; the symmetric partial is retained because the source proposition assumes both coordinates separating.

Two hypotheses mark exact geometric boundaries rather than hiding them:

• hbaseChange is irreducibility after the literal extension of constants K → L^p, the consequence of absolute irreducibility needed by Gauss descent;
• hsecondNotFrobenius says that the separating second coordinate is not a p-th power in L. Equivalently, it is the missing differential/basis compatibility needed to turn separability into degree exactly p.

All remaining assumptions are the printed positivity, exact bidegree, size, and excluded-degree-alternative hypotheses.

theorem BGS.CorvajaZannier.planeCurve_auxiliaryFamily_linearIndependent_of_nonzero_partials {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (a b h k : ℕ) : 0 < a → 0 < h → 0 < k → Irreducible ((MvPolynomial.map perfectConstantsToFrobeniusSubfield) f) → (planeCurveFrobeniusRelation f).natDegree = a → (transposeBivariate (planeCurveFrobeniusRelation f)).natDegree = b → a * h + b * k < p → ¬(a ≤ k ∧ b ≤ h) → LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0) (planeCurveFunction f 1) h k)

Plane-curve auxiliary-family linear independence with the Frobenius exclusion discharged from the separating-coordinate hypothesis.

theorem BGS.CorvajaZannier.planeCurve_auxiliaryFamily_linearIndependent_of_absoluteIrreducible {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hf := ⋯; ∀ (a b h k : ℕ), 0 < a → 0 < h → 0 < k → (planeCurveFrobeniusRelation f).natDegree = a → (transposeBivariate (planeCurveFrobeniusRelation f)).natDegree = b → a * h + b * k < p → ¬(a ≤ k ∧ b ≤ h) → LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0) (planeCurveFunction f 1) h k)

Plane-curve auxiliary-family linear independence from absolute irreducibility and the two separating-coordinate hypotheses. Absolute irreducibility supplies both irreducibility over the constant field and the literal base change to the Frobenius subfield used by the resultant proof.

theorem BGS.CorvajaZannier.planeCurve_auxiliaryFamily_linearIndependent_of_absoluteIrreducible_coordinateDegrees {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hf := ⋯; ∀ (h k : ℕ), 0 < h → 0 < k → MvPolynomial.degreeOf 0 f * h + MvPolynomial.degreeOf 1 f * k < p → ¬(MvPolynomial.degreeOf 0 f ≤ k ∧ MvPolynomial.degreeOf 1 f ≤ h) → LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0) (planeCurveFunction f 1) h k)

The strongest plane-curve auxiliary-family theorem at the present algebraic boundary: the bidegrees are the actual coordinate degrees of the defining equation, so no degree-identification hypotheses remain.