The wild different bound for number fields #
At a prime w of a number-field extension L/K, the exponent of the different is at most
e(w/v) - 1 + v_w(e(w/v)). The local different bound is transported through the canonical
completions at v and w. Both the different exponent and the valuation of the natural number
e(w/v) are expressed as multiplicities of ideals of ๐ L.
In the wild case, the existing lower-bound criterion also gives e(w/v) as a lower bound.
Neither bound is always an equality: the dyadic examples โ(i) and โ(โ2) attain different
endpoints.
References #
- J. Neukirch, Algebraic Number Theory, Chapter III, Theorem 2.6.
- J.-P. Serre, Local Fields, Chapter III, ยง6, Proposition 13.
theorem
IsDedekindDomain.HeightOneSpectrum.multiplicity_differentIdeal_le_ramificationIdx_sub_one_add_multiplicity_span
{K : Type u_1}
{L : Type u_2}
[Field K]
[NumberField K]
[Field L]
[NumberField L]
[Algebra K L]
(v : HeightOneSpectrum (NumberField.RingOfIntegers K))
(w : HeightOneSpectrum (NumberField.RingOfIntegers L))
[w.asIdeal.LiesOver v.asIdeal]
:
The upper bound for the global different exponent. The multiplicity of w in the
different is at most e(w/v) - 1 plus the multiplicity of w in the ideal generated by
e(w/v).