Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.OnePointDivisorSplit

Splitting an effective divisor at one place #

The one-point Stepanov argument starts with a many-pole divisor supplied by plane monomials, then removes every allowed pole except the distinguished one. This file records the elementary divisor identities needed for that comparison. The actual codimension estimate is kept separate.

source
noncomputable def BGS.HasseWeil.finiteExtensionDivisorAway (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) :
CorvajaZannier.FiniteExtensionDivisor K L

Delete the coefficient of D at P, retaining all other coefficients.

Equations
Instances For
    source
    @[simp]
    theorem BGS.HasseWeil.finiteExtensionDivisorAway_apply_self (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) :
    (finiteExtensionDivisorAway K L D P) P = 0
    source
    @[simp]
    theorem BGS.HasseWeil.finiteExtensionDivisorAway_apply_of_ne (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P v : CorvajaZannier.FiniteExtensionPlace K L) (hv : v ≠ P) :
    (finiteExtensionDivisorAway K L D P) v = D v
    source
    theorem BGS.HasseWeil.single_add_finiteExtensionDivisorAway (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) :
    Finsupp.single P (D P) + finiteExtensionDivisorAway K L D P = D

    Splitting off the P coefficient recovers the original divisor.

    source
    theorem BGS.HasseWeil.finiteExtensionDivisorAway_effective (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (v : CorvajaZannier.FiniteExtensionPlace K L) :
    0 ≤ (finiteExtensionDivisorAway K L D P) v

    Removing one coefficient preserves effectiveness.

    source
    @[simp]
    theorem BGS.HasseWeil.finiteExtensionDivisorDegree_single (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (z : ℤ) :
    CorvajaZannier.finiteExtensionDivisorDegree K L (Finsupp.single P z) = z * ↑(CorvajaZannier.finiteExtensionPlaceDegree K L P)

    The degree of a divisor supported at one place.

    source
    theorem BGS.HasseWeil.finiteExtensionDivisorDegree_neg (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) :
    CorvajaZannier.finiteExtensionDivisorDegree K L (-D) = -CorvajaZannier.finiteExtensionDivisorDegree K L D

    Divisor degree changes sign under negation.

    source
    theorem BGS.HasseWeil.finiteExtensionDivisorDegree_sub (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D E : CorvajaZannier.FiniteExtensionDivisor K L) :
    CorvajaZannier.finiteExtensionDivisorDegree K L (D - E) = CorvajaZannier.finiteExtensionDivisorDegree K L D - CorvajaZannier.finiteExtensionDivisorDegree K L E

    Divisor degree respects subtraction.

    source
    theorem BGS.HasseWeil.finiteExtensionDivisorDegree_away (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) :
    CorvajaZannier.finiteExtensionDivisorDegree K L (finiteExtensionDivisorAway K L D P) = CorvajaZannier.finiteExtensionDivisorDegree K L D - D P * ↑(CorvajaZannier.finiteExtensionPlaceDegree K L P)

    Degree bookkeeping for the divisor away from the selected place.

    source
    theorem BGS.HasseWeil.single_coeff_le_of_effective (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) :
    Finsupp.single P (D P) ≤ D

    For an effective divisor, its one-place part is coefficientwise below it.

    source
    theorem BGS.HasseWeil.onePointRiemannSpace_le_of_effective (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) :
    CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (D P).toNat ≤ CorvajaZannier.finiteExtensionRiemannSpace K L D

    The one-point space using the selected coefficient embeds in the full Riemann space of an effective divisor.