Exceptional-place bookkeeping for Corvaja--Zannier

This file constructs the exceptional set used in the global summation in Corvaja--Zannier Proposition 2. For two nonzero functions u and v, it is the union of the supports of their exhaustive principal divisors. Thus both functions, every auxiliary grid monomial, and their grid product have order zero away from the set. Its residue-degree-weighted size is at most twice the sum of the two heights.

The final section proves the source estimate

-(H(u) + H(v)) <= sum_{w in S} ord_w ((1-v)/(1-u)) deg(w).

The same estimate is also supplied in the paper's orientation (1-u)/(1-v). No algebraic-closedness hypothesis is needed for the weighted statements; over an algebraically closed constant field they specialize to ordinary cardinality and unweighted orders.

Source provenance: published pages 1936--1937; checked semantic reconstruction Papers/CorvajaZannier2013/CorvajaZannier2013.tex, lines 731--779. The earlier Proposition 2 source gives the same bookkeeping in Papers/arXiv-math-0512074v3/jag_rivisto2.tex, lines 618--653.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.exceptionalSupportPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the finite extension exceptional support construction.

Equations

• BGS.CorvajaZannier.exceptionalSupportPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.exceptionalSupportPolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.CorvajaZannier.exceptionalSupportFiniteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.exceptionalSupportFiniteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.exceptionalSupportPolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.CorvajaZannier.exceptionalSupportFiniteIntegralClosureIsTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)

theorem BGS.CorvajaZannier.exceptionalSupportInfinityIntegralClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.exceptionalSupportInfinityIntegralClosureIsDedekindDomain (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_one (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : finiteExtensionPrincipalDivisor K L 1 = 0

The exhaustive principal divisor of one is zero.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_mul (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) : finiteExtensionPrincipalDivisor K L (x * y) = finiteExtensionPrincipalDivisor K L x + finiteExtensionPrincipalDivisor K L y

Exhaustive principal divisors turn a nonzero product into a sum.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_pow (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (m : ℕ) : finiteExtensionPrincipalDivisor K L (x ^ m) = m • finiteExtensionPrincipalDivisor K L x

Exhaustive principal divisors turn a nonzero power into a multiple.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_inv (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionPrincipalDivisor K L x⁻¹ = -finiteExtensionPrincipalDivisor K L x

Exhaustive principal divisors turn a nonzero inverse into a negative.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_div (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) : finiteExtensionPrincipalDivisor K L (x / y) = finiteExtensionPrincipalDivisor K L x - finiteExtensionPrincipalDivisor K L y

Exhaustive principal divisors turn a quotient into a difference.

def BGS.CorvajaZannier.finiteExtensionAuxiliaryGridProduct (L : Type u_2) [Field L] (u v : L) (h k : ℕ) : L

Product of all grid monomials in the auxiliary family. Its divisor is the ordGrid term in the global Wronskian summation.

Equations

• BGS.CorvajaZannier.finiteExtensionAuxiliaryGridProduct L u v h k = ∏ rs : Fin (k + 1) × Fin h, u ^ ↑rs.1 * v ^ ↑rs.2

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_auxiliaryGridProduct (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (h k : ℕ) : finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k) = ∑ rs : Fin (k + 1) × Fin h, (↑rs.1 • finiteExtensionPrincipalDivisor K L u + ↑rs.2 • finiteExtensionPrincipalDivisor K L v)

Exact principal-divisor formula for the auxiliary grid product.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.exceptionalSupportPlaceDecidableEq (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : DecidableEq (FiniteExtensionPlace K L)

Decidable equality on (FiniteExtensionPlace K L) used in the finite extension exceptional support construction.

Equations

• BGS.CorvajaZannier.exceptionalSupportPlaceDecidableEq K L = Classical.decEq (BGS.CorvajaZannier.FiniteExtensionPlace K L)

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_supportDegree_le (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) : ∑ w ∈ (finiteExtensionPrincipalDivisor K L x).support, finiteExtensionPlaceDegree K L w ≤ finiteExtensionPositiveDegree K L x + finiteExtensionHeight K L x

The residue-degree-weighted number of places in the support of a principal divisor is bounded by its positive degree plus its pole height.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_supportDegree_le_two_mul_height (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : ∑ w ∈ (finiteExtensionPrincipalDivisor K L x).support, finiteExtensionPlaceDegree K L w ≤ 2 * finiteExtensionPositiveDegree K L x

For a nonzero function, the weighted support has degree at most twice its height.

theorem BGS.CorvajaZannier.finiteExtensionHeight_mul_le (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) : finiteExtensionHeight K L (x * y) ≤ finiteExtensionHeight K L x + finiteExtensionHeight K L y

Pole height is subadditive under multiplication.

theorem BGS.CorvajaZannier.finiteExtensionHeight_inv_eq_positiveDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionHeight K L x⁻¹ = finiteExtensionPositiveDegree K L x

The pole height of an inverse is the positive degree of the original function.

theorem BGS.CorvajaZannier.finiteExtensionHeight_inv (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionHeight K L x⁻¹ = finiteExtensionHeight K L x

Pole height is invariant under inversion of a nonzero function.

theorem BGS.CorvajaZannier.finiteExtensionHeight_div_le (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) : finiteExtensionHeight K L (x / y) ≤ finiteExtensionHeight K L x + finiteExtensionHeight K L y

Pole height is subadditive under division.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_one_sub_apply_of_neg (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (w : FiniteExtensionPlace K L) (hxneg : (finiteExtensionPrincipalDivisor K L x) w < 0) : (finiteExtensionPrincipalDivisor K L (1 - x)) w = (finiteExtensionPrincipalDivisor K L x) w

At a pole of x, subtracting x from one does not change the exhaustive place order.

theorem BGS.CorvajaZannier.finiteExtensionHeight_one_sub (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (hxone : x ≠ 1) : finiteExtensionHeight K L (1 - x) = finiteExtensionHeight K L x

The functions x and 1-x have the same pole height.

def BGS.CorvajaZannier.finiteExtensionFamilyMemberSupportEmbedding (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) : ↥(finiteExtensionPrincipalDivisor K L (f a)).support ↪ FiniteExtensionFamilyPlace K L f

Embed the divisor support of one function into the common support of its family.

Equations

• BGS.CorvajaZannier.finiteExtensionFamilyMemberSupportEmbedding K L f a = { toFun := fun (w : ↥(BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L (f a)).support) => ⟨↑w, ⋯⟩, inj' := ⋯ }

noncomputable def BGS.CorvajaZannier.finiteExtensionFamilyMemberSupport (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) : Finset (FiniteExtensionFamilyPlace K L f)

The support of one family member, lifted to the common family place type.

Equations

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

@[simp]

theorem BGS.CorvajaZannier.mem_finiteExtensionFamilyMemberSupport_iff (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (w : FiniteExtensionFamilyPlace K L f) : w ∈ finiteExtensionFamilyMemberSupport K L f a ↔ ↑w ∈ (finiteExtensionPrincipalDivisor K L (f a)).support

theorem BGS.CorvajaZannier.sum_finiteExtensionFamilyMemberSupport_placeDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) : ∑ w ∈ finiteExtensionFamilyMemberSupport K L f a, finiteExtensionPlaceDegree K L ↑w = ∑ w ∈ (finiteExtensionPrincipalDivisor K L (f a)).support, finiteExtensionPlaceDegree K L w

noncomputable def BGS.CorvajaZannier.finiteExtensionExceptionalSet (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) : Finset (FiniteExtensionFamilyPlace K L f)

The finite exceptional set consisting exactly of the zero and pole places of the selected functions u and v, embedded into a caller's common family place type.

Equations

• BGS.CorvajaZannier.finiteExtensionExceptionalSet K L f iU iV = BGS.CorvajaZannier.finiteExtensionFamilyMemberSupport K L f iU ∪ BGS.CorvajaZannier.finiteExtensionFamilyMemberSupport K L f iV

@[simp]

theorem BGS.CorvajaZannier.mem_finiteExtensionExceptionalSet_iff (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) (w : FiniteExtensionFamilyPlace K L f) : w ∈ finiteExtensionExceptionalSet K L f iU iV ↔ ↑w ∈ (finiteExtensionPrincipalDivisor K L (f iU)).support ∨ ↑w ∈ (finiteExtensionPrincipalDivisor K L (f iV)).support

theorem BGS.CorvajaZannier.finiteExtensionExceptionalSet_weightedDegree_le (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) : ∑ w ∈ finiteExtensionExceptionalSet K L f iU iV, finiteExtensionPlaceDegree K L ↑w ≤ 2 * (finiteExtensionPositiveDegree K L (f iU) + finiteExtensionPositiveDegree K L (f iV))

Residue-degree-weighted boundary bound for the exceptional set.

theorem BGS.CorvajaZannier.finiteExtensionFamilyWeightedOrder_sum_ge_neg_height (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (a : A) (S : Finset (FiniteExtensionFamilyPlace K L f)) : -↑(finiteExtensionHeight K L (f a)) ≤ ∑ w ∈ S, finiteExtensionFamilyWeightedOrder K L f a w

The sum of the weighted orders over an arbitrary subset of the common family place type is bounded below by minus the full pole height.

theorem BGS.CorvajaZannier.finiteExtensionHeight_one_sub_div_one_sub_le (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (huone : u ≠ 1) (hvone : v ≠ 1) : finiteExtensionHeight K L ((1 - v) / (1 - u)) ≤ finiteExtensionHeight K L u + finiteExtensionHeight K L v

The height bound for the reciprocal one-minus ratio used in the support estimate.

theorem BGS.CorvajaZannier.finiteExtensionExceptionalSet_oneSubV_div_oneSubU_weightedOrder_lower_bound (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV iRho : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) (huone : f iU ≠ 1) (hvone : f iV ≠ 1) (hRho : f iRho = (1 - f iV) / (1 - f iU)) : -(↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) ≤ ∑ w ∈ finiteExtensionExceptionalSet K L f iU iV, finiteExtensionFamilyWeightedOrder K L f iRho w

The source lower bound for the exceptional-set contribution of rho = (1-v)/(1-u).

theorem BGS.CorvajaZannier.finiteExtensionExceptionalSet_oneSubU_div_oneSubV_weightedOrder_lower_bound (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV iRho : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) (huone : f iU ≠ 1) (hvone : f iV ≠ 1) (hRho : f iRho = (1 - f iU) / (1 - f iV)) : -(↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) ≤ ∑ w ∈ finiteExtensionExceptionalSet K L f iU iV, finiteExtensionFamilyWeightedOrder K L f iRho w

The same lower bound in the paper's orientation rho = (1-u)/(1-v).

theorem BGS.CorvajaZannier.finiteExtensionFamilyOrder_u_eq_zero_outsideExceptionalSet (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) (w : FiniteExtensionFamilyPlace K L f) (hw : w ∉ finiteExtensionExceptionalSet K L f iU iV) : finiteExtensionFamilyOrder K L f iU w = 0

Away from the exceptional set, u has order zero.

theorem BGS.CorvajaZannier.finiteExtensionFamilyOrder_v_eq_zero_outsideExceptionalSet (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) (w : FiniteExtensionFamilyPlace K L f) (hw : w ∉ finiteExtensionExceptionalSet K L f iU iV) : finiteExtensionFamilyOrder K L f iV w = 0

Away from the exceptional set, v has order zero.

theorem BGS.CorvajaZannier.finiteExtensionFamilyOrder_v_positive_mem_exceptionalSet (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) (w : FiniteExtensionFamilyPlace K L f) (hw : 0 < finiteExtensionFamilyOrder K L f iV w) : w ∈ finiteExtensionExceptionalSet K L f iU iV

Every positive-order place of v lies in the exceptional set.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_gridMonomial_eq_zero_outside (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) (r s : ℕ) (w : FiniteExtensionFamilyPlace K L f) (hw : w ∉ finiteExtensionExceptionalSet K L f iU iV) : (finiteExtensionPrincipalDivisor K L (f iU ^ r * f iV ^ s)) ↑w = 0

Every individual grid monomial has order zero away from the exceptional set.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_auxiliaryGridProduct_eq_zero_outside (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) (h k : ℕ) (w : FiniteExtensionFamilyPlace K L f) (hw : w ∉ finiteExtensionExceptionalSet K L f iU iV) : (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L (f iU) (f iV) h k)) ↑w = 0

The auxiliary grid product has order zero away from the zero and pole places of u and v.

theorem BGS.CorvajaZannier.finiteExtensionFamilyOrder_gridProduct_eq_zero_outsideExceptionalSet (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] (f : A → L) (iU iV iGrid : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) (h k : ℕ) (hGrid : f iGrid = finiteExtensionAuxiliaryGridProduct L (f iU) (f iV) h k) (w : FiniteExtensionFamilyPlace K L f) (hw : w ∉ finiteExtensionExceptionalSet K L f iU iV) : finiteExtensionFamilyOrder K L f iGrid w = 0

A family entry equal to the grid product has family order zero away from the exceptional set.

theorem BGS.CorvajaZannier.finiteExtensionExceptionalSet_card_le (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] [IsAlgClosed K] (f : A → L) (iU iV : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) : (finiteExtensionExceptionalSet K L f iU iV).card ≤ 2 * (finiteExtensionPositiveDegree K L (f iU) + finiteExtensionPositiveDegree K L (f iV))

Over an algebraically closed constant field, the weighted boundary bound is the ordinary cardinality bound used in the published proof.

theorem BGS.CorvajaZannier.finiteExtensionExceptionalSet_oneSubV_div_oneSubU_order_lower_bound (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] [IsAlgClosed K] (f : A → L) (iU iV iRho : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) (huone : f iU ≠ 1) (hvone : f iV ≠ 1) (hRho : f iRho = (1 - f iV) / (1 - f iU)) : -(↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) ≤ ∑ w ∈ finiteExtensionExceptionalSet K L f iU iV, finiteExtensionFamilyOrder K L f iRho w

Unweighted source estimate for rho = (1-v)/(1-u) over algebraically closed constants.

theorem BGS.CorvajaZannier.finiteExtensionExceptionalSet_oneSubU_div_oneSubV_order_lower_bound (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {A : Type u_3} [Fintype A] [IsAlgClosed K] (f : A → L) (iU iV iRho : A) (hu : f iU ≠ 0) (hv : f iV ≠ 0) (huone : f iU ≠ 1) (hvone : f iV ≠ 1) (hRho : f iRho = (1 - f iU) / (1 - f iV)) : -(↑(finiteExtensionPositiveDegree K L (f iU)) + ↑(finiteExtensionPositiveDegree K L (f iV))) ≤ ∑ w ∈ finiteExtensionExceptionalSet K L f iU iV, finiteExtensionFamilyOrder K L f iRho w

Unweighted source estimate in the paper's orientation rho = (1-u)/(1-v).