Weak approximation for the places of an algebraic function field #
Finitely many distinct places of a function field F/k impose independent conditions on F:
given pairwise distinct places P₁, …, Pₙ, target functions f₁, …, fₙ : F and prescribed
integers r₁, …, rₙ, there is a single g : F with ord_{Pᵢ} (g - fᵢ) = rᵢ for every i.
This is the weak approximation theorem, Stichtenoth, Algebraic Function Fields and Codes,
Theorem 1.3.1, in the equality form; it is TauCeti.Place.exists_forall_ord_sub_eq.
The analytic content is not reproved here. TauCeti.Valuation.exists_forall_sub_eq_exp already
proves weak approximation for an arbitrary finite family of surjective, pairwise inequivalent
ℤᵐ⁰-valued valuations of a field, by way of Mathlib's
AbsoluteValue.denseRange_algebraMap_pi. What a place adds is exactly the two hypotheses that
engine consumes: its valuation is surjective by normalization, and distinct places have
inequivalent valuations because a normalized valuation is determined by its equivalence class
(TauCeti.Place.eq_of_isEquiv). So the work in this file is to package the conclusion in the
additive ord vocabulary and to draw the consequences the divisor theory uses.
Taking all targets to be 0 prescribes the orders themselves
(TauCeti.Place.exists_forall_ord_eq), which is the form in which independence of places is
usually met: a function may be asked to have a simple zero at one place and a pole of any
prescribed order at each of finitely many others. Taking all prescribed orders to be 1
instead makes g agree with each target to first order. When the targets are integral, so is
g; choosing integral lifts of prescribed residue classes therefore shows that the residue
maps of finitely many distinct places are simultaneously surjective
(TauCeti.Place.exists_forall_residue_eq), a Chinese-remainder statement for the places of F.
Main results #
TauCeti.Place.exists_forall_ord_sub_eq: weak approximation (Stichtenoth, Theorem 1.3.1).TauCeti.Place.exists_forall_mem_valuation_sub_le: weak approximation along a finite set of places, as the boundv_P (g - f P) ≤ exp (r P).TauCeti.Place.exists_forall_ord_eqandTauCeti.Place.exists_ne_zero_forall_ord_eq: prescribed orders at finitely many distinct places, by an arbitrary and by a nonzero function.TauCeti.Place.exists_ord_eq_one_and_forall_mem_ord_eq_zero: a function with a simple zero at a given place which is a unit at each of finitely many other places.TauCeti.Place.exists_mem_integers_notMem_integers: the valuation rings of two distinct places are incomparable.TauCeti.Place.exists_forall_residue_eq: simultaneous surjectivity of the residue maps of finitely many distinct places.TauCeti.Place.exists_residue_eq_and_forall_mem_ord_eq: a prescribed residue at one place together with prescribed orders at finitely many others.
Implementation notes #
The families are indexed by a Finite type together with an injective map to Place k F,
matching the shape of the approximation engine. The Finset restatements
(TauCeti.Place.exists_forall_mem_ord_sub_eq and
TauCeti.Place.exists_forall_mem_ord_eq) are what the divisor theory, which meets places as
elements of the support of a divisor rather than as a numbered list, actually applies.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.3.
The weak approximation theorem for the places of an algebraic function field
(Stichtenoth, Theorem 1.3.1), in the equality form: for finitely many pairwise distinct places
P i, arbitrary target functions f i and arbitrary prescribed integers r i, some single
g : F satisfies ord_{P i} (g - f i) = r i for every i.
The prescription is an equality, not an inequality: the error g - f i is not merely small at
P i, its order there is exactly r i. In particular g - f i ≠ 0 whenever r i ≠ 0.
Prescribed orders: the orders of a function at finitely many distinct places may be
prescribed arbitrarily and independently. This is weak approximation with all targets 0, and
it is the statement that finitely many places of F are independent.
Prescribed orders realized by a nonzero function, which is the form the principal-divisor
map Fˣ → Divisor k F consumes. Because ord_P has the junk value ord_P 0 = 0, the witness
of TauCeti.Place.exists_forall_ord_eq can only fail to be nonzero when every prescribed order
is 0, and then a constant serves.
Weak approximation for a finite set of places, which is how the divisor theory meets them: the places of the support of a divisor carry no numbering.
Weak approximation along a finite set of places, in the multiplicative inequality form in
which the repartition filtrations meet it: some g : F satisfies
v_P (g - f P) ≤ exp (r P), that is ord_P (g - f P) ≥ -r P or g = f P, at every P ∈ s.
A global uniformizer at a place, away from finitely many others: some t : F has a
simple zero at P and is a unit of the valuation ring of every other place of s. Such a t
is in particular a prime element at P (TauCeti.Place.isUniformizer_iff_ord_eq_one), so a
uniformizer may always be chosen to interfere with no prescribed finite set of places.
A prescribed residue at one place, together with prescribed orders at finitely many others.
Compared with TauCeti.Place.exists_forall_residue_eq, only one residue is prescribed, but the
function is additionally required to be small — of prescribed order, in particular of
prescribed positive order — at each of the remaining places. This is the shape Stichtenoth's
count of the zeros of a function consumes: a lift of a residue basis at one place must not
interfere with the other places under consideration.
The valuation rings of two distinct places are incomparable: neither contains the other.
Together with TauCeti.Place.integers_injective this is the sense in which the places of F
are its maximal proper subrings containing k, no two of them comparable (Stichtenoth,
Theorem 1.1.13).
Approximation to first order: some g : F agrees with a prescribed target at each of
finitely many distinct places to first order, that is, up to an element of the maximal ideal
there.
Simultaneous evaluation at finitely many distinct places: any prescribed family of
residues, one in the residue field of each place, is realized by a single function of F that
is integral at all of them. Equivalently, the residue maps of finitely many distinct places are
jointly surjective on ⋂ᵢ 𝒪_{P i}; this is the Chinese remainder theorem for the places of a
function field.