Strong approximation for an algebraic function field

Weak approximation (TauCeti.Place.exists_forall_mem_ord_sub_eq) prescribes the behaviour of a function at finitely many places of F / k and says nothing whatever about the remaining ones. Strong approximation keeps that prescription and adds regularity at every place of a set S which misses at least one place of F / k: given such an S, a finite subset s ⊆ S, targets f P and prescribed orders r P, there is a single x : F with

ord_P (x - f P) = r P for every P ∈ s, and x ∈ 𝒪_P for every P ∈ S outside s.

Some freedom is what pays for the extra control, and the properness of S is exactly that freedom: for S the set of all places the statement is false, because a function regular at every place is a constant (TauCeti.Place.coe_algebraicClosure_eq_iInter_integers).

This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Theorem 1.6.5. Unlike weak approximation it is a consequence of Riemann's theorem, and it is the form of approximation that consumers working inside a holomorphy ring 𝒪_S want.

Main results

• TauCeti.Place.exists_forall_mem_valuation_sub_le_and_forall_mem_integers: strong approximation in the inequality form, ord_P (x - f P) ≥ r P on s and integrality on the rest of S.
• TauCeti.Place.exists_forall_mem_ord_sub_eq_and_forall_mem_integers: strong approximation (Stichtenoth, Theorem 1.6.5), with the orders on s prescribed exactly.

Implementation notes

The proof is the repartition-space argument. Take a place Q ∉ S and let E be the divisor with coefficient -r P at each P ∈ s and n copies of Q, with n large enough that E is nonspecial; the enlargement happens at Q alone, so it disturbs no coefficient of E at a place of S. Then A_F(E) + F = A_F (TauCeti.adeleFiltration_sup_diagonalRepartitions_eq_repartitionSpace_iff), so the repartition carrying f P at each P ∈ s and 0 elsewhere differs from a constant x by a repartition bounded by E. Reading that bound off place by place gives both conclusions at once: at P ∈ s it is the approximation ord_P (x - f P) ≥ r P, and at the other places of S, where E has coefficient 0 and the repartition has entry 0, it is the integrality of x.

The inequality form is stated multiplicatively, as v_P (x - f P) ≤ exp (-r P), for the reason recorded in TauCeti/FieldTheory/FunctionField/Repartition/Basic.lean: the additive reading r P ≤ ord_P (x - f P) is wrong at x = f P, where the junk value ord_P 0 = 0 would exclude an exact hit whenever r P > 0. No such guard is needed in the equality form, whose conclusion ord_P (x - f P) = r P already forces x ≠ f P when r P ≠ 0.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.6 (Theorem 1.6.5).

theorem TauCeti.Place.exists_forall_mem_valuation_sub_le_and_forall_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {S : Set (Place k F)} (hS : S ≠ Set.univ) {s : Finset (Place k F)} (hsS : ↑s ⊆ S) (f : Place k F → F) (r : Place k F → ℤ) : ∃ (x : F), (∀ P ∈ s, P.valuation (x - f P) ≤ WithZero.exp (-r P)) ∧ ∀ P ∈ S, P ∉ s → x ∈ P.integers

Strong approximation, in the inequality form (Stichtenoth, Theorem 1.6.5): for a set S of places of F / k that is not all of them and a finite subset s ⊆ S, some x : F approximates the target f P to order r P at every P ∈ s and is regular at every place of S outside s.

The approximation is the multiplicative bound v_P (x - f P) ≤ exp (-r P), which reads ord_P (x - f P) ≥ r P at every place where x ≠ f P and is satisfied outright where x = f P.

theorem TauCeti.Place.exists_forall_mem_ord_sub_eq_and_forall_mem_integers {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {S : Set (Place k F)} (hS : S ≠ Set.univ) {s : Finset (Place k F)} (hsS : ↑s ⊆ S) (f : Place k F → F) (r : Place k F → ℤ) : ∃ (x : F), (∀ P ∈ s, P.ord (x - f P) = r P) ∧ ∀ P ∈ S, P ∉ s → x ∈ P.integers

Strong approximation (Stichtenoth, Theorem 1.6.5): for a set S of places of F / k that is not all of them and a finite subset s ⊆ S, some x : F satisfies ord_P (x - f P) = r P at every P ∈ s and is regular at every place of S outside s.

The orders on s are prescribed exactly, as in weak approximation (TauCeti.Place.exists_forall_mem_ord_sub_eq); what strong approximation adds is the regularity of x at the remaining places of S, at the price of requiring S to be proper.