H¹(G, 𝔽_p) of a pro-p group and its generator rank

For a profinite pro-p group G, the dimension of H¹(G, 𝔽_p) over 𝔽_p is the topological generator rank of G: the cohomology cohomFp p G 1 is the continuous 𝔽_p-dual of G (TauCeti.cohomFpLinearEquivContinuousZModDual), whose dimension Burnside's basis theorem reads as the rank (TauCeti.IsProP.topologicalGeneratorRank_eq_rank_continuousZModDual). The identity is stated first for cardinals, with no finiteness hypothesis, and then for the natural-number rank of a topologically finitely generated group; in between, H¹(G, 𝔽_p) is finite-dimensional exactly when G is topologically finitely generated. These are the statements through which a finite-dimensionality hypothesis on H¹(G, 𝔽_p), such as the one in the definition of a Demushkin group, is converted into finite generation and a rank.

Main results

• TauCeti.IsProP.rank_cohomFp_one: dim_{𝔽_p} H¹(G, 𝔽_p) = d(G) as cardinals.
• TauCeti.IsProP.finite_cohomFp_one_iff: H¹(G, 𝔽_p) is finite-dimensional exactly when G is topologically finitely generated.
• TauCeti.IsProP.finrank_cohomFp_one: dim_{𝔽_p} H¹(G, 𝔽_p) = d(G) for a topologically finitely generated pro-p group.

References

• J.-P. Serre, Galois Cohomology, I §4.2.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, (3.9.1).

theorem TauCeti.IsProP.rank_cohomFp_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : Module.rank (ZMod p) ↑(cohomFp p G 1).toModuleCat = topologicalGeneratorRank G

The dimension of H¹(G, 𝔽_p) is the topological generator rank, for a profinite pro-p group G, as an identity of cardinals with no finiteness hypothesis.

theorem TauCeti.IsProP.finite_cohomFp_one_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) : Module.Finite (ZMod p) ↑(cohomFp p G 1).toModuleCat ↔ IsTopologicallyFinitelyGenerated G

H¹(G, 𝔽_p) is finite-dimensional exactly when G is topologically finitely generated, for a profinite pro-p group G.

theorem TauCeti.IsProP.finrank_cohomFp_one {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) : Module.finrank (ZMod p) ↑(cohomFp p G 1).toModuleCat = topologicalGeneratorRankNat G hfg

The dimension of H¹(G, 𝔽_p) is the topological generator rank, for a topologically finitely generated profinite pro-p group G.