The trace of the powers of a prime, through the different

Let B be a Dedekind domain, module-finite over a Dedekind domain A with Frac B / Frac A separable, and let P be a nonzero prime of B which is the only prime above an ideal p of A, so that p · B = P ^ e. Write d for the multiplicity of P in the different ideal 𝔡(B/A). The trace dual of B is 𝔡⁻¹, so the integral trace carries P ^ m into p ^ r exactly when P ^ m lies in the fractional ideal p ^ r 𝔡⁻¹. Its P-adic valuation is e r - d, and its valuation at every other prime of B is nonpositive, since P is the only prime above p; so the condition is exactly e r ≤ m + d. When A is a discrete valuation ring with maximal ideal p, every ideal of A is a power of p and the criterion determines the image completely:

Tr(P ^ m) = p ^ ((m + d) / e),

with the division of natural numbers. This is the trace side of the theory of the different, in the form used to compute the norm on the unit filtration of an extension of local fields: the expansion N(1 + x) = 1 + Tr(x) + ⋯ + N(x) has trace terms whose valuations the formula reads off (Serre, Local Fields, Chapter V, §3).

The proof rests on the trace criterion TauCeti.dvd_differentIdeal_iff_forall_intTrace_mem, applied to the factorization P ^ (e r - m) * P ^ m = p ^ r · B when m ≤ e r; when m > e r the inclusion Tr(P ^ m) ⊆ Tr(p ^ r · B) ⊆ p ^ r holds for free.

Main results

• TauCeti.map_intTrace_pow_le_pow_iff: Tr(P ^ m) ⊆ p ^ r ↔ e r ≤ m + d.
• TauCeti.map_intTrace_pow_eq_maximalIdeal_pow: for A a discrete valuation ring, Tr(P ^ m) = 𝓂_A ^ ((m + d) / e).

References

• J.-P. Serre, Local Fields, Chapter III (the different) and Chapter V, §3.

theorem TauCeti.map_intTrace_pow_le_pow_iff (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} {P : Ideal B} [P.IsPrime] {e : ℕ} (hP : P ≠ ⊥) (hPe : Ideal.map (algebraMap A B) p = P ^ e) (m r : ℕ) : Submodule.map (Algebra.intTrace A B) (Submodule.restrictScalars A (P ^ m)) ≤ p ^ r ↔ e * r ≤ m + multiplicity P (differentIdeal A B)

The trace of a power of the prime above p. If p · B = P ^ e for an ideal p of A and a nonzero prime P of B, the integral trace carries P ^ m into p ^ r exactly when e * r ≤ m + d, where d is the multiplicity of P in the different ideal.

theorem TauCeti.map_intTrace_pow_eq_maximalIdeal_pow (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDomain A] [IsDiscreteValuationRing A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {P : Ideal B} [P.IsPrime] {e : ℕ} (hP : P ≠ ⊥) (hPe : Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) = P ^ e) (m : ℕ) : Submodule.map (Algebra.intTrace A B) (Submodule.restrictScalars A (P ^ m)) = IsLocalRing.maximalIdeal A ^ ((m + multiplicity P (differentIdeal A B)) / e)

The trace of a power of the prime above the maximal ideal of a discrete valuation ring. If A is a discrete valuation ring with maximal ideal 𝓂_A and 𝓂_A · B = P ^ e for a nonzero prime P of B, the image of P ^ m under the integral trace is 𝓂_A ^ ((m + d) / e), where d is the multiplicity of P in the different ideal and the division is that of natural numbers.