Auxiliary file: sub_one_le_d—the bound n - 1 ≤ d (L) #
Footnote 1 of the paper refers to Corps locaux for the fact that c L = d L - n + 1 is a
nonnegative integer ([Serre 1978, p.1031, footnote 1][Serre1978]); in the ℕ-valued
model this is the bound n - 1 ≤ d L for L in sigma K n.
The classical route: for L / K totally ramified of degree n the residue degree is 1, so the
valuation of K composed with the norm is the valuation of L on the units of L, and d L is
the valuation of the discriminant, equal to the valuation of the different; and the different of a
totally ramified extension has valuation at least e - 1 = n - 1
([Serre 1979, Chap. III, §6][Serre1979]), with equality exactly in the tame case. In the hand-rolled
discIdeal model the natural approach is via the power basis of a uniformizer of L: its
discriminant is plus or minus the norm of the derivative of the (Eisenstein) minimal polynomial at
that uniformizer, and that derivative has valuation at least n - 1 term by term.
References #
- [Serre1978] J-P. Serre, Une «formule de masse» pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris 286 (1978), Série A, 1031–1036.
- [Serre1979] J-P. Serre, Local fields, Graduate Texts in Mathematics 67, Springer, 1979.
Every member of sigma K n is generated by a root of an Eisenstein polynomial—the extraction
converse to isTotallyRamified_adjoin. Route: integers L is a Dedekind domain (Krull–Akizuki
through the separable-finite route, IsIntegralClosure.isDedekindDomain); any maximal ideal Q
of integers L lies over 𝓂[K] (integrality) and contains maximalIdealAbove L, so
IsTotallyRamified puts the extension of 𝓂[K] inside Q ^ n; an element ξ of Q outside
Q ^ 2 then satisfies eisenstein_shape, so its minimal polynomial is Eisenstein of degree exactly
n and ξ generates L by dimension count. No fundamental identity summing the e i * f i to
n, no localness of integers L, and no norm computation is needed—the paper's valuation-based
argument (p.1032, around eq. (5)) is replaced by divisibility of ideal powers.
The discriminant ideal at an adjoined Eisenstein root—the equality behind the bound
sub_one_le_d_adjoin, and the input the change of variables consumes. discIdeal is generated by
the discriminant of the power basis: every generator of discIdeal is the discriminant of an
integral basis, whose transition matrix from the power basis is integral by monogenicity
(integers_eq_adjoin), so that discriminant is the squared determinant times the power-basis
discriminant—while the power basis is itself an integral basis and so contributes its own
discriminant. The generator is exhibited in the form norm_derivative_core produces, the
power-basis discriminant being plus or minus the norm of the derivative of g at ξ, which is what
makes it land in the n - 1-st power of 𝓂[K].
The discriminant bound at an adjoined Eisenstein root. discIdeal is generated by the
power-basis discriminant (discIdeal_eq_span), which lands in the n - 1-st power of 𝓂[K];
finiteness of the multiplicity comes from its being nonzero.
d L as a π-adic order, the form the change of variables consumes: the discriminant of the
power basis at an Eisenstein generator is an associate of π ^ d L. discIdeal being the span of
that discriminant, the multiplicity of 𝓂[K] in it is exactly the order of the generator.
The discriminant exponent of a totally ramified degree-n extension is at least n - 1.