Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionRiemannLowerFromGenus

One-point Riemann lower bounds from the intrinsic genus #

Riemann's inequality gives the intrinsic function-field genus itself as a simultaneous budget for every one-point Riemann space. This applies to the exhaustive BGS place type, including both finite and infinity places.

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

Equations
Instances For
    source
    theorem BGS.HasseWeil.genusRiemannConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower K (RatFunc K) L
    source
    @[instance_reducible]
    noncomputable def BGS.HasseWeil.genusRiemannPolynomialAlgebra (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 riemann lower from genus construction.

    Equations
    Instances For
      source
      theorem BGS.HasseWeil.genusRiemannPolynomialRatFuncTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
      IsScalarTower (Polynomial K) (RatFunc K) L
      source
      theorem BGS.HasseWeil.genusRiemannConstantPolynomialTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
      IsScalarTower K (Polynomial K) L
      source
      theorem BGS.HasseWeil.finiteExtension_onePoint_riemann_lower_of_genus (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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] (P : CorvajaZannier.FiniteExtensionPlace K L) (N : ℕ) :
      N * CorvajaZannier.finiteExtensionPlaceDegree K L P + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P N) + MarkoffRiemannRoch.FunctionField.genus K L

      Riemann's inequality gives the intrinsic genus as a simultaneous budget for every one-point Riemann space in the exhaustive finite/infinity place model.