Nyll.JacobianVarieties.Picard.DivisionPointDivisors

Module documentation

Divisor representatives of actual division points

Given the Picard point equivalence supplied by exists_pic0_algPoints_equivariant_of_abelJacobi, an actual division point has a divisor representative avoiding any prescribed finite set, together with a function realizing its division relation. This lemma does not assert the later monodromy or cohomology comparison.

theorem

exists_divisor_of_algPoint_division

L29 ↗

JacobianVarieties.Picard.exists_divisor_of_algPoint_division

Documentation

Moving the inverse image of an algebraic division point supplies the division function and the support avoidance needed for Weil evaluation.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Picard

Lean source · statement

theorem exists_divisor_of_algPoint_division
    {K Ω F : Type} [Field K] [Field Ω] [Algebra K Ω]
    [Field F] [Algebra Ω F] [HasPrincipalDivisors Ω F]
    {J : Scheme} {b : J ⟶ Spec (.of K)}
    (G : RelativeGroupLaw K b) (hc : G.IsCommutative)
    (e : Pic0 Ω F ≃+ G.AlgPoints hc Ω)
    (n : ℕ) (Q : G.AlgPoints hc Ω)
    (B : Divisor.degZero (K := Ω) (F := F))
    (hQ : n • Q = e (Pic0.mk B)) (S : Finset (Place Ω F)) :
    ∃ (E : Divisor.degZero (K := Ω) (F := F)) (f : F),
      e (Pic0.mk E) = Q ∧
      (∀ v ∈ (E : Divisor Ω F).support, v ∉ S) ∧
      f ≠ 0 ∧
      ∀ v : Place Ω F, v.ord f = (n : ℤ) * (E : Divisor Ω F) v -
        (B : Divisor Ω F) v

Module documentation

Divisor representatives of actual division points

Declarations

exists_divisor_of_algPoint_division