Continuous cohomology of a compact group is torsion in positive degrees

Let G be a compact group and X a topological representation of G whose underlying module is discrete. Every class of Hⁿ⁺¹(G, X) = continuousCohomology (n + 1) X is killed by the index of some open subgroup of G, so Hⁿ⁺¹(G, X) is a torsion group; and when X is a ℚ-vector space, Hⁿ⁺¹(G, X) vanishes (NSW (1.6.1)). Degree zero is excluded on purpose: H⁰(G, X) = X^G is not torsion in general, for instance for the trivial action on ℤ.

The argument runs on Mathlib's coinduced resolution X → C(G, X) → C(G, C(G, X)) → ⋯, whose differentials are d₀ = const and dₘ₊₁ F = const F - dₘ ∘ F. Evaluation at any point x : G contracts that resolution, dₘ (F x) + (dₘ₊₁ F) x = F, but it is not G-equivariant, so it does not descend to the homogeneous cochains. The sum of the evaluations over a transversal of an open subgroup U does descend, as soon as the cochain F is invariant under right translation by U. A homogeneous cochain of a discrete representation of a compact group is locally constant, so its right-translation stabilizer is such an open subgroup, of finite index [G : U]. Summing the contraction identity over the cosets of U then exhibits [G : U] • F as a coboundary whenever F is a cocycle of positive degree. For a ℚ-vector space X, division by [G : U] is an endomorphism of X, and the additivity of Hⁿ⁺¹(G, -) turns the annihilation into vanishing.

The summed contraction identity is TopRep.d_sum_apply_add_sum_d_apply, and the invariance of the coset sum is ContRepresentation.sum_apply_out_mem_invariants.

A second, hypothesis-free form of the same phenomenon is also recorded here: an exponent of the coefficients is an exponent of Hⁿ(G, X) in every degree, for any topological group, by exponent-inheritance along the coinduced resolution.

Torsion in positive degree keeps the long exact sequence of a short exact sequence 0 → A → B → C → 0 of discrete modules over a compact group exact on p-primary components: a p-primary class in the image of a map of torsion groups has a p-primary preimage (TauCeti.exists_mem_primaryComponent_apply_eq).

Main results

• TauCeti.ContinuousCohomology.exists_openSubgroup_index_nsmul_eq_zero: every class of positive degree is killed by the index of an open subgroup.
• TauCeti.ContinuousCohomology.isAddTorsion_continuousCohomology: Hⁿ⁺¹(G, X) is torsion.
• TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_module_rat: Hⁿ⁺¹(G, X) vanishes when X is a ℚ-vector space.
• TauCeti.ContinuousCohomology.nsmul_continuousCohomology_eq_zero: in every degree, and over any topological group, Hⁿ(G, X) is killed by every N that kills X.
• TauCeti.ContCohomology.DiscreteShortExact.primaryComponent_middle_eq_bot and TauCeti.ContCohomology.DiscreteShortExact.primaryComponent_right_eq_bot: the long exact sequence of a short exact sequence of discrete modules over a compact group is exact on p-primary components in positive degrees.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.1).
• K. S. Brown, Cohomology of Groups, Chapter III, (10.1), the model for finite groups.

Torsion

theorem TauCeti.ContinuousCohomology.exists_openSubgroup_index_nsmul_eq_zero {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {X : TopRep k G} [DiscreteTopology ↑X] (n : ℕ) (x : ↑(continuousCohomology (n + 1) X).toModuleCat) : ∃ (U : OpenSubgroup G), (↑U).index • x = 0

Continuous cohomology of positive degree is killed by finite indices. Over a compact group, every class of Hⁿ⁺¹(G, X) for a discrete representation X is annihilated by the index [G : U] of some open subgroup U.

theorem TauCeti.ContinuousCohomology.isAddTorsion_continuousCohomology {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {X : TopRep k G} [DiscreteTopology ↑X] (n : ℕ) : IsAddTorsion ↑(continuousCohomology (n + 1) X).toModuleCat

Continuous cohomology of positive degree is torsion (NSW (1.6.1)). Over a compact group, Hⁿ⁺¹(G, X) is a torsion group for every discrete representation X. Degree zero is excluded: H⁰(G, X) = X^G need not be torsion.

theorem TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_module_rat {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {X : TopRep k G} [DiscreteTopology ↑X] [Module ℚ ↑X] (n : ℕ) : Subsingleton ↑(continuousCohomology (n + 1) X).toModuleCat

Continuous cohomology with rational coefficients vanishes in positive degree. Over a compact group, Hⁿ⁺¹(G, X) = 0 for every discrete representation X whose underlying group is a ℚ-vector space.

Exponents inherited from the coefficients

theorem TauCeti.ContinuousCohomology.nsmul_resolutionX_eq_zero {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {N : ℕ} (hX : ∀ (x : ↑X), N • x = 0) (n : ℕ) (F : ↑(X.resolutionX n)) : N • F = 0

Every term of the coinduced resolution of X is killed by N when X is.

theorem TauCeti.ContinuousCohomology.nsmul_continuousCohomology_eq_zero {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {N : ℕ} (hX : ∀ (x : ↑X), N • x = 0) (n : ℕ) (x : ↑(continuousCohomology n X).toModuleCat) : N • x = 0

Continuous cohomology inherits the exponent of its coefficients: if N kills every element of X, then it kills every class of Hⁿ(G, X), in every degree. It is the all-degree counterpart of TauCeti.ContCohomology.nsmul_H1_eq_zero and TauCeti.ContCohomology.nsmul_H2_eq_zero.

Exactness on p-primary components

theorem TauCeti.ContCohomology.DiscreteShortExact.primaryComponent_middle_eq_bot {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (hp : Nat.Prime p) {n : ℕ} (hA : AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G A)).toModuleCat) p = ⊥) (hC : AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G C)).toModuleCat) p = ⊥) : AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G B)).toModuleCat) p = ⊥

Exactness at Hⁿ⁺¹(G, B) on p-primary components. For a short exact sequence 0 → A → B → C → 0 of discrete modules over a compact group and a prime p, if the p-primary components of Hⁿ⁺¹(G, A) and Hⁿ⁺¹(G, C) vanish, so does that of Hⁿ⁺¹(G, B).

theorem TauCeti.ContCohomology.DiscreteShortExact.primaryComponent_right_eq_bot {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (hp : Nat.Prime p) {n : ℕ} (hB : AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G B)).toModuleCat) p = ⊥) (hA : AddCommGroup.primaryComponent (↑(continuousCohomology (n + 2) (ofDiscreteModule ℤ G A)).toModuleCat) p = ⊥) : AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G C)).toModuleCat) p = ⊥

Exactness at Hⁿ⁺¹(G, C) on p-primary components. For a short exact sequence 0 → A → B → C → 0 of discrete modules over a compact group and a prime p, if the p-primary components of Hⁿ⁺¹(G, B) and Hⁿ⁺²(G, A) vanish, so does that of Hⁿ⁺¹(G, C).