The trace of a quotient by a power of a prime

Let B be a Dedekind domain over a commutative ring A, let p be a maximal ideal of A with residue field κ = A ⧸ p, and let P be a maximal ideal of B with p · B ⊆ P ^ n, so that B ⧸ P ^ n is a κ-algebra. This file computes the trace of that algebra:

Tr_{(B ⧸ P ^ n) / κ} (z) = n · Tr_{(B ⧸ P) / κ} (z).

The P-adic filtration of B ⧸ P ^ n has n graded pieces, each of them a copy of the residue field B ⧸ P on which multiplication by z acts as multiplication by the residue of z; the trace of an endomorphism of a filtered vector space is the sum of the traces on the pieces, so the n copies contribute n equal summands. The induction runs over one step of the filtration at a time, through the short exact sequence

0 → B ⧸ P --· a--> B ⧸ P ^ (n + 1) → B ⧸ P ^ n → 0,

where a is any element of P ^ n not in P ^ (n + 1); injectivity of multiplication by a and exactness in the middle are the two Dedekind facts Ideal.IsPrime.mem_pow_mul and Ideal.exists_mul_add_mem_pow_succ, and the trace identity is LinearMap.trace_eq_add_of_exact.

The formula is what makes the tame case of Dedekind's different theorem work: it produces an element of B ⧸ P ^ e with nonzero trace as soon as the residue extension is separable and the characteristic of κ does not divide e (see TauCeti.RingTheory.DedekindDomain.Different, where it is combined with Mathlib's trace computation for B ⧸ p · B, Algebra.trace_quotient_eq_of_isDedekindDomain).

Main results

• Algebra.trace_quotient_pow_mk: the trace formula Tr_{B ⧸ P ^ n} = n · Tr_{B ⧸ P}.

theorem Algebra.trace_quotient_pow_mk {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain B] {p : Ideal A} [p.IsMaximal] {P : Ideal B} [P.IsMaximal] [Module.Finite A B] (hP : P ≠ ⊥) (n : ℕ) [instA : Algebra (A ⧸ p) (B ⧸ P ^ n)] [instT : IsScalarTower A (A ⧸ p) (B ⧸ P ^ n)] [Algebra (A ⧸ p) (B ⧸ P)] [IsScalarTower A (A ⧸ p) (B ⧸ P)] (z : B) : (trace (A ⧸ p) (B ⧸ P ^ n)) ((Ideal.Quotient.mk (P ^ n)) z) = n • (trace (A ⧸ p) (B ⧸ P)) ((Ideal.Quotient.mk P) z)

The trace of a quotient by a prime power. For P a maximal ideal of a Dedekind domain B that is module-finite over A, and p a maximal ideal of A making both B ⧸ P ^ n and B ⧸ P algebras over the residue field A ⧸ p, the trace of the residue of z in B ⧸ P ^ n is n times its trace in the residue field B ⧸ P.

The two IsScalarTower hypotheses pin the algebra structures to the ones induced by A → B; they are what Ideal.Quotient.algebraQuotientOfLEComap provides, and they hold for B ⧸ P ^ n exactly when p · B ⊆ P ^ n.