Moving a divisor within its class to avoid finitely many places

Every divisor class of an algebraic function field contains a representative whose support misses any prescribed finite set of places:

∀ D, ∀ s : Finset (Place k F), ∃ D' ~ D, Disjoint D'.support s.

Weak approximation is what makes this true. Finitely many distinct places impose independent conditions on F, so there is a function whose order at each place of s is exactly the negative of the coefficient of D there; adding its divisor cancels D on s and changes nothing about the class.

Main results

• TauCeti.Divisor.exists_linearlyEquivalent_disjoint_support: the statement above.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 1.3.1 (weak approximation) and Definition 1.4.3 (linear equivalence).
• J. Silverman, The Arithmetic of Elliptic Curves, III.8 — the divisor construction of the Weil pairing, where evaluating one function on another's divisor requires exactly this move.

theorem TauCeti.Divisor.exists_linearlyEquivalent_disjoint_support {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) (s : Finset (Place k F)) : ∃ (D' : Divisor k F), (Place.orderSystem hF).LinearlyEquivalent D D' ∧ Disjoint D'.support s

Every divisor class has a representative avoiding a given finite set of places.

Evaluating a function on a divisor requires the divisor's support to miss the function's zeros and poles; this is what makes that arrangeable, by replacing the divisor with a linearly equivalent one that avoids them. Weil reciprocity and the divisor construction of the Weil pairing both need the move.