AlgebraicCurve.RROpens.exists_effective_sub_add_smul_single_mem_principal
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsEffectiveSubAddSmul
universe u v
open AlgebraicCurve ModuleLean source · statement
theorem _root_.AlgebraicCurve.RROpens.exists_effective_sub_add_smul_single_mem_principal {K : Type
u} {F : Type v} [Field K] [Field F] [Algebra K F]
[HasPrincipalDivisors K F] (g : ℕ) (Kc : Divisor K F)
(hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
(P : Place K F) (hP : P.deg = 1) (A : Divisor K F) (hA : Divisor.degree A = 0) :
∃ E : Divisor K F, (∀ v, 0 ≤ E v) ∧
E - (A + (g : ℤ) • Finsupp.single P 1) ∈ Divisor.principal (K := K) (F := F)