The cohomological dimension of a Demushkin group

Tate's theorem: an infinite Demushkin group has cd_p G = 2 (Serre's exposé, §9.1). The lower bound holds for every Demushkin group: H²(G, 𝔽_p) is one-dimensional, so H²(G, 𝔽_p) ≠ 0 and Hⁿ(G, 𝔽_p) ≠ 0 → n ≤ cd_p G (TauCeti.le_cohomologicalDimensionAt_of_nontrivial_cohomFp) gives 2 ≤ cd_p G. The upper bound is the right exactness of H² on the finite 𝔽_p[G]-modules, which follows from Tate's perfect duality on those modules (TauCeti.IsDemushkin.dualityMap2_bijective) through TauCeti.IsProP.cohomologicalDimensionAt_le_two_of_forall_dualityMap2_bijective.

The hypothesis "infinite" is needed for the upper bound and not for the lower one: the finite Demushkin group ℤ/2 has cd_2 (ℤ/2) = ⊤.

Main results

• TauCeti.IsDemushkin.two_le_cohomologicalDimensionAt: a Demushkin group has 2 ≤ cd_p G.
• TauCeti.IsDemushkin.cohomologicalDimensionAt_eq_two: an infinite Demushkin group has cd_p G = 2.

References

• J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 8 (1962/63), exposé 252, §9.1.

theorem TauCeti.IsDemushkin.two_le_cohomologicalDimensionAt {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsDemushkin p G) : 2 ≤ cohomologicalDimensionAt p G

A Demushkin group has p-cohomological dimension at least 2: its H²(G, 𝔽_p) is one-dimensional, hence nonzero.

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

Tate's theorem: an infinite Demushkin group has p-cohomological dimension exactly 2. The lower bound is H²(G, 𝔽_p) ≠ 0; the upper bound is the right exactness of H² on the finite 𝔽_p[G]-modules, which Tate's perfect duality provides.