AlgebraicCurve.CurveModel.exists_openKummerUnits_of_sum_eq_zero
Every sum-zero boundary residue vector is realized by an actual function whose orders off the boundary are divisible by the exponent.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra
open scoped BigOperators
namespace AlgebraicCurve.CurveModelLean source · statement
theorem exists_openKummerUnits_of_sum_eq_zero
{K F : Type} [Field K] [IsAlgClosed K]
[Field F] [Algebra K F] [IsCurveOver K F]
(M : CurveModel K F)
(ε : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
(S : Set (Place K F)) [Fintype S]
(v₀ : S) (n : ℕ+) (hchar : ((n : ℕ) : K) ≠ 0)
(a : S → ZMod (n : ℕ)) (ha : ∑ v : S, a v = 0) :
∃ u : Pic0.openKummerUnits K F S n,
Pic0.openKummerResidue S n u = Multiplicative.ofAdd a