Zero counting from principal-divisor height

This file isolates the divisor-theoretic counting step used after a Hasse--Weil estimate. Every place has positive degree, so each distinct zero of a function contributes at least one to the degree of its positive divisor. The product formula then identifies that degree with the pole height.

No point-count estimate is used here. In particular, the genuinely Hasse--Weil input can remain a separate upstream theorem.

@[instance_reducible]

noncomputable def BGS.HasseWeil.zeroCountingPolynomialAlgebra (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 zero counting construction.

Equations

• BGS.HasseWeil.zeroCountingPolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

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

theorem BGS.HasseWeil.zeroCountingFiniteIntegralClosureModuleFinite (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) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.zeroCountingInfinityIntegralClosureModuleFinite (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 ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.finiteExtensionPlaceDegree_pos (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] (v : CorvajaZannier.FiniteExtensionPlace K L) : 0 < CorvajaZannier.finiteExtensionPlaceDegree K L v

Every finite or above-infinity place of a finite separable function-field extension has positive degree.

noncomputable def BGS.HasseWeil.finiteExtensionZeroPlaces (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) : Finset (CorvajaZannier.FiniteExtensionPlace K L)

The finite set of places where x has positive order.

Equations

• BGS.HasseWeil.finiteExtensionZeroPlaces K L x = {v ∈ (BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L x).support | 0 < (BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v}

@[simp]

theorem BGS.HasseWeil.mem_finiteExtensionZeroPlaces_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] (x : L) (v : CorvajaZannier.FiniteExtensionPlace K L) : v ∈ finiteExtensionZeroPlaces K L x ↔ 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v

theorem BGS.HasseWeil.finiteExtensionPositiveDegree_eq_sum_zeroPlaces (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) : CorvajaZannier.finiteExtensionPositiveDegree K L x = ∑ v ∈ finiteExtensionZeroPlaces K L x, ((CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v).toNat * CorvajaZannier.finiteExtensionPlaceDegree K L v

The degree of the positive divisor is the weighted sum over the zero places.

theorem BGS.HasseWeil.card_le_finiteExtensionPositiveDegree_of_orders_positive (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 (CorvajaZannier.FiniteExtensionPlace K L)) (hpositive : ∀ v ∈ S, 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v) : S.card ≤ CorvajaZannier.finiteExtensionPositiveDegree K L x

Any finite set of positive-order places has cardinality at most the degree of the positive divisor.

theorem BGS.HasseWeil.sum_placeDegree_le_finiteExtensionPositiveDegree_of_orders_positive (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 (CorvajaZannier.FiniteExtensionPlace K L)) (hpositive : ∀ v ∈ S, 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v) : ∑ v ∈ S, CorvajaZannier.finiteExtensionPlaceDegree K L v ≤ CorvajaZannier.finiteExtensionPositiveDegree K L x

Any finite family of positive-order places contributes its full residue-degree weight to the positive divisor. This is the form needed when degree-one and degree-two closed points are counted simultaneously over a quadratic constant-field extension.

theorem BGS.HasseWeil.sum_placeDegree_le_finiteExtensionHeight_of_orders_positive (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) (S : Finset (CorvajaZannier.FiniteExtensionPlace K L)) (hpositive : ∀ v ∈ S, 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v) : ∑ v ∈ S, CorvajaZannier.finiteExtensionPlaceDegree K L v ≤ CorvajaZannier.finiteExtensionHeight K L x

Weighted positive-order place counting in terms of pole height.

theorem BGS.HasseWeil.Fintype.card_le_finiteExtensionHeight_of_injective_orders_positive (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] {ι : Type u_3} [Fintype ι] (x : L) (hx : x ≠ 0) (place : ι → CorvajaZannier.FiniteExtensionPlace K L) (hinjective : Function.Injective place) (hpositive : ∀ (i : ι), 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) (place i)) : Fintype.card ι ≤ CorvajaZannier.finiteExtensionHeight K L x

If a finite type injects into positive-order places of a nonzero function, then its cardinality is bounded by the pole height of that function.