The trace near an unramified place

Let F' / k' be a finite separable extension of the algebraic function field F / k, and let P' be a place of F' over the place P of F. Classically, Tr_{F'/F} decomposes as the sum ∑_{Q' ∣ P} Tr_{F'_{Q'}/F_P} of the traces of the completions over P (Stichtenoth, Section IV.2). This file proves two completion-free consequences, for functions z that are regular at P' and vanish to order at least e(Q' ∣ P) · m at every other place Q' over P, so that the local traces at those places are negligible to order m.

• Local degree one. If e(P' ∣ P) = f(P' ∣ P) = 1, the completions at P' and at P coincide and the trace is, near P', the identity: ord_{P'} (Tr_{F'/F} z - z) ≥ m.
• Unramified over a rational place. If P is rational with uniformizer t and e(P' ∣ P) = 1, so that the completion at P' is F'_{P'}((t)) with F'_{P'} separable over k, the trace acts on expansions coefficientwise: Tr_{F'/F} z ≡ ∑_{i < m} Tr_{F'_{P'}/k} (aᵢ) tⁱ to order m, where ∑ aᵢ tⁱ is the expansion of z at P'. In residue form, res_{P,t} (Tr_{F'/F} v) = Tr_{F'_{P'}/k} (res_{P',t} v) for every v regular at the other places over P.

These identify the local components of a cotrace of Weil differentials with those of the differential it comes from, at places of arbitrary degree.

Both proofs work in the local model 𝒪'_P ⊇ 𝒪_P, the integral closure of the valuation ring of P in F', which is finite and free over 𝒪_P. Let x be a uniformizer of P and reduce modulo x ^ m: the trace of 𝒪'_P ⧸ x ^ m over 𝒪_P ⧸ x ^ m is the reduction of the trace (TauCeti.Algebra.trace_quotient_map_mk). By weak approximation some w is congruent to 1 at P' and to 0 at the other places over P, to order m; multiplication by its class is a projection onto the summand of 𝒪'_P ⧸ x ^ m belonging to P', through which z acts. When e = f = 1 that summand is free of rank one with basis the class of w, and the class of z is a • w for an a ∈ 𝒪_P congruent to z at P', so the trace of z is a modulo x ^ m (TauCeti.Algebra.trace_sub_one_mem_of_mul_self_sub_mem). Over a rational place with e = 1, the summand is free with basis functions whose expansions at P' are constant to order m and run over a k-basis βⱼ of F'_{P'}; on it z acts by the matrix ∑ᵢ [aᵢ] xⁱ, where [aᵢ] is the matrix of multiplication by aᵢ in the basis βⱼ, whose trace is ∑ᵢ Tr (aᵢ) xⁱ (TauCeti.Algebra.trace_sub_sum_mem_of_forall_mul_sub_sum_mem).

Main results

• TauCeti.Place.exists_sub_algebraMap_mem_filtration: at a place with e = f = 1, every regular function of F' is congruent to a regular function of F to any prescribed order.
• TauCeti.Place.algebraMap_trace_sub_mem_filtration: at a place with e = f = 1, the trace is the identity to order m near P'.
• TauCeti.Place.trace_sub_sum_mem_filtration: at an unramified place over a rational place, the trace acts on expansions as the coefficientwise trace of F'_{P'} / k, to order m.
• TauCeti.Place.residue_trace: in that situation, res_{P,t} (Tr_{F'/F} v) = Tr_{F'_{P'}/k} (res_{P',t} v).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section IV.2 and Remark 4.3.7.
• J.-P. Serre, Local Fields, GTM 67, Springer, 1979, Chapter II, §2 and §4.

theorem TauCeti.Place.exists_sub_algebraMap_mem_filtration (k : Type u_1) {k' : Type u_2} (F : Type u_3) {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (P' : Place k' F') (he : ramificationIdx F P' = 1) (hf : relativeDegree k F P' = 1) (n : ℕ) {z : F'} (hz : z ∈ P'.integers) : ∃ a ∈ (restrict k F P').integers, z - (algebraMap F F') a ∈ P'.filtration ↑n

Expansion at a place of local degree one: if e(P' ∣ P) = f(P' ∣ P) = 1, every function regular at P' is congruent to a function of F regular at P, to any prescribed order n.

theorem TauCeti.Place.algebraMap_trace_sub_mem_filtration (k : Type u_1) {k' : Type u_2} (F : Type u_3) {F' : Type u_4} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (P' : Place k' F') [Algebra.IsIntegral k k'] [Algebra.IsSeparable F F'] (hF' : IsFunctionField k' F') (he : ramificationIdx F P' = 1) (hf : relativeDegree k F P' = 1) (m : ℕ) {z : F'} (hz : z ∈ P'.integers) (hzQ : ∀ (Q' : Place k' F'), restrict k F Q' = restrict k F P' → Q' ≠ P' → z ∈ Q'.filtration (↑(ramificationIdx F Q') * ↑m)) : (algebraMap F F') ((Algebra.trace F F') z) - z ∈ P'.filtration ↑m

The trace is the identity near a place of local degree one. Let P' be a place of F' over P with e(P' ∣ P) = f(P' ∣ P) = 1. If z is regular at P' and vanishes to order at least e(Q' ∣ P) · m at every other place Q' of F' over P, then Tr_{F'/F} z is congruent to z at P' to order m.

The trace at an unramified place over a rational place

theorem TauCeti.Place.trace_sub_sum_mem_filtration {k : Type u_5} {F : Type u_6} {F' : Type u_7} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k F') [Algebra.IsSeparable k P'.ResidueField] {P : Place k F} (hPP' : restrict k F P' = P) {t : F} (ht : P.ord t = 1) (ht' : P'.ord ((algebraMap F F') t) = 1) (hF' : IsFunctionField k F') (hP : P.degree = 1) (m : ℕ) (z : ↥P'.integers) (hzQ : ∀ (Q' : Place k F'), restrict k F Q' = P → Q' ≠ P' → ↑z ∈ Q'.filtration (↑(ramificationIdx F Q') * ↑m)) : (Algebra.trace F F') ↑z - ∑ i : Fin m, (algebraMap k F) ((Algebra.trace k P'.ResidueField) ((PowerSeries.coeff ↑i) ((P'.powerSeriesExpansionResidueField ht') z))) * t ^ ↑i ∈ P.filtration ↑m

The trace commutes with expansions at an unramified place over a rational place. Let P be a rational place of F with uniformizer t, and let P' be a place of F' over P at which t is still a uniformizer, that is e(P' ∣ P) = 1, with residue field F'_{P'} separable over k. If z is regular at P' and vanishes to order at least e(Q' ∣ P) · m at every other place Q' over P, then, to order m at P,

Tr_{F'/F} z ≡ ∑_{i < m} Tr_{F'_{P'}/k} (aᵢ) tⁱ,

where ∑ aᵢ tⁱ is the expansion of z at P' with coefficients in F'_{P'}.

Classically, the completion of F' at P' is F'_{P'}((t)), whose trace over k((t)) is the coefficientwise trace, and the hypothesis on z makes the local traces at the other places over P negligible to order m.

theorem TauCeti.Place.residue_trace {k : Type u_5} {F : Type u_6} {F' : Type u_7} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P' : Place k F') [Algebra.IsSeparable k P'.ResidueField] {P : Place k F} (hPP' : restrict k F P' = P) {t : F} (ht : P.ord t = 1) (ht' : P'.ord ((algebraMap F F') t) = 1) (hF' : IsFunctionField k F') (hP : P.degree = 1) {v : F'} (hv : ∀ (Q' : Place k F'), restrict k F Q' = P → Q' ≠ P' → v ∈ Q'.integers) : (P.residue hP ht) ((Algebra.trace F F') v) = (P'.traceResidue ht') v

Residues commute with the trace at an unramified place over a rational place. Let P be a rational place of F with uniformizer t, and let P' be a place of F' over P at which t is still a uniformizer, with residue field F'_{P'} separable over k. For a function v regular at every other place of F' over P,

res_{P,t} (Tr_{F'/F} v) = Tr_{F'_{P'}/k} (res_{P',t} v).

This is the residue form of TauCeti.Place.trace_sub_sum_mem_filtration.