The Corvaja--Zannier auxiliary family

The proof of Corvaja--Zannier's Proposition 2 considers the family

u ^ i * (1 - u) / (1 - v) for 0 ≤ i < k, together with u ^ r * v ^ s for 0 ≤ r ≤ k and 0 ≤ s < h.

This file formalizes the purely algebraic first half of their linear- independence argument. Any dependence of that family produces a nonzero bivariate polynomial of the exact source form

P₁(U) * (1 - U) + P₂(U, V) * (1 - V)

which vanishes at (u, v). Bivariate polynomials are represented as polynomials in V whose coefficients are polynomials in U. Excluding the resulting relation by a resultant and degree argument is deliberately left as the next boundary; it is not assumed here through a typeclass or an axiom.

Source provenance: published pages 1933--1934; checked semantic reconstruction Papers/CorvajaZannier2013/CorvajaZannier2013.tex, lines 518--570. The dependence-to-relation step formalized here is lines 518--545.

def BGS.CorvajaZannier.auxiliaryFamily {L : Type u_2} [Field L] (u v : L) (h k : ℕ) : Fin k ⊕ Fin (k + 1) × Fin h → L

The exact auxiliary family used in Corvaja--Zannier's Proposition 2.

The left summand indexes u ^ i * (1 - u) / (1 - v) for i < k; the right summand indexes the rectangular family u ^ r * v ^ s for r ≤ k, s < h.

Equations

• BGS.CorvajaZannier.auxiliaryFamily u v h k (Sum.inl i) = u ^ ↑i * ((1 - u) / (1 - v))
• BGS.CorvajaZannier.auxiliaryFamily u v h k (Sum.inr rs) = u ^ ↑rs.1 * v ^ ↑rs.2

noncomputable def BGS.CorvajaZannier.auxiliaryPowerPolynomial {C : Type u_1} [Field C] {k : ℕ} (c : Fin k → C) : Polynomial C

The polynomial Σ i, c i * U ^ i.

Equations

• BGS.CorvajaZannier.auxiliaryPowerPolynomial c = (Polynomial.ofFn k) c

noncomputable def BGS.CorvajaZannier.auxiliaryGridPolynomial {C : Type u_1} [Field C] {h k : ℕ} (d : Fin (k + 1) × Fin h → C) : Polynomial (Polynomial C)

The bivariate polynomial Σ (r,s), d (r,s) * U ^ r * V ^ s, represented as a polynomial in V over C[U].

Equations

• BGS.CorvajaZannier.auxiliaryGridPolynomial d = (Polynomial.ofFn h) fun (s : Fin h) => (Polynomial.ofFn (k + 1)) fun (r : Fin (k + 1)) => d (r, s)

noncomputable def BGS.CorvajaZannier.auxiliaryRelationPolynomial {C : Type u_1} [Field C] {h k : ℕ} (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) : Polynomial (Polynomial C)

The bivariate relation obtained after clearing the denominator 1 - v from a dependence of the auxiliary family.

Equations

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

noncomputable def BGS.CorvajaZannier.evalBivariate {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (u v : L) (P : Polynomial (Polynomial C)) : L

Evaluate a bivariate polynomial, represented as a polynomial in V over C[U], at (u, v).

Equations

• BGS.CorvajaZannier.evalBivariate u v P = Polynomial.eval₂ (Polynomial.eval₂RingHom (algebraMap C L) u) v P

@[simp]

theorem BGS.CorvajaZannier.evalBivariate_auxiliaryPowerPolynomial {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] {k : ℕ} (u : L) (c : Fin k → C) : Polynomial.eval₂ (algebraMap C L) u (auxiliaryPowerPolynomial c) = ∑ i : Fin k, (algebraMap C L) (c i) * u ^ ↑i

@[simp]

theorem BGS.CorvajaZannier.evalBivariate_auxiliaryGridPolynomial {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] {h k : ℕ} (u v : L) (d : Fin (k + 1) × Fin h → C) : evalBivariate u v (auxiliaryGridPolynomial d) = ∑ rs : Fin (k + 1) × Fin h, (algebraMap C L) (d rs) * (u ^ ↑rs.1 * v ^ ↑rs.2)

@[simp]

theorem BGS.CorvajaZannier.evalBivariate_auxiliaryRelationPolynomial {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] {h k : ℕ} (u v : L) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) : evalBivariate u v (auxiliaryRelationPolynomial c d) = (∑ i : Fin k, (algebraMap C L) (c i) * u ^ ↑i) * (1 - u) + (∑ rs : Fin (k + 1) × Fin h, (algebraMap C L) (d rs) * (u ^ ↑rs.1 * v ^ ↑rs.2)) * (1 - v)

theorem BGS.CorvajaZannier.auxiliaryPowerPolynomial_natDegree_lt {C : Type u_1} [Field C] {k : ℕ} (hk : 0 < k) (c : Fin k → C) : (auxiliaryPowerPolynomial c).natDegree < k

The first coefficient polynomial has degree strictly less than k, as in the source's bound deg P₁ ≤ k - 1.

theorem BGS.CorvajaZannier.auxiliaryGridPolynomial_natDegree_lt {C : Type u_1} [Field C] {h k : ℕ} (hh : 0 < h) (d : Fin (k + 1) × Fin h → C) : (auxiliaryGridPolynomial d).natDegree < h

The rectangular polynomial has degree strictly less than h in its outer variable V, as in the source's bound deg_V P₂ ≤ h - 1.

theorem BGS.CorvajaZannier.auxiliaryGridPolynomial_coeff_natDegree_le {C : Type u_1} [Field C] {h k : ℕ} (d : Fin (k + 1) × Fin h → C) (s : ℕ) : ((auxiliaryGridPolynomial d).coeff s).natDegree ≤ k

Every coefficient of the rectangular polynomial, viewed as a polynomial in V, has degree at most k in U.

theorem BGS.CorvajaZannier.auxiliaryPowerPolynomial_eq_zero_iff {C : Type u_1} [Field C] {k : ℕ} (c : Fin k → C) : auxiliaryPowerPolynomial c = 0 ↔ ∀ (i : Fin k), c i = 0

The power polynomial is zero exactly when all of its coefficients are zero.

theorem BGS.CorvajaZannier.auxiliaryGridPolynomial_eq_zero_iff {C : Type u_1} [Field C] {h k : ℕ} (d : Fin (k + 1) × Fin h → C) : auxiliaryGridPolynomial d = 0 ↔ ∀ (rs : Fin (k + 1) × Fin h), d rs = 0

The grid polynomial is zero exactly when all of its coefficients are zero.

theorem BGS.CorvajaZannier.auxiliaryRelationPolynomial_eq_zero_iff {C : Type u_1} [Field C] {h k : ℕ} (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) : auxiliaryRelationPolynomial c d = 0 ↔ (∀ (i : Fin k), c i = 0) ∧ ∀ (rs : Fin (k + 1) × Fin h), d rs = 0

The source's relation polynomial is identically zero only for the trivial pair of coefficient families. This is the formal version of evaluating at V = 1 first and then using that both polynomial rings are domains.

theorem BGS.CorvajaZannier.exists_nonzero_auxiliaryRelationPolynomial_of_not_linearIndependent {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] {h k : ℕ} (u v : L) (hv : v ≠ 1) (hdep : ¬LinearIndependent C (auxiliaryFamily u v h k)) : ∃ (c : Fin k → C) (d : Fin (k + 1) × Fin h → C), auxiliaryRelationPolynomial c d ≠ 0 ∧ evalBivariate u v (auxiliaryRelationPolynomial c d) = 0

A dependence of the Corvaja--Zannier auxiliary family produces a nonzero bivariate relation of the exact source form which vanishes at (u, v).

This is the algebraic input to the subsequent resultant argument.

theorem BGS.CorvajaZannier.exists_nonzero_bounded_auxiliaryRelationPolynomial_of_not_linearIndependent {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] {h k : ℕ} (u v : L) (hh : 0 < h) (hk : 0 < k) (hv : v ≠ 1) (hdep : ¬LinearIndependent C (auxiliaryFamily u v h k)) : ∃ (c : Fin k → C) (d : Fin (k + 1) × Fin h → C), auxiliaryRelationPolynomial c d ≠ 0 ∧ evalBivariate u v (auxiliaryRelationPolynomial c d) = 0 ∧ (auxiliaryPowerPolynomial c).natDegree < k ∧ (auxiliaryGridPolynomial d).natDegree < h ∧ ∀ (s : ℕ), ((auxiliaryGridPolynomial d).coeff s).natDegree ≤ k

The dependence-to-relation implication together with all three degree bounds used by the source's resultant estimate.

theorem BGS.CorvajaZannier.auxiliaryFamily_linearIndependent_of_no_relation {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] {h k : ℕ} (u v : L) (hv : v ≠ 1) (hNoRelation : ∀ (c : Fin k → C) (d : Fin (k + 1) × Fin h → C), auxiliaryRelationPolynomial c d ≠ 0 → evalBivariate u v (auxiliaryRelationPolynomial c d) ≠ 0) : LinearIndependent C (auxiliaryFamily u v h k)

If the resultant step excludes every nonzero relation polynomial of the source form, then the auxiliary family is linearly independent.