Documentation

TauCeti.RingTheory.LaurentSeries.Level.Trace

The trace of a ramified Laurent-series level #

Let L = K⸨u⸩ be the ramified level of degree d over F = K⸨t⸩, where t = u ^ d. In the power basis 1, u, ..., u ^ (d - 1), multiplication by f has r-th diagonal coefficient the residue-zero exponent-congruence component of f, for every r. Hence, in every characteristic,

Tr_{L/F} (f) = d • contract d f 0,

so the trace keeps exactly the exponents of f divisible by d, multiplies them by d and reads them as exponents of t. On monomials, Tr (u ^ k) is d t ^ (k / d) when d ∣ k and 0 otherwise.

This is the trace on the coefficient of dt: the residue of g dt in the variable u, for g ∈ L, is that of g · d(u ^ d) = d g u ^ (d - 1) du. Comparing coefficients gives, in every characteristic, the residue formula for the trace

Res_t (Tr_{L/F} (g) dt) = Res_u (g dt).

When d is nonzero in K, every differential on L has the form g dt, so this is the formula Res_F ∘ Tr_{L/F} = Res_L for all differentials. When the characteristic of K divides d, the form dt = d u ^ (d - 1) du vanishes on L, so every g dt is zero there and the identity says nothing about other differentials such as u⁻¹ du.

On the actual level K⸨t ^ (1 / d)⸩ of the Puiseux field, the coefficient of t ^ j in the trace of x is d times the rational-exponent coefficient of t ^ j in x. For j = -1 this says that the residue of the trace of x dt is d times the rational-exponent residue of x dt, and it shows that the traces of x from levels n ∣ m differ by the factor m / n.

Main results #

source
theorem TauCeti.LaurentSeries.Level.trace_eq_nsmul_contract {K : Type u_1} [Field K] (d : ℕ+) (f : Level K d) :
(Algebra.trace (LaurentSeries K) (Level K d)) f = ↑d • LaurentSeries.contract d ((ringEquivLaurentSeries K d) f) 0

The trace of a ramified level. The trace of f from level d down to K⸨X⸩ is d times the residue-zero exponent-congruence component of f, in every characteristic.

source
@[simp]
theorem TauCeti.LaurentSeries.Level.coeff_trace {K : Type u_1} [Field K] (d : ℕ+) (f : Level K d) (j : ℤ) :
((Algebra.trace (LaurentSeries K) (Level K d)) f).coeff j = ↑d • ((ringEquivLaurentSeries K d) f).coeff (↑↑d * j)

The coefficient of t ^ j in the trace of f is d times the coefficient of u ^ (d * j) in f.

source
theorem TauCeti.LaurentSeries.Level.trace_parameter_zpow {K : Type u_1} [Field K] (d : ℕ+) (k : ℤ) :
(Algebra.trace (LaurentSeries K) (Level K d)) (parameter K d ^ k) = if ↑↑d ∣ k then ↑d • (HahnSeries.single (k / ↑↑d)) 1 else 0

The trace of the monomial u ^ k is d t ^ (k / d) when d ∣ k, and zero otherwise.

source
theorem TauCeti.LaurentSeries.Level.coeff_neg_one_trace {K : Type u_1} [Field K] (d : ℕ+) (g : Level K d) :
((Algebra.trace (LaurentSeries K) (Level K d)) g).coeff (-1) = ((ringEquivLaurentSeries K d) g * (LaurentSeries.derivative K) ((HahnSeries.single ↑↑d) 1)).coeff (-1)

Residue of the trace. For g in level d, the residue of Tr_{L/F} (g) dt is the residue in the level variable u of the form g dt, where dt = d(u ^ d).

source
@[simp]
theorem TauCeti.puiseuxField.coeff_trace_level {K : Type u_1} [Field K] (d : ℕ+) (x : ↥(level K d)) (j : ℤ) :
((Algebra.trace (LaurentSeries K) ↥(level K d)) x).coeff j = ↑d • (↑↑x).coeff ↑j

The trace of an actual level. For x in level d of the Puiseux field, the coefficient of t ^ j in its trace down to K⸨X⸩ is d times the coefficient of t ^ j in x. For j = -1 this is Res_t (Tr (x) dt) = d • Res_t (x dt), with the residue on the right taken among rational exponents.

source
theorem TauCeti.puiseuxField.trace_inclusion_level {K : Type u_1} [Field K] {n m : ℕ+} (h : n ∣ m) (x : ↥(level K n)) :
(Algebra.trace (LaurentSeries K) ↥(level K m)) ((IntermediateField.inclusion ⋯) x) = (↑m / ↑n) • (Algebra.trace (LaurentSeries K) ↥(level K n)) x

For n ∣ m, the trace from level m of an element of level n is m / n times its trace from level n.