The weak approximation theorem to Weierstrass gap theorem…

TheoremThe weak approximation theorem #

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.

TauCeti.Place.exists_forall_ord_sub_eq.{u, v, u_1} {k : Type u} {F : Type v} [Field k] [Field F]
  [Algebra k F] {ι : Type u_1} [Finite ι] {P : ι → TauCeti.Place k F} (hP : Function.Injective P)
  (f : ι → F) (r : ι → ℤ) : ∃ g, ∀ (i : ι), (P i).ord (g - f i) = r i

Lean

Formalized in Tau Ceti as TauCeti.Place.exists_forall_ord_sub_eq.

Sources

LeanTauCeti.Place.exists_forall_ord_sub_eq

Used by 43

Used byPerfect local Tate duality for E[m] · The Hurwitz genus formula for y² = x³ - x over K(x), as a numerical identity · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · Serre duality in degree zero · Serre duality, in dimensions · Serre duality on X_F, in dimensions · The Riemann–Roch theorem for line bundles, in Serre-duality form · The Riemann–Roch theorem on X_F in dimension form · A curve of genus zero with a divisor of degree one has nodal reduction · TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual · The Abel–Jacobi map into the degree-zero Picard fppf sheaf · The Abel–Jacobi map of a curve of positive genus separates points over every field extension · The degree-zero Picard functor Pic⁰_{X/S} · The points of an elliptic curve form Pic⁰ of its projective model · The Riemann–Roch theorem · The Riemann–Roch theorem with the sheaf of differentials · Belyi's theorem, existence direction · Abhyankar's lemma (Stichtenoth, Theorem 3.9.1) · High powers of a transcendental function have pole divisors whose section ring is generated in degree one · Riemann's theorem · The abstract residue theorem (Stichtenoth, (1.45)) · The anti-equivalence between regular proper curves and algebraic function fields over a field k · The duality theorem, in dimensions · The genus of a smooth projective plane curve (Fulton, *Algebraic Curves*, Section 8.3) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · The residue theorem (Stichtenoth, Corollary 4.3.3) · The Riemann–Roch identity, read as duality · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · Castelnuovo's inequality (Stichtenoth, Theorem 3.11.3) · Clifford's theorem · Dedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · Hilbert's different formula · Riemann's inequality (Stichtenoth, Corollary 3.11.4) · Strong approximation (Stichtenoth, Theorem 1.6.5) · The Artin--Schreier genus formula, cross-multiplied for a possible constant-field extension · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz bound (Stichtenoth, Exercise 3.18) · The residue theorem for k(x) (Stichtenoth, Corollary 4.3.3, for k(x))

TheoremWeierstrass gap theorem (Stichtenoth, Theorem 1.6.8)#

at a rational place of a function field with integrally closed constants and genus g, there are exactly g gaps.

TauCeti.Place.card_weierstrassGaps.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k] [Field F]
  [Algebra k F] (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  {P : TauCeti.Place k F} (hP : P.degree = 1) : P.weierstrassGaps.card = TauCeti.genus k F