The standard dyadic Demushkin presentation D₀ = ⟨A, S, Y ∣ A²S⁴(S,Y)⟩

This file defines the pro-2 group D₀, presented on three generators A, S, Y by the single relator A²S⁴(S,Y), where (x, y) = x⁻¹y⁻¹xy is Labute's commutator convention. In Labute's classification of Demushkin groups with q = 2 and odd rank, D₀ is the normal form of rank 3 with f = 2; it is the abstract group that the local theory identifies with the maximal pro-2 quotient of the absolute Galois group of ℚ₂. The name D₀, the marked generators A, S, Y and the relator A²S⁴[S,Y] follow Roe–Turturean, §3.1, equation (3.1), whose commutator convention is the same. Neither that identification nor the Demushkin property itself is established here.

What is established is that the presentation is not vacuous. The map on the free pro-2 group sending A ↦ 0, S ↦ 1, Y ↦ 0 in ℤ/2 kills the relator, because the commutator dies in an abelian group and 2 · 0 + 4 · 1 = 0, so it descends to a continuous surjection D₀ ↠ ℤ/2. Hence D₀ is nontrivial: the marked generator S is not the identity. The marked generators topologically generate D₀, so D₀ is topologically finitely generated, and a continuous homomorphism out of D₀ is determined by its values on A, S and Y.

The presentation is moreover minimal: the relator is a product of two squares and a commutator, so it lies in the Frattini subgroup of the free pro-2 group on three generators, and therefore D₀ has topological generator rank exactly 3. This is the rank n = 3 of the Demushkin invariants of D₀: the relator is the q = 2, odd-rank normal-form word TauCeti.demushkinWordTwoOdd with n = 3 and f = 2.

Main definitions

• TauCeti.d0Relator: the relator A²S⁴(S,Y) in the free pro-2 group on Fin 3.
• TauCeti.demushkinD0: the presented pro-2 group D₀.
• TauCeti.d0A, TauCeti.d0S, TauCeti.d0Y: its marked generators.
• TauCeti.d0Lift: the continuous homomorphism D₀ → P determined by three elements of a pro-2 group P satisfying the relation a²s⁴(s,y) = 1.
• TauCeti.d0FreeCharacter: the character A ↦ 0, S ↦ 1, Y ↦ 0 of the free pro-2 group.
• TauCeti.d0Character: the induced character D₀ → ℤ/2.

Main results

• TauCeti.d0Relator_eq_demushkinWordTwoOdd: the relator is the odd-rank normal-form word at n = 3, f = 2.
• TauCeti.d0_relation: the marked generators satisfy A²S⁴(S,Y) = 1.
• TauCeti.d0_hom_ext: a continuous homomorphism out of D₀ is determined by its values on A, S and Y.
• TauCeti.d0FreeCharacter_d0Relator: the character kills the relator.
• TauCeti.d0Character_surjective: the induced character D₀ → ℤ/2 is surjective.
• TauCeti.d0S_ne_one and the Nontrivial demushkinD0 instance: D₀ is nontrivial.
• TauCeti.d0_topologicallyGenerates: A, S, Y topologically generate D₀.
• TauCeti.isTopologicallyFinitelyGenerated_demushkinD0: D₀ is topologically finitely generated.
• TauCeti.d0Relator_mem_proPFrattini: the relator lies in the Frattini subgroup of the free pro-2 group, so the presentation of D₀ is minimal.
• TauCeti.topologicalGeneratorRankNat_demushkinD0: D₀ has topological generator rank 3.

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 III, §9.
• D. Roe, D. Turturean, A Presentation of the Absolute Galois Group of ℚ₂, preprint (2026), §3.1, https://roed314.github.io/gq2/.
• J.-P. Serre, Galois Cohomology, Chapter I, §4.5.

noncomputable def TauCeti.d0Relator : freeProP 2 (Fin 3)

The dyadic Demushkin relator A²S⁴(S,Y) in the free pro-2 group on the three generators A = of 0, S = of 1, Y = of 2, written in Labute's commutator convention (x, y) = x⁻¹y⁻¹xy.

theorem TauCeti.d0Relator_def : d0Relator = freeProP.of 0 ^ 2 * freeProP.of 1 ^ 4 * ((freeProP.of 1)⁻¹ * (freeProP.of 2)⁻¹ * freeProP.of 1 * freeProP.of 2)

The relator A²S⁴(S,Y), written out on the free generators.

theorem TauCeti.d0Relator_eq_demushkinWordTwoOdd : d0Relator = demushkinWordTwoOdd 2 3 (freeProPGen 2 3)

The relator A²S⁴(S,Y) is the q = 2, n odd normal-form word with n = 3 and f = 2, read on the free generators.

@[reducible, inline]

noncomputable abbrev TauCeti.demushkinD0 : Type

D₀ = ⟨A, S, Y ∣ A²S⁴(S,Y)⟩, the standard dyadic one-relator pro-2 group, presented on three generators by the single relator d0Relator.

instance TauCeti.isClosed_d0_definingSubgroup : IsClosed ↑(Subgroup.normalClosure {d0Relator}).topologicalClosure

Closedness of the defining normal subgroup, for the quotient topology instances.

noncomputable def TauCeti.d0A : demushkinD0

The marked generator A of D₀, the image of the first free pro-2 generator.

noncomputable def TauCeti.d0S : demushkinD0

The marked generator S of D₀, the image of the second free pro-2 generator.

noncomputable def TauCeti.d0Y : demushkinD0

The marked generator Y of D₀, the image of the third free pro-2 generator.

@[simp]

theorem TauCeti.presentedProP_of_d0Relator_zero : presentedProP.of 2 {d0Relator} 0 = d0A

The first canonical generator of the presented group D₀ is A.

@[simp]

theorem TauCeti.presentedProP_of_d0Relator_one : presentedProP.of 2 {d0Relator} 1 = d0S

The second canonical generator of the presented group D₀ is S.

@[simp]

theorem TauCeti.presentedProP_of_d0Relator_two : presentedProP.of 2 {d0Relator} 2 = d0Y

The third canonical generator of the presented group D₀ is Y.

theorem TauCeti.range_presentedProP_of_d0Relator : Set.range (presentedProP.of 2 {d0Relator}) = {d0A, d0S, d0Y}

The set of canonical generators of D₀ is {A, S, Y}.

@[simp]

theorem TauCeti.d0_relation : d0A ^ 2 * d0S ^ 4 * (d0S⁻¹ * d0Y⁻¹ * d0S * d0Y) = 1

The marked generators of D₀ satisfy the defining relation A²S⁴(S,Y) = 1.

noncomputable def TauCeti.d0Lift {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (a s y : P) (h : a ^ 2 * s ^ 4 * (s⁻¹ * y⁻¹ * s * y) = 1) : demushkinD0 →ₜ* P

The universal property of D₀: three elements a, s, y of a pro-2 group P satisfying a²s⁴(s,y) = 1 determine a continuous homomorphism D₀ → P with A ↦ a, S ↦ s, Y ↦ y.

@[simp]

theorem TauCeti.d0Lift_d0A {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (a s y : P) (h : a ^ 2 * s ^ 4 * (s⁻¹ * y⁻¹ * s * y) = 1) : (d0Lift hP a s y h) d0A = a

d0Lift sends A to a.

@[simp]

theorem TauCeti.d0Lift_d0S {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (a s y : P) (h : a ^ 2 * s ^ 4 * (s⁻¹ * y⁻¹ * s * y) = 1) : (d0Lift hP a s y h) d0S = s

d0Lift sends S to s.

@[simp]

theorem TauCeti.d0Lift_d0Y {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (a s y : P) (h : a ^ 2 * s ^ 4 * (s⁻¹ * y⁻¹ * s * y) = 1) : (d0Lift hP a s y h) d0Y = y

d0Lift sends Y to y.

theorem TauCeti.d0_hom_ext {Q : Type u_1} [Group Q] [TopologicalSpace Q] [T2Space Q] {φ ψ : demushkinD0 →ₜ* Q} (hA : φ d0A = ψ d0A) (hS : φ d0S = ψ d0S) (hY : φ d0Y = ψ d0Y) : φ = ψ

Two continuous homomorphisms out of D₀ into a Hausdorff group that agree on the marked generators A, S, Y are equal.

theorem TauCeti.d0_hom_ext_iff {Q : Type u_1} [Group Q] [TopologicalSpace Q] [T2Space Q] {φ ψ : demushkinD0 →ₜ* Q} : φ = ψ ↔ φ d0A = ψ d0A ∧ φ d0S = ψ d0S ∧ φ d0Y = ψ d0Y

noncomputable def TauCeti.d0FreeCharacter : freeProP 2 (Fin 3) →ₜ* Multiplicative (ZMod 2)

The character of the free pro-2 group on A, S, Y with values A ↦ 0, S ↦ 1, Y ↦ 0 in ℤ/2, written multiplicatively. It is the map that exhibits D₀ as nontrivial.

@[simp]

theorem TauCeti.d0FreeCharacter_of (i : Fin 3) : d0FreeCharacter (freeProP.of i) = ![1, Multiplicative.ofAdd 1, 1] i

The values of d0FreeCharacter on the free generators.

@[simp]

theorem TauCeti.d0FreeCharacter_d0Relator : d0FreeCharacter d0Relator = 1

d0FreeCharacter kills the relator A²S⁴(S,Y): the commutator dies in the abelian group ℤ/2, and 2 · 0 + 4 · 1 = 0.

theorem TauCeti.d0FreeCharacter_surjective : Function.Surjective ⇑d0FreeCharacter

d0FreeCharacter is surjective, because S already hits the generator of ℤ/2.

noncomputable def TauCeti.d0Character : demushkinD0 →ₜ* Multiplicative (ZMod 2)

The character D₀ → ℤ/2 with values A ↦ 0, S ↦ 1, Y ↦ 0, induced by d0FreeCharacter.

@[simp]

theorem TauCeti.d0Character_comp_mk : d0Character.comp (presentedProP.mk 2 {d0Relator}) = d0FreeCharacter

d0Character is the descent of d0FreeCharacter along the presentation map.

@[simp]

theorem TauCeti.d0Character_mk (x : freeProP 2 (Fin 3)) : d0Character ((presentedProP.mk 2 {d0Relator}) x) = d0FreeCharacter x

d0Character agrees with d0FreeCharacter on the image of the free pro-2 group.

@[simp]

theorem TauCeti.d0Character_d0A : d0Character d0A = 1

d0Character vanishes on A.

@[simp]

theorem TauCeti.d0Character_d0S : d0Character d0S = Multiplicative.ofAdd 1

d0Character takes S to the generator of ℤ/2.

@[simp]

theorem TauCeti.d0Character_d0Y : d0Character d0Y = 1

d0Character vanishes on Y.

theorem TauCeti.d0Character_surjective : Function.Surjective ⇑d0Character

The induced character D₀ ↠ ℤ/2 is surjective.

theorem TauCeti.d0S_ne_one : d0S ≠ 1

The marked generator S of D₀ is not the identity: it maps to the generator of ℤ/2.

instance TauCeti.instNontrivialDemushkinD0 : Nontrivial demushkinD0

D₀ is nontrivial: the presentation ⟨A, S, Y ∣ A²S⁴(S,Y)⟩ does not collapse.

theorem TauCeti.isProP_demushkinD0 : IsProP 2 demushkinD0

D₀ is a pro-2 group.

theorem TauCeti.d0_topologicallyGenerates : (Subgroup.closure {d0A, d0S, d0Y}).topologicalClosure = ⊤

The marked generators A, S, Y topologically generate D₀.

theorem TauCeti.isTopologicallyFinitelyGenerated_demushkinD0 : IsTopologicallyFinitelyGenerated demushkinD0

D₀ is topologically finitely generated, by its three marked generators.

theorem TauCeti.d0Relator_mem_proPFrattini : d0Relator ∈ proPFrattini 2 (freeProP 2 (Fin 3))

The relator A²S⁴(S,Y) lies in the Frattini subgroup of the free pro-2 group on three generators, being the q = 2, n odd normal-form word with f = 2 ≥ 1.

@[simp]

theorem TauCeti.topologicalGeneratorRankNat_demushkinD0 : topologicalGeneratorRankNat demushkinD0 isTopologicallyFinitelyGenerated_demushkinD0 = 3

D₀ has topological generator rank 3: its presentation on A, S, Y is minimal, because the relator lies in the Frattini subgroup of the free pro-2 group.