Module

Exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached

1 declaration indexed from sourceView source ↗

Module documentation

Vanishing of the index of specialty for sufficiently large multiples of a place divisor.

Imports5

Imported by3

theorem

exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached

L30 ↗

AlgebraicCurve.exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace Exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K ↥(LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (Q : Place K F) :
    ∃ n : ℕ, indexOfSpecialty ((n : ℤ) • Finsupp.single Q (1 : ℤ)) = 0

Module documentation

Declarations

exists_indexOfSpecialty_nsmul_single_eq_zero_of_genusReached