Direct weighted bounds on exhaustive exceptional places

The family-place API is useful when several functions are indexed together. The canonical global summation, however, is stated directly on the exhaustive sum of finite and infinite places. This file records the corresponding subset lower bound and specializes it to the one-minus quotient used in Proposition 2.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_u_eq_zero_outside_propositionTwoExceptionalPlaces (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) (P : FiniteExtensionPlace K L) (hP : P ∉ propositionTwoExceptionalPlaces K L u v) : (finiteExtensionPrincipalDivisor K L u) P = 0

The first coordinate has order zero away from the direct Proposition 2 exceptional set.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_v_eq_zero_outside_propositionTwoExceptionalPlaces (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) (P : FiniteExtensionPlace K L) (hP : P ∉ propositionTwoExceptionalPlaces K L u v) : (finiteExtensionPrincipalDivisor K L v) P = 0

The second coordinate has order zero away from the direct Proposition 2 exceptional set.

theorem BGS.CorvajaZannier.mem_propositionTwoExceptionalPlaces_of_v_order_pos (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) (P : FiniteExtensionPlace K L) (hP : 0 < (finiteExtensionPrincipalDivisor K L v) P) : P ∈ propositionTwoExceptionalPlaces K L u v

Every positive-order place of the second coordinate belongs to the direct Proposition 2 exceptional set.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_gridProduct_eq_zero_off_propositionTwoExceptionalPlaces (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 : ℕ) (P : FiniteExtensionPlace K L) (hP : P ∉ propositionTwoExceptionalPlaces K L u v) : (finiteExtensionPrincipalDivisor K L (finiteExtensionAuxiliaryGridProduct L u v h k)) P = 0

Every auxiliary grid product has order zero away from the direct Proposition 2 exceptional set.

theorem BGS.CorvajaZannier.finiteExtensionWeightedOrder_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] (x : L) (S : Finset (FiniteExtensionPlace K L)) : -↑(finiteExtensionHeight K L x) ≤ ∑ P ∈ S, (finiteExtensionPrincipalDivisor K L x) P * ↑(finiteExtensionPlaceDegree K L P)

On any finite set of exhaustive places, the weighted order sum of a function is bounded below by minus its full pole height.

theorem BGS.CorvajaZannier.finiteExtensionOneSubU_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] (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (huone : u ≠ 1) (hvone : v ≠ 1) (S : Finset (FiniteExtensionPlace K L)) : -↑(finiteExtensionPositiveDegree K L u) - ↑(finiteExtensionPositiveDegree K L v) ≤ ∑ P ∈ S, (finiteExtensionPrincipalDivisor K L ((1 - u) / (1 - v))) P * ↑(finiteExtensionPlaceDegree K L P)

The exceptional-set contribution of (1-u)/(1-v) is bounded below by minus the sum of the two coordinate heights. The assertion holds for every finite set, and hence in particular for the zero-and-pole set of u,v.