Powered-image relations over the Frobenius constant field

This file proves that the equation of the image of a plane curve under the coordinate-power map remains irreducible after arbitrary scalar extension. It then transports that equation to the Frobenius constant field and applies the relation criterion to obtain the auxiliary-family linear independence used in the Corvaja--Zannier Wronskian argument.

noncomputable def BGS.CorvajaZannier.bivariateEvalAlgHom {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] (u v : A) : Polynomial (Polynomial K) →ₐ[K] A

The algebra homomorphism evaluating a bivariate polynomial at two chosen elements.

Equations

• BGS.CorvajaZannier.bivariateEvalAlgHom u v = Polynomial.eval₂AlgHom (Polynomial.aeval u) v ⋯

theorem BGS.CorvajaZannier.bivariateEvalAlgHom_comp {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] (F : A →ₐ[K] B) (u v : A) : F.comp (bivariateEvalAlgHom u v) = bivariateEvalAlgHom (F u) (F v)

theorem BGS.CorvajaZannier.bivariateQuotientEvalEmbedding {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] (u v : A) (g : Polynomial (Polynomial K)) (hzero : (bivariateEvalAlgHom u v) g = 0) (hdiv : ∀ (P : Polynomial (Polynomial K)), (bivariateEvalAlgHom u v) P = 0 → g ∣ P) : ∃ (F : Polynomial (Polynomial K) ⧸ Ideal.span {g} →ₐ[K] A), Function.Injective ⇑F

@[simp]

theorem BGS.CorvajaZannier.bivariateEvalAlgHom_eq_evalBivariate {K : Type u_1} [Field K] {L : Type u_4} [Field L] [Algebra K L] (u v : L) (P : Polynomial (Polynomial K)) : (bivariateEvalAlgHom u v) P = evalBivariate u v P

theorem BGS.CorvajaZannier.primitiveClearedMinpolyRelation_dvd_of_evalBivariate_eq_zero {K : Type u_1} [Field K] {L : Type u_4} [Field L] [Algebra K L] (u : L) (hu : Transcendental K u) (v : L) (hv : IsIntegral (↥K⟮u⟯) v) (P : Polynomial (Polynomial K)) (hP : evalBivariate u v P = 0) : primitiveClearedMinpolyRelation u hu v ∣ P

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_quotient_embeds_source {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : have g := poweredCoordinateImageRelation hf hpartialSecond m hm n; ∃ (F : Polynomial (Polynomial K) ⧸ Ideal.span {g} →ₐ[K] PlaneCurveCoordinateRing f), Function.Injective ⇑F

noncomputable def BGS.CorvajaZannier.iteratedPolynomialBaseChangeEquiv {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] : TensorProduct K E (Polynomial (Polynomial K)) ≃ₐ[E] Polynomial (Polynomial E)

Base change equivalence for iterated polynomial rings.

Equations

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

theorem BGS.CorvajaZannier.bivariateEquiv_map_commutes {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] (g : Polynomial (Polynomial K)) : (Polynomial.Bivariate.equivMvPolynomial E).symm ((MvPolynomial.map (algebraMap K E)) ((Polynomial.Bivariate.equivMvPolynomial K) g)) = Polynomial.map (Polynomial.mapRingHom (algebraMap K E)) g

theorem BGS.CorvajaZannier.iteratedPolynomialBaseChangeEquiv_tmul_one {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] (g : Polynomial (Polynomial K)) : (iteratedPolynomialBaseChangeEquiv E) (1 ⊗ₜ[K] g) = Polynomial.map (Polynomial.mapRingHom (algebraMap K E)) g

noncomputable def BGS.CorvajaZannier.bivariateQuotientEquivMvPolynomial {K : Type u_1} [Field K] (g : Polynomial (Polynomial K)) : (Polynomial (Polynomial K) ⧸ Ideal.span {g}) ≃ₐ[K] PlaneCurveCoordinateRing ((Polynomial.Bivariate.equivMvPolynomial K) g)

The equivalence between a bivariate quotient and its multivariate presentation.

Equations

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

theorem BGS.CorvajaZannier.tensorProduct_map_id_injective {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] {A : Type u_6} {B : Type u_7} [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] (F : A →ₐ[K] B) (hF : Function.Injective ⇑F) : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id E E) F)

theorem BGS.CorvajaZannier.tensorProduct_isDomain_of_embedding {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] {A : Type u_6} {B : Type u_7} [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] (F : A →ₐ[K] B) (hF : Function.Injective ⇑F) (hdom : IsDomain (TensorProduct K E B)) : IsDomain (TensorProduct K E A)

noncomputable def BGS.CorvajaZannier.planeCurveCoordinateRingBaseChangeEquiv {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) : TensorProduct K E (PlaneCurveCoordinateRing f) ≃+* PlaneCurveCoordinateRing ((MvPolynomial.map (algebraMap K E)) f)

The base change equivalence for the coordinate ring of the plane curve.

Equations

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

theorem BGS.CorvajaZannier.planeCurveCoordinateRingBaseChange_isDomain {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] (f : MvPolynomial (Fin 2) K) (hfE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) : IsDomain (TensorProduct K E (PlaneCurveCoordinateRing f))

theorem BGS.CorvajaZannier.irreducible_mvPolynomial_map_of_tensorQuotient_isDomain {K : Type u_1} [Field K] (E : Type u_5) [Field E] [Algebra K E] (G : MvPolynomial (Fin 2) K) (hG : Irreducible G) (hdom : IsDomain (TensorProduct K E (PlaneCurveCoordinateRing G))) : Irreducible ((MvPolynomial.map (algebraMap K E)) G)

theorem BGS.CorvajaZannier.poweredCoordinateImageRelation_irreducible_map {K : Type u_1} [Field K] {E : Type u_5} [Field E] [Algebra K E] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : Irreducible (Polynomial.map (Polynomial.mapRingHom (algebraMap K E)) (poweredCoordinateImageRelation hf hpartialSecond m hm n))

theorem BGS.CorvajaZannier.transposeBivariate_map {K : Type u_1} [Field K] {E : Type u_5} [Field E] (i : K →+* E) (P : Polynomial (Polynomial K)) : transposeBivariate (Polynomial.map (Polynomial.mapRingHom i) P) = Polynomial.map (Polynomial.mapRingHom i) (transposeBivariate P)

theorem BGS.CorvajaZannier.evalBivariate_map_mapRingHom {K : Type u_1} [Field K] {E : Type u_5} [Field E] [Algebra K E] {L : Type u_6} [Field L] [Algebra K L] [Algebra E L] [IsScalarTower K E L] (u v : L) (P : Polynomial (Polynomial K)) : evalBivariate u v (Polynomial.map (Polynomial.mapRingHom (algebraMap K E)) P) = evalBivariate u v P

noncomputable def BGS.CorvajaZannier.poweredCoordinateFrobeniusImageRelation {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : Polynomial (Polynomial ↥(frobeniusSubfield (PlaneCurveFunctionField f) p))

The relation between powered coordinates and the Frobenius image.

Equations

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

theorem BGS.CorvajaZannier.poweredCoordinateFrobeniusImageRelation_natDegree {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : (poweredCoordinateFrobeniusImageRelation hf hpartialSecond m hm n).natDegree = (transposeBivariate (poweredCoordinateImageRelation hf hpartialSecond m hm n)).natDegree

theorem BGS.CorvajaZannier.transposeBivariate_poweredCoordinateFrobeniusImageRelation_natDegree {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : (transposeBivariate (poweredCoordinateFrobeniusImageRelation hf hpartialSecond m hm n)).natDegree = (poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree

theorem BGS.CorvajaZannier.evalBivariate_poweredCoordinateFrobeniusImageRelation_eq_zero {K : Type u_1} [Field K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [PerfectField K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : evalBivariate (planeCurveFunction f 1 ^ n) (planeCurveFunction f 0 ^ m) (poweredCoordinateFrobeniusImageRelation hf hpartialSecond m hm n) = 0

theorem BGS.CorvajaZannier.poweredCoordinateFrobeniusImageRelation_irreducible {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)) (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n : ℕ) : Irreducible (poweredCoordinateFrobeniusImageRelation hf hpartialSecond m hm n)

theorem BGS.CorvajaZannier.poweredCoordinateFrobeniusImage_auxiliaryFamily_linearIndependent {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)) (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : ¬p ∣ n) (h k : ℕ) (hh : 0 < h) (hk : 0 < k) (hsize : have g := poweredCoordinateFrobeniusImageRelation hf hpartialSecond m hm n; g.natDegree * h + (transposeBivariate g).natDegree * k < p) (hexcluded : have g := poweredCoordinateFrobeniusImageRelation hf hpartialSecond m hm n; ¬(g.natDegree ≤ k ∧ (transposeBivariate g).natDegree ≤ h)) : LinearIndependent (↥(frobeniusSubfield (PlaneCurveFunctionField f) p)) (auxiliaryFamily (planeCurveFunction f 0 ^ m) (planeCurveFunction f 1 ^ n) h k)