ℤ/2 is the unique finite Demushkin group

A Demushkin group G of rank n has topological abelianization G^{ab} ≅ ℤ_p^{n-1} × ℤ_p ⧸ (q) (TauCeti.IsDemushkin.nonempty_continuousMulEquiv_topologicalAbelianization). If G^{ab} is finite, the free factor ℤ_p^{n-1} is finite, so n = 1, and a Demushkin group of rank one is ℤ/2 (TauCeti.IsDemushkin.demushkinRank_eq_one_iff). Hence a Demushkin group is finite exactly when it is ℤ/2, exactly when its rank is one, and exactly when its abelianization is finite; every Demushkin group at an odd prime, and every Demushkin group of rank at least two, is infinite. For the finite one the invariants are n = 1 and q = 2, the values Labute lists for ℤ/2.

Finiteness is the hypothesis that separates ℤ/2 from the Demushkin groups of the classification: the rank formula n(U) - 2 = [G : U] (n(G) - 2) for open subgroups and the equality cd_p G = 2 hold for infinite Demushkin groups only, and the results here let those statements be read with the hypothesis 2 ≤ demushkinRank in place of Infinite G.

Main results

• TauCeti.IsDemushkin.demushkinRank_eq_one_of_finite_topologicalAbelianization: a Demushkin group with finite abelianization has rank one.
• TauCeti.IsDemushkin.finite_iff_demushkinRank_eq_one, TauCeti.IsDemushkin.finite_topologicalAbelianization_iff: a Demushkin group is finite exactly when its rank is one, exactly when its abelianization is finite.
• TauCeti.IsDemushkin.finite_iff_nonempty_continuousMulEquiv_multiplicative_zmod_two: ℤ/2 is the unique finite Demushkin group.
• TauCeti.IsDemushkin.infinite_iff_two_le_demushkinRank: a Demushkin group is infinite exactly when its rank is at least two.
• TauCeti.IsDemushkin.eq_two_of_finite, TauCeti.IsDemushkin.infinite_of_ne_two: a finite Demushkin group lives at p = 2; at an odd prime every Demushkin group is infinite.
• TauCeti.IsDemushkin.natCard_eq_two_of_finite, TauCeti.IsDemushkin.demushkinQ_eq_two_of_finite: a finite Demushkin group has two elements and q-invariant 2; TauCeti.demushkinQ_multiplicative_zmod_two records q(ℤ/2) = 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.demushkinRank_eq_one_of_finite_topologicalAbelianization {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) [Finite (TopologicalAbelianization G)] : demushkinRank hG = 1

A Demushkin group with finite abelianization has rank one: in G^{ab} ≅ ℤ_p^{n-1} × ℤ_p ⧸ (q) the free factor ℤ_p^{n-1} is finite only for n = 1.

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

A finite Demushkin group has rank one.

theorem TauCeti.IsDemushkin.finite_iff_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) : Finite G ↔ demushkinRank hG = 1

A Demushkin group is finite exactly when its rank is one.

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

ℤ/2 is the unique finite Demushkin group: a Demushkin group is finite exactly when it is topologically isomorphic to ℤ/2.

theorem TauCeti.IsDemushkin.finite_topologicalAbelianization_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) : Finite (TopologicalAbelianization G) ↔ Finite G

A Demushkin group is finite exactly when its abelianization is finite.

theorem TauCeti.IsDemushkin.infinite_iff_two_le_demushkinRank {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) : Infinite G ↔ 2 ≤ demushkinRank hG

A Demushkin group is infinite exactly when its rank is at least two.

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

A Demushkin group of rank at least two is infinite.

theorem TauCeti.IsDemushkin.infinite_of_one_lt_topologicalGeneratorRankNat {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) {hfg : IsTopologicallyFinitelyGenerated G} (h : 1 < topologicalGeneratorRankNat G hfg) : Infinite G

A Demushkin group whose topological generator rank exceeds one is infinite.

theorem TauCeti.IsDemushkin.two_le_demushkinRank_of_infinite {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) [Infinite G] : 2 ≤ demushkinRank hG

An infinite Demushkin group has rank at least two.

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

A finite Demushkin group lives at p = 2.

theorem TauCeti.IsDemushkin.infinite_of_ne_two {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (hp : p ≠ 2) : Infinite G

At an odd prime every Demushkin group is infinite.

theorem TauCeti.IsDemushkin.natCard_eq_two_of_finite {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) [Finite G] : Nat.card G = 2

A finite Demushkin group has two elements.

theorem TauCeti.IsDemushkin.natCard_topologicalAbelianization_eq_two_of_finite {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) [Finite G] : Nat.card (TopologicalAbelianization G) = 2

The abelianization of a finite Demushkin group has two elements: it is a quotient of G, which has two elements, and it maps onto ℤ/2.

theorem TauCeti.IsDemushkin.demushkinQ_eq_two_of_finite {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) [Finite G] : demushkinQ hG = 2

A finite Demushkin group has q-invariant 2: its abelianization is the torsion group ℤ/2.

@[simp]

theorem TauCeti.demushkinQ_multiplicative_zmod_two {isDemushkin_multiplicative_zmod_two : IsDemushkin 2 (Multiplicative (ZMod 2))} : demushkinQ isDemushkin_multiplicative_zmod_two = 2

q(ℤ/2) = 2: the q-invariant of the finite Demushkin group ℤ/2.