Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.PoleDivisor

Pole divisors in the exhaustive finite-extension place model #

The existing Corvaja--Zannier infrastructure records principal divisors and their total pole height. The Stepanov argument also needs the actual effective pole divisor. This file defines it by retaining the negative coefficients of the principal divisor and changing their signs, proves that it makes the original function a section, and identifies its divisor degree with the existing height.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.poleDivisorConstantAlgebra (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 pole divisor construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.poleDivisorConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower K (RatFunc K) L
    source
    noncomputable def BGS.HasseWeil.finiteExtensionPoleDivisor (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) :
    CorvajaZannier.FiniteExtensionDivisor K L

    The effective negative part of the principal divisor of x.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem BGS.HasseWeil.finiteExtensionPoleDivisor_apply (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) :
      (finiteExtensionPoleDivisor K L x) v = if (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v < 0 then -(CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v else 0
      source
      theorem BGS.HasseWeil.finiteExtensionPoleDivisor_effective (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) :
      0 ≤ (finiteExtensionPoleDivisor K L x) v

      A pole divisor is effective.

      source
      theorem BGS.HasseWeil.finiteExtensionPrincipal_add_poleDivisor_effective (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) :
      0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v + (finiteExtensionPoleDivisor K L x) v

      Adding the pole divisor to the principal divisor is effective.

      source
      theorem BGS.HasseWeil.mem_finiteExtensionRiemannSpace_poleDivisor (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 : L) (hx : x ≠ 0) :
      x ∈ CorvajaZannier.finiteExtensionRiemannSpace K L (finiteExtensionPoleDivisor K L x)

      Every nonzero function is a section of its pole divisor.

      source
      theorem BGS.HasseWeil.finiteExtensionDivisorDegree_poleDivisor (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.finiteExtensionDivisorDegree K L (finiteExtensionPoleDivisor K L x) = ↑(CorvajaZannier.finiteExtensionHeight K L x)

      The degree of the pole divisor is the previously defined pole height.

      source
      theorem BGS.HasseWeil.finiteExtensionDivisorDegree_nsmul (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (n : ℕ) (D : CorvajaZannier.FiniteExtensionDivisor K L) :
      CorvajaZannier.finiteExtensionDivisorDegree K L (n • D) = ↑n * CorvajaZannier.finiteExtensionDivisorDegree K L D

      Divisor degree commutes with natural scaling.

      source
      theorem BGS.HasseWeil.pow_mul_pow_mem_poleDivisor_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] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (i j : ℕ) :
      x ^ i * y ^ j ∈ CorvajaZannier.finiteExtensionRiemannSpace K L (i • finiteExtensionPoleDivisor K L x + j • finiteExtensionPoleDivisor K L y)

      A coordinate monomial is a section of the sum of the correspondingly scaled pole divisors.

      source
      theorem BGS.HasseWeil.finiteExtensionDivisorDegree_pow_mul_pow_budget (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 y : L) (i j : ℕ) :
      CorvajaZannier.finiteExtensionDivisorDegree K L (i • finiteExtensionPoleDivisor K L x + j • finiteExtensionPoleDivisor K L y) = ↑i * ↑(CorvajaZannier.finiteExtensionHeight K L x) + ↑j * ↑(CorvajaZannier.finiteExtensionHeight K L y)

      The degree of the monomial pole budget is the corresponding linear combination of the two coordinate heights.