The pro-2 Galois group of ℚ₂

The absolute Galois group of ℚ₂ has maximal pro-2 quotient isomorphic to the standard dyadic Demushkin group D₀.

The field ℚ₂ contains exactly two 2-power roots of unity, ±1, and has degree N = 1 over itself, so it lies in the odd dyadic case and G_{ℚ₂}(2) is a Demushkin group of rank N + 2 = 3. This module identifies G_{ℚ₂}(2) with D₀, both as an unmarked group and with the standard orientation of D₀ corresponding to the cyclotomic orientation of G_{ℚ₂}(2).

Main results

• TauCeti.localRootOfUnityOrder_two_ratPadic: q(ℚ₂) = 2.
• TauCeti.isDyadicOddCase_ratPadic: ℚ₂ lies in the odd dyadic case.
• TauCeti.demushkinRank_absoluteGaloisGroupProP_two_ratPadic: G_{ℚ₂}(2) has rank 3.
• TauCeti.absoluteGaloisGroupProP_two_ratPadic_marked: the marked identification G_{ℚ₂}(2) ≃ D₀, carrying the standard orientation to the cyclotomic orientation, which is surjective.
• TauCeti.absoluteGaloisGroupProP_two_ratPadic: G_{ℚ₂}(2) ≃ D₀, its unmarked corollary.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter VII, §5.
• D. Roe, D. Turturean, A Presentation of the Absolute Galois Group of ℚ₂, manuscript (2026), §3.1, https://roed314.github.io/gq2/.

theorem TauCeti.ratPadicTwo_hasPrimitiveRoot : ∃ (ζ : ℚ_[2]), IsPrimitiveRoot ζ 2

ℚ₂ contains the primitive square root of unity -1.

theorem TauCeti.not_exists_isPrimitiveRoot_four_ratPadic : ¬∃ (ζ : ℚ_[2]), IsPrimitiveRoot ζ 4

ℚ₂ contains no primitive fourth root of unity, since its cyclotomic character is surjective while a primitive fourth root would force its image into 1 + 4ℤ₂.

theorem TauCeti.localRootOfUnityOrder_two_ratPadic : localRootOfUnityOrder 2 ℚ_[2] ⋯ = 2

The group of 2-power roots of unity in ℚ₂ has order two.

theorem TauCeti.isDyadicOddCase_ratPadic : IsDyadicOddCase ℚ_[2]

ℚ₂ is in the odd-degree dyadic case: its root-of-unity order is two and its degree is one.

@[simp]

theorem TauCeti.demushkinRank_absoluteGaloisGroupProP_two_ratPadic (hG : IsDemushkin 2 (absoluteGaloisGroupProP 2 ℚ_[2])) : demushkinRank hG = 3

G_{ℚ₂}(2) has Demushkin rank 3: for any witness hG that G_{ℚ₂}(2) is a Demushkin group, the associated rank demushkinRank hG is 3, the rank N + 2 at N = 1.

theorem TauCeti.absoluteGaloisGroupProP_two_ratPadic_marked : ∃ (e : absoluteGaloisGroupProP 2 ℚ_[2] ≃ₜ* demushkinD0), standardD0Orientation.comp ↑e = cyclotomicOrientation 2 ℚ_[2] ratPadicTwo_hasPrimitiveRoot ∧ Function.Surjective ⇑(cyclotomicOrientation 2 ℚ_[2] ratPadicTwo_hasPrimitiveRoot)

The marked presentation of G_{ℚ₂}(2). There is an isomorphism e : G_{ℚ₂}(2) ≃ D₀ = ⟨A, S, Y ∣ A²S⁴(S,Y)⟩ along which the standard orientation of D₀ pulls back to the cyclotomic orientation of G_{ℚ₂}(2), and the cyclotomic orientation is surjective.

theorem TauCeti.absoluteGaloisGroupProP_two_ratPadic : Nonempty (absoluteGaloisGroupProP 2 ℚ_[2] ≃ₜ* demushkinD0)

The maximal pro-2 quotient of G_{ℚ₂} is D₀.