The totally ramified quadratic extensions of ℚ_2

This file determines σ_{ℚ_2}(2) = totallyRamifiedOfDegree ℚ_[2] 2 explicitly, together with the wild exponent of each member, independently of Serre's mass formula:

σ_{ℚ_2}(2) = {ℚ_2(√-1), ℚ_2(√-5), ℚ_2(√2), ℚ_2(√-2), ℚ_2(√10), ℚ_2(√-10)}.

These six fields are distinct. The first two have discriminant exponent 2, hence wild exponent c = 1, and the other four have discriminant exponent 3, hence c = 2, so Serre's mass formula reads 2 · 2⁻¹ + 4 · 2⁻² = 2. This is the smallest wildly ramified instance of the mass formula, and it distinguishes c(L) = d(L) - n + 1 from its neighbours d(L) - n and d(L) - n + 2, which give the sums 4 and 1.

The proof runs through the eight square classes 1, -1, 5, -5, 2, -2, 10, -10 of ℚ_2 (TauCeti.squareClass_padicTwoSquareClassRep_bijective). A quadratic subextension is ℚ_2(√a) for some a ∈ ℚ_2ˣ, and it depends only on the square class of a. The class 1 gives ℚ_2 itself. The class 5 is also the class of -3, since -15 is 1 modulo 8, and ℚ_2(√-3) is generated by a primitive cube root of unity, so it is unramified (TauCeti.mem_maximalUnramifiedExtension_of_sq_eq_neg_three). The classes 2u, for u a unit, give the fields ℚ_2(√c) for the uniformizers c = 2u, and the classes -1 and -5 give the fields ℚ_2(√(1 - c)) for the uniformizers c = 2 and c = 6. Their membership in σ_{ℚ_2}(2) and their discriminant exponents 2 v(2) + 1 = 3 and 2 v(2) = 2 are the specializations to ℚ_2 of TauCeti.natCast_discriminantExponent_adjoin_of_sq_eq_of_irreducible, TauCeti.adjoin_mem_totallyRamifiedOfDegree_two_of_sq_eq_one_sub and TauCeti.natCast_discriminantExponent_adjoin_of_sq_eq_one_sub_of_irreducible.

Main results

• TauCeti.totallyRamifiedOfDegree_two_eq_padicTwo: the six fields above are σ_{ℚ_2}(2).
• TauCeti.encard_totallyRamifiedOfDegree_two_padicTwo: σ_{ℚ_2}(2) has exactly six elements.
• TauCeti.tsum_one_div_pow_wildExponent_two_padicTwo: Serre's mass formula ∑_{L ∈ σ_{ℚ_2}(2)} 2 ^ (-c(L)) = 2.

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 ℚ_2.

Uniformizers of ℚ_2

The two families of ramified quadratic extensions

The six totally ramified quadratic extensions

theorem TauCeti.totallyRamifiedOfDegree_two_eq_padicTwo {x₁ x₂ x₃ x₄ x₅ x₆ : SeparableClosure ℚ_[2]} (h₁ : x₁ ^ 2 = -1) (h₂ : x₂ ^ 2 = -5) (h₃ : x₃ ^ 2 = 2) (h₄ : x₄ ^ 2 = -2) (h₅ : x₅ ^ 2 = 10) (h₆ : x₆ ^ 2 = -10) : totallyRamifiedOfDegree ℚ_[2] 2 = {ℚ_[2]⟮x₁⟯, ℚ_[2]⟮x₂⟯, ℚ_[2]⟮x₃⟯, ℚ_[2]⟮x₄⟯, ℚ_[2]⟮x₅⟯, ℚ_[2]⟮x₆⟯}

The totally ramified quadratic extensions of ℚ_2. If x₁, …, x₆ are square roots of -1, -5, 2, -2, 10, -10 in the separable closure of ℚ_2, then σ_{ℚ_2}(2) = {ℚ_2(x₁), ℚ_2(x₂), ℚ_2(x₃), ℚ_2(x₄), ℚ_2(x₅), ℚ_2(x₆)}.

theorem TauCeti.encard_totallyRamifiedOfDegree_two_padicTwo : (totallyRamifiedOfDegree ℚ_[2] 2).encard = 6

σ_{ℚ_2}(2) has exactly six elements.

theorem TauCeti.tsum_one_div_pow_wildExponent_two_padicTwo : ∑' (L : ↑(totallyRamifiedOfDegree ℚ_[2] 2)), 1 / 2 ^ (↑L).wildExponent = 2

Serre's mass formula for the quadratic extensions of ℚ_2: ∑_{L ∈ σ_{ℚ_2}(2)} 2 ^ (-c(L)) = 2 · 2⁻¹ + 4 · 2⁻² = 2.