Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.GeneralFiniteExtensionRiemannLower

A coarse Riemann inequality for arbitrary function fields #

This file derives the amount of Riemann-space growth needed by the intrinsic Stepanov argument without appealing to an external Riemann--Roch theorem.

For a finite separable extension L / K(X), choose a primitive element y. The monomials X^i y^j with j < [L : K(X)] are linearly independent. Their pole divisors give a cofinal family of effective divisors supported above infinity and hence a coarse, but uniform-for-L, Riemann inequality. The finite-place approximation theorem then transfers this inequality to every one-point divisor at a finite place.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.generalRiemannConstantAlgebra (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 general finite extension riemann lower construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.generalRiemannConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower K (RatFunc K) L
    source
    theorem BGS.HasseWeil.generalRiemannInfinityModuleFinite (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)
    source
    theorem BGS.HasseWeil.infinitySupported_riemann_lower_of_monomial (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] (x y : L) (hx0 : x ≠ 0) (hy0 : y ≠ 0) (b : ℕ) (hLI : ∀ (n : ℕ), LinearIndependent K (planeMonomialGrid x y (n + 1) b)) (hxHeight : CorvajaZannier.finiteExtensionHeight K L x = b) (hxInfinity : ∀ (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)), 0 < (finiteExtensionPoleDivisor K L x) (Sum.inr P)) (E : CorvajaZannier.FiniteExtensionDivisor K L) :
    (∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ E v) → (∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K L), E (Sum.inl q) = 0) → (CorvajaZannier.finiteExtensionDivisorDegree K L E).toNat + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L E) + ((b - 1) * CorvajaZannier.finiteExtensionHeight K L y + 1)

    A monomial grid with the expected X-height gives a Riemann inequality for every effective divisor supported above infinity.

    source
    theorem BGS.HasseWeil.infinitySupported_riemann_lower_of_primitive (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] (x y : L) (hx0 : x ≠ 0) (hy0 : y ≠ 0) (hxMap : (algebraMap (RatFunc K) L) RatFunc.X = x) (hprimitive : (RatFunc K)⟮y⟯ = ⊤) (hxHeight : CorvajaZannier.finiteExtensionHeight K L x = Module.finrank (RatFunc K) L) (hxInfinity : ∀ (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)), 0 < (finiteExtensionPoleDivisor K L x) (Sum.inr P)) (E : CorvajaZannier.FiniteExtensionDivisor K L) :
    (∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ E v) → (∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K L), E (Sum.inl q) = 0) → (CorvajaZannier.finiteExtensionDivisorDegree K L E).toNat + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L E) + ((Module.finrank (RatFunc K) L - 1) * CorvajaZannier.finiteExtensionHeight K L y + 1)

    A nonzero primitive element and the exact pole height of X supply the monomial hypotheses of infinitySupported_riemann_lower_of_monomial.

    source
    theorem BGS.HasseWeil.exists_nonzero_primitive_element (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] :
    ∃ (y : L), y ≠ 0 ∧ (RatFunc K)⟮y⟯ = ⊤

    A finite separable extension has a primitive element which can be chosen nonzero, including the degree-one case.

    source
    theorem BGS.HasseWeil.finitePlace_riemann_lower_of_primitive (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] (x y : L) (hx0 : x ≠ 0) (hy0 : y ≠ 0) (hxMap : (algebraMap (RatFunc K) L) RatFunc.X = x) (hprimitive : (RatFunc K)⟮y⟯ = ⊤) (hxHeight : CorvajaZannier.finiteExtensionHeight K L x = Module.finrank (RatFunc K) L) (hxInfinity : ∀ (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)), 0 < (finiteExtensionPoleDivisor K L x) (Sum.inr P)) (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (N : ℕ) :
    N * CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl q) + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L (Sum.inl q) N) + ((Module.finrank (RatFunc K) L - 1) * CorvajaZannier.finiteExtensionHeight K L y + 1)

    The coarse primitive-element Riemann inequality at every finite place.

    source
    theorem BGS.HasseWeil.exists_finitePlace_riemann_lower_budget (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] :
    ∃ (g : ℕ), ∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (N : ℕ), N * CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl q) + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L (Sum.inl q) N) + g

    Every finite separable extension of K(X) admits a single natural-number budget for Riemann's inequality at all of its finite places. The budget is constructed from a nonzero primitive element; no genus or Riemann--Roch input is assumed.