The totally ramified quadratic extensions in odd residue characteristic

Let K be a nonarchimedean local field whose residue characteristic is not 2. This file determines σ_K(2) = totallyRamifiedOfDegree K 2 explicitly, independently of Serre's mass formula: for a uniformizer ϖ of K and a unit u of 𝒪[K] that is not a square,

σ_K(2) = {K(√ϖ), K(√(u ϖ))},

and these two fields are distinct. Both have wild exponent 0, so the mass formula ∑_{L ∈ σ_K(2)} q ^ (-c(L)) = 2 holds in this case. This is the smallest instance of the tame count #σ_K(n) = n, and for K = ℚ_p with p odd it is the classical list ℚ_p(√p), ℚ_p(√(u p)).

The proof runs through the four square classes 1, u, ϖ, u ϖ of K. A quadratic subextension is K(√a) for some a ∈ Kˣ, and it depends only on the square class of a. The class 1 gives K itself. The class u gives a subfield of the maximal unramified extension, since square roots of units are unramified away from residue characteristic two, and an unramified member of σ_K(n) has n = 1. The classes ϖ and u ϖ give the two fields above, generated by roots of the Eisenstein polynomials X ^ 2 - ϖ and X ^ 2 - u ϖ.

Main results

• TauCeti.totallyRamifiedOfDegree_two_eq: σ_K(2) = {K(√ϖ), K(√(u ϖ))} in odd residue characteristic.
• TauCeti.adjoin_ne_adjoin_of_sq_eq_of_sq_eq_mul: the two fields are distinct whenever 2 ≠ 0 in K.
• TauCeti.encard_totallyRamifiedOfDegree_two: σ_K(2) has exactly two elements.
• TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_two: Serre's mass formula for n = 2 in odd residue characteristic.
• TauCeti.Padic.totallyRamifiedOfDegree_two_eq and TauCeti.Padic.tsum_one_div_pow_wildExponent_two: the same for ℚ_p with p odd, where σ_{ℚ_p}(2) = {ℚ_p(√p), ℚ_p(√(u p))}.

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.
• J.-P. Serre, A Course in Arithmetic, Chapter II, §3, for the square classes of ℚ_p.

theorem TauCeti.adjoin_ne_adjoin_of_sq_eq_of_sq_eq_mul {K : Type u_1} [Field K] [ValuativeRel K] [NeZero 2] {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : ϖ ≠ 0) (u : (↥(ValuativeRel.valuation K).integer)ˣ) (hu : ¬IsSquare ↑↑u) {x y : SeparableClosure K} (hx : x ^ 2 = (algebraMap K (SeparableClosure K)) ↑ϖ) (hy : y ^ 2 = (algebraMap K (SeparableClosure K)) ↑(↑u * ϖ)) : K⟮x⟯ ≠ K⟮y⟯

The two fields K(√ϖ) and K(√(u ϖ)) are distinct when 2 ≠ 0 in K, ϖ ≠ 0 and u is a unit of 𝒪[K] that is not a square: equality would make ϖ · u ϖ, hence u, a square.

theorem TauCeti.totallyRamifiedOfDegree_two_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ 2) {ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) (u : (↥(ValuativeRel.valuation K).integer)ˣ) (hu : ¬IsSquare ↑↑u) {x y : SeparableClosure K} (hx : x ^ 2 = (algebraMap K (SeparableClosure K)) ↑ϖ) (hy : y ^ 2 = (algebraMap K (SeparableClosure K)) ↑(↑u * ϖ)) : totallyRamifiedOfDegree K 2 = {K⟮x⟯, K⟮y⟯}

The totally ramified quadratic extensions in odd residue characteristic. Let ϖ be a uniformizer of K and u a unit of 𝒪[K] that is not a square, and let x and y be square roots of ϖ and u ϖ in the separable closure. If the residue characteristic of K is not 2, then σ_K(2) = {K(x), K(y)}.

theorem TauCeti.encard_totallyRamifiedOfDegree_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ 2) : (totallyRamifiedOfDegree K 2).encard = 2

σ_K(2) has exactly two elements when the residue characteristic of K is not 2.

theorem TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ 2) : ∑' (L : ↑(totallyRamifiedOfDegree K 2)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent = 2

Serre's mass formula for quadratic extensions in odd residue characteristic: ∑_{L ∈ σ_K(2)} q ^ (-c(L)) = 2, where q is the cardinality of the residue field of K. Both members of σ_K(2) are tamely ramified, with weight 1.

theorem TauCeti.Padic.totallyRamifiedOfDegree_two_eq {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) (u : (↥(ValuativeRel.valuation ℚ_[p]).integer)ˣ) (hu : ¬IsSquare ↑↑u) {x y : SeparableClosure ℚ_[p]} (hx : x ^ 2 = ↑p) (hy : y ^ 2 = (algebraMap ℚ_[p] (SeparableClosure ℚ_[p])) (↑↑u * ↑p)) : totallyRamifiedOfDegree ℚ_[p] 2 = {ℚ_[p]⟮x⟯, ℚ_[p]⟮y⟯}

The totally ramified quadratic extensions of ℚ_p for an odd prime p: if u is a unit of the ring of integers of ℚ_p that is not a square, and x and y are square roots of p and u p in the separable closure, then σ_{ℚ_p}(2) = {ℚ_p(x), ℚ_p(y)}.

theorem TauCeti.Padic.tsum_one_div_pow_wildExponent_two {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : ∑' (L : ↑(totallyRamifiedOfDegree ℚ_[p] 2)), 1 / ↑p ^ (↑L).wildExponent = 2

Serre's mass formula for quadratic extensions of ℚ_p for an odd prime p: ∑_{L ∈ σ_{ℚ_p}(2)} p ^ (-c(L)) = 2.