AlgebraicCurve.Pic0.exists_kummer_representative_avoiding
A torsion class has a Kummer function whose divided divisor avoids any prescribed finite set. Both the function and its Kummer class are actual.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicCurve.Pic0Lean source · statement
theorem exists_kummer_representative_avoiding
{K F : Type*} [Field K] [Field F] [Algebra K F] [HasPrincipalDivisors K F]
(n : ℕ+) (x : torsion K F (n : ℕ)) (S : Finset (Place K F)) :
∃ (D : Divisor.degZero (K := K) (F := F)) (u : kummerUnits K F n),
mk D = x.1 ∧
(∀ v ∈ (D : Divisor K F).support, v ∉ S) ∧
(∀ v : Place K F, v.ord (u.val : F) = (n : ℤ) * (D : Divisor K F) v) ∧
Multiplicative.toAdd (kummerClass n u) = x