The different exponent of a monogenic Galois extension

Suppose the integral closure of the valuation ring at a place is generated by one element x. For a finite Galois extension, the derivative of the minimal polynomial of x is the product of the displacements x - σ x over the nonidentity automorphisms. Taking the place order gives

d(P' | P) = ∑_{σ ≠ 1} ord_{P'}(x - σ x).

This is the local form of Hilbert's different formula needed for explicit ramification computations. In particular, a generating uniformizer at a totally ramified place supplies the monogenic hypothesis.

References

• J.-P. Serre, Local Fields, Chapter IV, §1.

theorem TauCeti.Place.differentExponent_eq_sum_ord_sub_aut_of_algebra_adjoin_eq_top (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [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'] [IsGalois F F'] {P' : Place k' F'} [DecidableEq Gal(F'/F)] {x : ↥(integralClosure (↥(restrict k F P').integers) F')} (hx : (↥(restrict k F P').integers)[x] = ⊤) : ↑(differentExponent k F P') = ∑ σ ∈ Finset.univ.erase 1, P'.ord ((algebraMap (↥(integralClosure (↥(restrict k F P').integers) F')) F') x - σ ((algebraMap (↥(integralClosure (↥(restrict k F P').integers) F')) F') x))

If an element generates the integral closure of a valuation ring in a finite Galois extension, the different exponent is the sum of the orders of its nontrivial Galois displacements.