Finiteness of H¹ over a topologically finitely generated group

A continuous 1-cocycle into a T1 module is determined by its values on a topological generating set (TauCeti.ContCohomology.eq_of_mem_Z1_of_eqOn_of_topologicalClosure_closure_eq_top). Over a topologically finitely generated group, restriction to a finite topological generating set is therefore an injection of the continuous 1-cocycles with values in a finite discrete module into a finite set, so the cocycles form a finite group, and so does H¹(G, M).

Main results

• TauCeti.IsTopologicallyFinitelyGenerated.finite_Z1 and TauCeti.IsTopologicallyFinitelyGenerated.finite_H1: over a topologically finitely generated group, Z¹(G, M) and H¹(G, M) are finite for every finite discrete G-module M.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_Z1 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (hG : IsTopologicallyFinitelyGenerated G) [Finite M] : Finite ↥(ContCohomology.Z1 G M)

Finiteness of the continuous 1-cocycles. Over a topologically finitely generated group, the continuous 1-cocycles with values in a finite discrete module form a finite group: restriction to a finite topological generating set is injective.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_H1 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (hG : IsTopologicallyFinitelyGenerated G) [ContinuousSMul G M] [Finite M] : Finite (ContCohomology.H1 G M)

Finiteness of H¹. Over a topologically finitely generated group, H¹(G, M) is finite for every finite discrete G-module M.