Heights and zero counts in a one-point Riemann space

This file supplies the direct bridge from membership in the one-point Riemann space L(nP) to the pole height used by the exhaustive principal-divisor API.

For a nonzero x ∈ L(nP), every negative-order place is P and its pole order is at most n. Unfolding finiteExtensionHeight therefore gives the bound height(x) ≤ n * deg(P). Combining this with the existing positive-order place count gives the corresponding Tao-style zero-count estimate.

@[instance_reducible]

noncomputable def BGS.HasseWeil.onePointHeightConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the one point height construction.

Equations

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

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

theorem BGS.HasseWeil.finiteExtensionHeight_le_of_mem_onePointRiemannSpace (K : Type u_1) [Field K] [Fintype 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] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) (x : L) (hx : x ≠ 0) (hxSpace : x ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) : CorvajaZannier.finiteExtensionHeight K L x ≤ n * CorvajaZannier.finiteExtensionPlaceDegree K L P

A nonzero function in L(nP) has pole height at most n * deg(P).

This is proved directly from the exhaustive principal-divisor support and the definition of finiteExtensionHeight; it does not invoke an abstract divisor-degree estimate.

theorem BGS.HasseWeil.finiteExtensionHeight_le_of_mem_onePointRiemannSpace_degree_one (K : Type u_1) [Field K] [Fintype 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] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) (x : L) (hx : x ≠ 0) (hxSpace : x ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) (hdegree : CorvajaZannier.finiteExtensionPlaceDegree K L P = 1) : CorvajaZannier.finiteExtensionHeight K L x ≤ n

Degree-one specialization of finiteExtensionHeight_le_of_mem_onePointRiemannSpace.

theorem BGS.HasseWeil.Fintype.card_le_mul_placeDegree_of_onePointRiemannSpace (K : Type u_1) [Field K] [Fintype 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 ι] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) (x : L) (hx : x ≠ 0) (hxSpace : x ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) (place : ι → CorvajaZannier.FiniteExtensionPlace K L) (hinjective : Function.Injective place) (hpositive : ∀ (i : ι), 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) (place i)) : Fintype.card ι ≤ n * CorvajaZannier.finiteExtensionPlaceDegree K L P

Tao-style zero count: a finite family injecting into positive-order places of a nonzero x ∈ L(nP) has cardinality at most n * deg(P).

theorem BGS.HasseWeil.Fintype.card_le_of_onePointRiemannSpace_degree_one (K : Type u_1) [Field K] [Fintype 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 ι] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) (x : L) (hx : x ≠ 0) (hxSpace : x ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) (hdegree : CorvajaZannier.finiteExtensionPlaceDegree K L P = 1) (place : ι → CorvajaZannier.FiniteExtensionPlace K L) (hinjective : Function.Injective place) (hpositive : ∀ (i : ι), 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) (place i)) : Fintype.card ι ≤ n

Degree-one specialization of the one-point zero count.