ℤ/2 is the unique Demushkin group of rank one

A Demushkin group of rank one is procyclic: it is topologically generated by a single element a. If a has infinite order the group is ℤ_p, the free pro-p group on one generator, whose H²(-, 𝔽_p) vanishes, so it is not Demushkin. Otherwise the group is a finite cyclic p-group ℤ/pᵏ. The rank is odd, so p = 2 by the parity constraint. For k ≥ 2 the mod-2 character of ℤ/2ᵏ lifts to ℤ/4, so its cup square vanishes (ContinuousMonoidHom.cupFp_zmodFourReductionClass_self_eq_zero); but in a Demushkin group of rank one H¹(G, 𝔽_p) is a line, so nondegeneracy of the cup pairing forces the cup square of every nonzero class to be nonzero. Hence k = 1, and the group is ℤ/2, which is Demushkin (TauCeti.isDemushkin_multiplicative_zmod_two).

Along the way, a group topologically isomorphic to ℤ/n is shown not to be Demushkin at p = 2 whenever 4 ∣ n; this covers the cyclic groups ℤ/2ᵏ with k ≥ 2.

Main results

• TauCeti.IsDemushkin.cupFp_self_ne_zero_of_demushkinRank_eq_one: in a Demushkin group of rank one, every nonzero class of H¹(G, 𝔽_p) has nonzero cup square.
• TauCeti.not_isDemushkin_of_four_dvd_of_continuousMulEquiv_multiplicative_zmod: a group topologically isomorphic to ℤ/n is not Demushkin at p = 2 when 4 ∣ n.
• TauCeti.IsDemushkin.eq_two_of_demushkinRank_eq_one: a Demushkin group of rank one lives at p = 2.
• TauCeti.IsDemushkin.nonempty_continuousMulEquiv_multiplicative_zmod_two_of_demushkinRank_eq_one: a Demushkin group of rank one is topologically isomorphic to ℤ/2.
• TauCeti.IsDemushkin.demushkinRank_eq_one_iff: a Demushkin group has rank one exactly when it is topologically isomorphic to ℤ/2.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, p. 106 and Remark 2.
• J.-P. Serre, Galois Cohomology, Springer (1997), Chapter I, §4.5.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), (3.9.10).

theorem TauCeti.IsDemushkin.cupFp_self_ne_zero_of_demushkinRank_eq_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (h : demushkinRank hG = 1) {a : ↑(cohomFp p G 1).toModuleCat} (ha : a ≠ 0) : ((cupFp p G) a) a ≠ 0

In a Demushkin group of rank one, every nonzero class of H¹(G, 𝔽_p) has nonzero cup square: H¹(G, 𝔽_p) is a line, so the class pairing nontrivially with a nonzero a is a multiple of a.

theorem TauCeti.IsDemushkin.demushkinRank_ne_one_of_zmod_four_reduction_ne_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (φ : G →ₜ* Multiplicative (ZMod 4)) {g : G} (hg : (ZMod.castHom demushkinRank_ne_one_of_zmod_four_reduction_ne_zero._proof_1 (ZMod 2)) (Multiplicative.toAdd (φ g)) ≠ 0) : demushkinRank hG ≠ 1

A Demushkin group at p = 2 admitting a continuous character to ℤ/4 with an odd value does not have rank one: the reduction modulo 2 of the character is a nonzero class of H¹(G, 𝔽₂) with vanishing cup square.

theorem TauCeti.not_isDemushkin_of_four_dvd_of_continuousMulEquiv_multiplicative_zmod {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} [NeZero n] (hn : 4 ∣ n) (e : G ≃ₜ* Multiplicative (ZMod n)) : ¬IsDemushkin 2 G

A profinite group topologically isomorphic to ℤ/n with 4 ∣ n is not Demushkin at p = 2: it has rank one, and its mod-2 character lifts to ℤ/4.

theorem TauCeti.IsDemushkin.eq_two_of_demushkinRank_eq_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (h : demushkinRank hG = 1) : p = 2

A Demushkin group of rank one lives at p = 2: at an odd prime the rank is even.

theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_multiplicative_zmod_two_of_demushkinRank_eq_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (h : demushkinRank hG = 1) : Nonempty (G ≃ₜ* Multiplicative (ZMod 2))

ℤ/2 is the unique Demushkin group of rank one: a Demushkin group of rank one is topologically isomorphic to ℤ/2. It is procyclic; a generator of infinite order would make it free pro-p of rank one, whose H² vanishes; a generator of finite order makes it a finite cyclic group ℤ/2ᵏ, and for k ≥ 2 the mod-2 character lifts to ℤ/4, so its cup square vanishes, against the nondegeneracy of the cup pairing on the line H¹(G, 𝔽₂).

theorem TauCeti.IsDemushkin.demushkinRank_eq_one_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) : demushkinRank hG = 1 ↔ Nonempty (G ≃ₜ* Multiplicative (ZMod 2))

A Demushkin group has rank one exactly when it is topologically isomorphic to ℤ/2.