The cotrace of Weil differentials #
Let F' / k' be a finite separable extension of the algebraic function field F / k, with
k' / k finite separable. For every Weil differential ω of F / k there is exactly one Weil
differential ω' of F' / k' with
Tr_{k'/k} (ω' α) = ω (Tr_{F'/F} α)
for every repartition α of F' that is constant on the fibres over the places of F. This
ω' is the cotrace Cotr_{F'/F} ω (Stichtenoth, Definition 3.4.5 and Theorem 3.4.6). Its
divisor is (Cotr ω) = Con (ω) + Diff(F'/F), the identity from which the Hurwitz genus formula
follows (TauCeti.FieldTheory.FunctionField.Different.Hurwitz).
The construction follows Stichtenoth. Every repartition of F' is a fibre-constant repartition
modulo A_{F'}(B'), for any divisor B' of F', by weak approximation on each of the finitely
many fibres where the repartition is not already bounded by B'
(TauCeti.exists_sub_relativeRepartitionPullback_mem_adeleFiltration). With
B' = Con D + Diff(F'/F), the trace estimate TauCeti.repartitionTrace_mem_adeleFiltration
shows that α ↦ ω (Tr α) is well defined on A_{F'} ⧸ A_{F'}(B'), which gives a k-linear form
on A_{F'}; the trace form of k' / k turns it into a k'-linear one
(Module.Dual.traceCompEquiv).
This gives Con (ω) + Diff(F'/F) ≤ (Cotr ω). The reverse inequality is the sharpness of the trace
estimate (TauCeti.Place.exists_forall_valuation_le_and_trace_eq): if Cotr ω were bounded by
Con (ω) + Diff(F'/F) + P' for a place P' over P, then, as v_P (ω) is the largest bound the
local component ω_P respects, some function x with ord_P x ≥ -(v_P (ω) + 1) and ω_P x ≠ 0
would be the trace of a function of F' bounded by Con (ω) + Diff(F'/F) + P' along the fibre
over P, and Cotr ω would have to kill the corresponding fibre-constant repartition.
Both further properties of Stichtenoth's Proposition 3.4.11 follow from uniqueness. Multiplying
a fibre-constant repartition by a function of F keeps it fibre-constant and commutes with the
trace, so the cotrace is F-semilinear. In a tower F₀ ⊆ F₁ ⊆ F₂, a fibre-constant
repartition for F₂ / F₀ is also fibre-constant for F₂ / F₁, its entrywise trace to F₁ is
fibre-constant for F₁ / F₀, and the traces compose, so the cotrace is transitive.
Main definitions #
TauCeti.weilDifferentialCotrace: the cotraceΩ_F → Ω_{F'}, as ak-linear map.
Main results #
TauCeti.exists_mem_weilDifferentialFiltration_trace_apply_eq: existence of the cotrace, with its bound.TauCeti.trace_weilDifferentialCotrace_apply: the defining identity of the cotrace.TauCeti.eq_weilDifferentialCotrace: the cotrace is the only Weil differential ofF'satisfying it.TauCeti.weilDifferentialCotrace_mem_weilDifferentialFiltration: ifω ∈ Ω_F(D), thenCotr ω ∈ Ω_{F'}(Con D + Diff(F'/F)).TauCeti.weilDifferentialCotrace_eq_zero_iffandTauCeti.weilDifferentialCotrace_injective: the cotrace is injective.TauCeti.conorm_add_different_le_weilDifferentialDivisor:Con (ω) + Diff(F'/F) ≤ (Cotr ω)for a nonzero Weil differentialω.TauCeti.weilDifferentialDivisor_weilDifferentialCotrace: the divisor of the cotrace,(Cotr ω) = Con (ω) + Diff(F'/F)(Stichtenoth, Theorem 3.4.6).TauCeti.weilDifferentialCotrace_smul: the cotrace isF-semilinear,Cotr (f · ω) = f · Cotr ω(Stichtenoth, Proposition 3.4.11(a)).TauCeti.weilDifferentialCotrace_weilDifferentialCotrace: the cotrace is transitive in towers,Cotr_{F₂/F₁} ∘ Cotr_{F₁/F₀} = Cotr_{F₂/F₀}(Stichtenoth, Proposition 3.4.11(b)).
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.4, Definition 3.4.5, Theorem 3.4.6 and Proposition 3.4.11.
The cotrace #
Existence of the cotrace (Stichtenoth, Theorem 3.4.6): for a Weil differential ω of
F / k bounded by D, some Weil differential ω' of F' / k' bounded by
Con D + Diff(F'/F) satisfies Tr_{k'/k} (ω' α) = ω (Tr_{F'/F} α) on the fibre-constant
repartitions α of F'.
Uniqueness of the cotrace (Stichtenoth, Theorem 3.4.6): two Weil differentials of F'
whose values on the fibre-constant repartitions have the same traces to k are equal.
The cotrace of a Weil differential Cotr_{F'/F} ω (Stichtenoth, Definition 3.4.5): the
unique Weil differential of F' / k' with Tr_{k'/k} (Cotr ω α) = ω (Tr_{F'/F} α) for every
fibre-constant repartition α of F'. It is characterized by
TauCeti.trace_weilDifferentialCotrace_apply and TauCeti.eq_weilDifferentialCotrace.
Equations
- TauCeti.weilDifferentialCotrace k' F' hF hF' = { toFun := fun (ω : ↥(TauCeti.weilDifferentialSpace k F)) => ⟨TauCeti.cotraceAux✝ hF hF' ω, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The defining identity of the cotrace: Tr_{k'/k} (Cotr ω α) = ω (Tr_{F'/F} α) for every
fibre-constant repartition α of F'.
The cotrace is the only Weil differential with its defining identity (Stichtenoth, Theorem 3.4.6).
The cotrace raises the bound by the different (Stichtenoth, Theorem 3.4.6): if ω is
bounded by D, then Cotr ω is bounded by Con D + Diff(F'/F).
The cotrace is injective: Cotr ω = 0 only for ω = 0, because the trace of the
fibre-constant repartitions is onto A_F.
The cotrace is injective.
The cotrace is F-semilinear (Stichtenoth, Proposition 3.4.11(a)):
Cotr (f · ω) = f · Cotr ω for a function f of F, which acts on the Weil differentials of
F' through F → F'.
The divisor of the cotrace is at least Con (ω) + Diff(F'/F) (Stichtenoth,
Theorem 3.4.6), for a nonzero Weil differential ω of F / k.
The divisor of the cotrace (Stichtenoth, Theorem 3.4.6): (Cotr ω) = Con (ω) + Diff(F'/F)
for every nonzero Weil differential ω of F / k.
The cotrace in a tower #
The cotrace is transitive in towers (Stichtenoth, Proposition 3.4.11(b)): for finite
separable extensions F₀ ⊆ F₁ ⊆ F₂ of function fields, with finite separable extensions
k₀ ⊆ k₁ ⊆ k₂ of their constant fields, Cotr_{F₂/F₁} ∘ Cotr_{F₁/F₀} = Cotr_{F₂/F₀}.