Infinitely many totally ramified extensions in equal characteristic

Let K be a nonarchimedean local field and 0 < n with (n : K) = 0, that is, K has characteristic p > 0 and p ∣ n. Then σ_K(n) = totallyRamifiedOfDegree K n is infinite. This is the converse half of Serre's finiteness dichotomy: outside this case the discriminant exponents of the members of σ_K(n) are bounded, and the mass formula forces σ_K(n) to be finite.

The witnesses are Serre's explicit family. For a uniformizer π of K and m ≥ 1, the polynomial X ^ n + π ^ m X + π is Eisenstein, and it has a root in SeparableClosure K because its derivative is the nonzero constant π ^ m. The root generates a member of σ_K(n) whose discriminant exponent is n * m, so these members are pairwise distinct.

The discriminant exponent is computed by natCast_discriminantExponent_adjoin_eq_iInf_of_eisenstein, the Eisenstein formula for a subextension of SeparableClosure K generated by a root of an Eisenstein polynomial.

Main results

• TauCeti.exists_mem_totallyRamifiedOfDegree_discriminantExponent_eq: if 0 < n and (n : K) = 0, then every multiple n * m with 0 < m is the discriminant exponent of a member of σ_K(n).
• TauCeti.infinite_totallyRamifiedOfDegree: if 0 < n and (n : K) = 0, then σ_K(n) is infinite.

References

• 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 Sér. A 286 (1978), 1031–1036, Remarque 1°.
• J.-P. Serre, Local Fields, Chapter III, §6, Proposition 13.

theorem TauCeti.exists_mem_totallyRamifiedOfDegree_discriminantExponent_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) (hnK : ↑n = 0) {m : ℕ} (hm : 0 < m) : ∃ L ∈ totallyRamifiedOfDegree K n, L.discriminantExponent = n * m

Serre's family of wild extensions. If 0 < n and (n : K) = 0, then for every 0 < m some member of σ_K(n) has discriminant exponent n * m: it is generated by a root of X ^ n + π ^ m X + π for a uniformizer π of K.

theorem TauCeti.infinite_totallyRamifiedOfDegree {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) (hnK : ↑n = 0) : (totallyRamifiedOfDegree K n).Infinite

Infinitely many totally ramified extensions in equal characteristic. If 0 < n and (n : K) = 0, that is, K has characteristic p > 0 with p ∣ n, then σ_K(n) is infinite: its discriminant exponents are unbounded.