The complementary module of a place, by valuations #
Let F' / k' be an extension of the algebraic function field F / k with F' / F finite and
separable, let P be a place of F / k, and let 𝒪'_P be the integral closure of its valuation
ring 𝒪_P in F'. The complementary module
C_P = {z ∈ F' | Tr_{F'/F} (z · 𝒪'_P) ⊆ 𝒪_P}
is Mathlib's trace dual Submodule.traceDual 𝒪_P F 1 of the local model. Stichtenoth describes
it as t · 𝒪'_P for an element t with v_{P'}(t) = -d(P' ∣ P) at every place P' above P
(Proposition 3.4.2 and Definition 3.4.3); this file proves the description in the form in which
it is used, as a valuation criterion:
z ∈ C_P ↔ ∀ P' ∣ P, v_{P'}(z) ≤ exp d(P' ∣ P).
Its consequence TauCeti.Place.valuation_trace_le_exp is the local estimate behind the trace of
repartitions, and so behind the divisor of the cotrace of a Weil differential: if
ord_{P'}(z) ≥ -(e(P' ∣ P) · n + d(P' ∣ P)) at every P' above P, then
ord_P (Tr_{F'/F} z) ≥ -n. The estimate is sharp: relaxing the bound by one at a single place
P' over P makes every x ∈ F with ord_P x ≥ -(n + 1) a trace, which is what pins the divisor
of the cotrace down exactly.
The criterion is read off the different ideal 𝔡 of the local model, which is the inverse of
C_P as a fractional ideal: z ∈ C_P exactly when z · 𝔡 ⊆ 𝒪'_P
(TauCeti.mem_traceDual_one_iff_forall_mem_differentIdeal). The order at P' of an
element of 𝔡 is at least d(P' ∣ P), with equality for an element of 𝔡 outside the
(d + 1)-st power of the centre of P'; and 𝒪'_P is the intersection of the valuation rings
of the places above P (TauCeti.Place.isIntegral_iff_forall_restrict_eq_mem_integers), which
is where the constant field k' has to be integral over k.
Main results #
TauCeti.Place.differentExponent_le_ord_of_mem_differentIdealandTauCeti.Place.exists_mem_differentIdeal_ord_eq: the smallest order atP'of a nonzero element of the different ideal of the local model isd(P' ∣ P).TauCeti.Place.valuation_le_exp_differentExponent_of_mem_traceDual: an element of the complementary module has order at least-d(P' ∣ P)atP'.TauCeti.Place.mem_traceDual_iff_forall_valuation_le: the valuation criterion for the complementary module (Stichtenoth, Proposition 3.4.2 and Definition 3.4.3).TauCeti.Place.valuation_trace_le_exp: the trace estimate at a place.TauCeti.Place.exists_forall_valuation_le_and_trace_eq: the trace estimate is sharp.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Definition 3.4.1, Proposition 3.4.2, Definition 3.4.3 and the proof of Theorem 3.4.6.
Elements of the different ideal vanish to order at least d(P' ∣ P) at P': the
different ideal of the local model is divisible by the d(P' ∣ P)-th power of the centre of
P'.
Some element of the different ideal vanishes to order exactly d(P' ∣ P) at P': the
(d + 1)-st power of the centre of P' does not divide the different ideal, so the different
ideal has an element outside it.
An element of the complementary module has order at least -d(P' ∣ P) at P': it
multiplies an element of the different ideal of order exactly d(P' ∣ P) into 𝒪'_P, whose
functions are regular at P'.
The valuation criterion for the complementary module (Stichtenoth, Proposition 3.4.2 and
Definition 3.4.3): an element z of F' satisfies Tr_{F'/F} (z · 𝒪'_P) ⊆ 𝒪_P exactly when
v_{P'}(z) ≤ exp d(P' ∣ P), that is ord_{P'} z ≥ -d(P' ∣ P) for z ≠ 0, at every place P' of
F' / k' lying over P.
The trace estimate at a place: if z ∈ F' has order at least
-(e(P' ∣ P) · n + d(P' ∣ P)) at every place P' of F' / k' over P, then its trace to F has
order at least -n at P. Multiplying z by a function of order n at P moves it into the
complementary module C_P, whose traces are regular at P.
The trace estimate is sharp (Stichtenoth, proof of Theorem 3.4.6): relaxing the bound of
TauCeti.Place.valuation_trace_le_exp by one at a single place P' over P relaxes the bound on
the traces by one. Every x ∈ F with ord_P x ≥ -(n + 1) is the trace of some z ∈ F' with
ord_{Q'} z ≥ -(e(Q' ∣ P) · n + d(Q' ∣ P)) at the places Q' ≠ P' over P and
ord_{P'} z ≥ -(e(P' ∣ P) · n + d(P' ∣ P) + 1).