Cohomology of finite cyclic groups with topological coefficients

First cohomology

For a cyclic group generated by g, a continuous one-cocycle is a coboundary exactly when its value at g has the form g • m - m. On a finite group this value is killed by the group norm TauCeti.groupNorm G M. Consequently H¹ vanishes if every element killed by the norm has the form g • m - m.

The coefficients need not be discrete. In particular, the criterion applies to a finite discrete quotient acting on a profinite abelian group, where the comparison with discrete group cohomology over Rep ℤ G does not cover coefficients and groups in arbitrary universes.

The sufficient condition is not unconditional: for a nontrivial finite cyclic group acting trivially on a cyclic group of the same order, the norm is zero and H¹ is nonzero.

Second cohomology

For a finite cyclic group G = ⟨g⟩ acting on an additive group M, second continuous cohomology is the quotient of the invariant subgroup by the image of the group norm:

H²(G, M) ≃ Mᴳ / N(M),       N(m) = ∑ x : G, x • m.

The isomorphism sends the class of a two-cocycle f to the class of ∑ x : G, f (x, g). The coefficient group may have an arbitrary topology: discreteness of the finite group makes every cochain continuous. This avoids the universe restriction in the comparison with Mathlib's bundled Rep ℤ G computation.

The proof uses the classical carry cocycle for surjectivity. For injectivity it constructs a primitive recursively around the cycle generated by g; the condition that its values close up is exactly that the displayed sum is a norm.

Main results

• TauCeti.ContCohomology.H1pi_eq_zero_iff_exists_smul_sub_eq: a cyclic one-cocycle class vanishes exactly when its value at the generator is a (g - 1)-image.
• TauCeti.ContCohomology.subsingleton_H1_of_forall_mem_zpowers: the vanishing criterion for finite cyclic H¹.
• TauCeti.ContCohomology.explicitH2CyclicEquiv: the cyclic H² computation.
• TauCeti.ContCohomology.explicitH2CyclicEquiv_mk: its formula on cocycle classes.

References

• J.-P. Serre, Local Fields, Springer GTM 67 (1979), Chapter VIII, §4, the cyclic-group descriptions H¹ = ker(N) / (g - 1)M and H² = Mᴳ / N(M).
• K. S. Brown, Cohomology of Groups, Springer GTM 87 (1982), Chapter VI, §2.
• Mathlib's Rep.FiniteCyclicGroup.groupCohomologyIsoOdd is the periodic-resolution version of the H¹ computation for linear representations. Here the criterion is proved directly on continuous cocycles.
• The carry cocycle used for surjectivity in degree two adapts Tau Ceti's Rep.FiniteCyclicGroup.carryCocycle from TauCeti.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic, the analogous construction for linear representations, to continuous cochains.

theorem TauCeti.ContCohomology.H1pi_eq_zero_iff_exists_smul_sub_eq {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (f : ↥(Z1 G M)) : ↑f = 0 ↔ ∃ (m : M), g • m - m = ↑f g

A continuous one-cocycle on a cyclic group represents zero exactly when its value at the chosen generator is a (g - 1)-image. This characterization also holds for infinite cyclic groups and for nondiscrete coefficients.

theorem TauCeti.ContCohomology.subsingleton_H1_of_forall_mem_zpowers {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) [Fintype G] (h : ∀ (m : M), (groupNorm G M) m = 0 → ∃ (b : M), g • b - b = m) : Subsingleton (H1 G M)

A finite cyclic group has vanishing first continuous cohomology if the kernel of the group norm consists of (g - 1)-images. No discreteness assumption on the coefficient group is required.

noncomputable def TauCeti.ContCohomology.explicitH2CyclicEquiv (G' : Type u) [Group G'] [TopologicalSpace G'] [DiscreteTopology G'] [Fintype G'] (M' : Type v) [AddCommGroup M'] [TopologicalSpace M'] [IsTopologicalAddGroup M'] [DistribMulAction G' M'] [ContinuousSMul G' M'] (g' : G') (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') : H2 G' M' ≃+ ↥(H0 G' M') ⧸ (groupNorm G' M').range.addSubgroupOf (H0 G' M')

For a finite cyclic group generated by g, second continuous cohomology is the quotient of the invariant subgroup by the image of the group norm. The coefficient topology is arbitrary.

@[simp]

theorem TauCeti.ContCohomology.explicitH2CyclicEquiv_mk (G' : Type u) [Group G'] [TopologicalSpace G'] [DiscreteTopology G'] [Fintype G'] (M' : Type v) [AddCommGroup M'] [TopologicalSpace M'] [IsTopologicalAddGroup M'] [DistribMulAction G' M'] [ContinuousSMul G' M'] (g' : G') (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (f : ↥(Z2 G' M')) : (explicitH2CyclicEquiv G' M' g' hg') ↑f = ↑⟨∑ x : G', ↑f (x, g'), ⋯⟩

The cyclic H² equivalence sends a cocycle class to the class of the sum of its values f (x, g) over the first variable.