The upper bound for the different exponent

Let L/K be a finite separable extension of nonarchimedean local fields with compatible valuations, of ramification index e = e(L/K), and suppose that e is nonzero in L, as it is in mixed characteristic. Then the different exponent satisfies

d(L/K) ≤ e − 1 + v_L(e),

where v_L(e) = TauCeti.natCastValuation L e is the normalized valuation of e in L. Together with the lower bound e ≤ d(L/K) of a wildly ramified extension, this is the second half of Dedekind's different theorem: e − 1 ≤ d(L/K) ≤ e − 1 + v_L(e), with equality on the left exactly in the tame case.

The bound is proved by factoring L/K through its maximal unramified subextension L₀. The different exponent and the ramification index of L/K are those of the totally ramified extension L/L₀, whose ring of integers is generated by a root of an Eisenstein polynomial, and for such a generator the bound is read off from the derivative of that polynomial.

Neither endpoint is forced in the wild case: ℚ₂(i)/ℚ₂ has d = e = 2, while ℚ₂(√2)/ℚ₂ has d = 3 = e − 1 + v_L(e).

Main results

• TauCeti.differentExponent_le_ramificationIndex_sub_one_add_natCastValuation: the upper bound d(L/K) ≤ e − 1 + v_L(e).
• TauCeti.differentExponent_bounds_of_wild: for a wildly ramified extension, e ≤ d(L/K) ≤ e − 1 + v_L(e).

References

• J.-P. Serre, Corps Locaux, Chapter III, §6, Proposition 13.
• J. Neukirch, Algebraic Number Theory, Chapter III, Theorem 2.6.

theorem TauCeti.differentExponent_le_ramificationIndex_sub_one_add_natCastValuation {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L] (he : ↑(ramificationIndex K L) ≠ 0) : differentExponent K L ≤ ramificationIndex K L - 1 + natCastValuation L (ramificationIndex K L) he

The upper bound of Dedekind's different theorem. If the ramification index e(L/K) is nonzero in L, the different exponent of L/K is at most e(L/K) − 1 + v_L(e(L/K)).

theorem TauCeti.differentExponent_bounds_of_wild {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L] (hwild : IsWildlyRamified K L) (he : ↑(ramificationIndex K L) ≠ 0) : ramificationIndex K L ≤ differentExponent K L ∧ differentExponent K L ≤ ramificationIndex K L - 1 + natCastValuation L (ramificationIndex K L) he

The different exponent of a wildly ramified extension lies between e(L/K) and e(L/K) − 1 + v_L(e(L/K)), provided e(L/K) is nonzero in L.