Countability of totally ramified extensions of fixed degree

For a nonarchimedean local field K, the family totallyRamifiedOfDegree K n inside its separable closure is countable. This permits exchanging its sum with a nonnegative integral in the mass formula, including in equal characteristic where the family can be infinite.

Finite coefficient quotients give a countable family of monic Eisenstein polynomials of degree n approximating all such polynomials. The uniform root-count theorem TauCeti.exists_card_aroots_eq implies that every counted extension contains a root of one of the approximants. That root generates the extension, since its degree is n. Each approximant has only finitely many roots in the separable closure, so these generated fields form a countable cover. In particular, the argument does not use the mass formula or its convergence.

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, §§2–3.

theorem TauCeti.countable_totallyRamifiedOfDegree {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) : (totallyRamifiedOfDegree K n).Countable

The totally ramified degree-n subextensions of a separable closure of a nonarchimedean local field form a countable set, also in equal characteristic.