Continuous cohomology of a discrete module is detected on finite sets of values

Let G be a compact group and X a discrete topological representation of G. Mathlib's continuous cohomology Hⁿ(G, X) is the homology of the homogeneous cochain complex, whose degree n term consists of the G-invariant elements of the iterated function space C(G, C(G, …, C(G, X))) with n + 1 arguments. Because G is compact and X is discrete, every such cochain takes only finitely many values in X once all its arguments are evaluated. This file records that fact and its consequence for cohomology: every class of Hⁿ(G, X) is the image of a class of Hⁿ(G, Y) for any subrepresentation Y ⊆ X containing those finitely many values. Without further hypotheses Y may be infinite, since the values need not generate a finite subgroup.

For a discrete torsion G-module M with continuous action, the values of a cocycle generate a finite G-stable subgroup N ≤ M, so every class of Hⁿ(G, M) comes from Hⁿ(G, N) for a finite N. In particular the vanishing of Hⁿ(G, -) on all finite p-primary discrete modules implies its vanishing on all p-primary discrete modules, which lets the p-cohomological dimension be tested on finite coefficient modules alone. This is the coefficient half of the dévissage of NSW (3.3.2), the other half being the reduction of the degree through dimension shifting.

Main definitions

• TauCeti.ContinuousCohomology.resolutionValues: the set of values in X of an element of the n-th term of the coinduced resolution of X.

Main results

• TauCeti.ContinuousCohomology.finite_resolutionValues: over a compact group, an element of the resolution of a discrete representation takes finitely many values.
• TauCeti.ContinuousCohomology.exists_resolutionMap_eq_of_resolutionValues_subset: an element of the resolution of X whose values lie in the range of an injective morphism Y ⟶ X comes from the resolution of Y.
• TauCeti.ContinuousCohomology.exists_finite_forall_mem_range_coeffMap: each class of Hⁿ(G, X) has a finite set of values S ⊆ X such that it lies in the range of coeffMap ι n for every injective ι : Y ⟶ X whose range contains S.
• TauCeti.ContinuousCohomology.exists_finite_addSubgroup_coeffMap_eq: each class of Hⁿ(G, M), for a discrete torsion G-module M, comes from a finite G-stable subgroup of M.
• TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_forall_finite_addSubgroup: Hⁿ(G, M) vanishes as soon as Hⁿ(G, N) vanishes for every finite G-stable subgroup N.
• TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_forall_finite: for a discrete p-primary torsion M and p ≠ 0, Hⁿ(G, M) vanishes as soon as Hⁿ(G, N) vanishes for every finite discrete p-primary G-module N.
• TauCeti.cohomologicalDimensionLE_iff_forall_finite, TauCeti.cohomologicalDimensionAt_le_iff_forall_finite: the p-cohomological dimension of a compact group is at most n exactly when Hⁱ(G, M) vanishes for every i > n and every finite discrete p-primary G-module M.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.3.2).
• J.-P. Serre, Galois Cohomology, Ch. I §3.1.

The values of an element of the coinduced resolution

def TauCeti.ContinuousCohomology.resolutionValues {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : ↑(X.resolutionX n) → Set ↑X

The set of values in X of an element of the n-th term C(G, C(G, …, X)) of the coinduced resolution of X: the values obtained by evaluating all n function arguments.

Equations

• TauCeti.ContinuousCohomology.resolutionValues X 0 x_2 = {x_2}
• TauCeti.ContinuousCohomology.resolutionValues X n.succ f = ⋃ (g : G), TauCeti.ContinuousCohomology.resolutionValues X n (f g)

@[simp]

theorem TauCeti.ContinuousCohomology.resolutionValues_zero {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (x : ↑X) : resolutionValues X 0 x = {x}

@[simp]

theorem TauCeti.ContinuousCohomology.resolutionValues_succ {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (f : ↑(X.resolutionX (n + 1))) : resolutionValues X (n + 1) f = ⋃ (g : G), resolutionValues X n (f g)

theorem TauCeti.ContinuousCohomology.resolutionValues_apply_subset {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (f : ↑(X.resolutionX (n + 1))) (g : G) : resolutionValues X n (f g) ⊆ resolutionValues X (n + 1) f

Evaluating the outermost argument of an element of the resolution does not enlarge its set of values.

theorem TauCeti.ContinuousCohomology.finite_resolutionValues {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [CompactSpace G] [DiscreteTopology ↑X] (n : ℕ) (x : ↑(X.resolutionX n)) : (resolutionValues X n x).Finite

Over a compact group, an element of the coinduced resolution of a discrete representation takes only finitely many values: each of its function arguments ranges over a compact space and lands in a discrete one.

Lifting along an injective morphism of coefficients

theorem TauCeti.ContinuousCohomology.resolutionMap_isInducing {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {Y X : TopRep k G} (ι : Y ⟶ X) (hι : Topology.IsInducing ⇑(TopRep.Hom.hom ι)) (n : ℕ) : Topology.IsInducing ⇑(TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) ι n))

The maps induced on the coinduced resolutions by an inducing morphism of representations are inducing in every degree: each term of the resolution of Y carries the topology induced from the corresponding term of the resolution of X.

theorem TauCeti.ContinuousCohomology.exists_resolutionMap_eq_of_resolutionValues_subset {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {Y X : TopRep k G} (ι : Y ⟶ X) [DiscreteTopology ↑X] [DiscreteTopology ↑Y] (hι : Function.Injective ⇑(TopRep.Hom.hom ι)) (n : ℕ) (x : ↑(X.resolutionX n)) : resolutionValues X n x ⊆ Set.range ⇑(TopRep.Hom.hom ι) → ∃ (y : ↑(Y.resolutionX n)), (TopRep.Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) ι n)) y = x

An element of the coinduced resolution of X all of whose values lie in the range of an injective morphism ι : Y ⟶ X comes from the coinduced resolution of Y.

theorem TauCeti.ContinuousCohomology.exists_cochainsMap_f_eq_of_resolutionValues_subset {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {Y X : TopRep k G} (ι : Y ⟶ X) [DiscreteTopology ↑X] [DiscreteTopology ↑Y] (hι : Function.Injective ⇑(TopRep.Hom.hom ι)) (n : ℕ) (c : ↑(X.homogeneousCochains.X n).toModuleCat) (hc : resolutionValues X (n + 1) ↑c ⊆ Set.range ⇑(TopRep.Hom.hom ι)) : ∃ (c' : ↑(Y.homogeneousCochains.X n).toModuleCat), (CategoryTheory.ConcreteCategory.hom ((ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) ι).f n)) c' = c

An invariant element of the coinduced resolution of X, that is a homogeneous cochain, all of whose values lie in the range of an injective morphism ι : Y ⟶ X is the image of a homogeneous cochain of Y under the induced cochain map.

Every cohomology class comes from a finite set of values

theorem TauCeti.ContinuousCohomology.exists_finite_forall_mem_range_coeffMap {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {X : TopRep k G} [DiscreteTopology ↑X] (n : ℕ) (x : ↑(continuousCohomology n X).toModuleCat) : ∃ (S : Set ↑X), S.Finite ∧ ∀ (Y : TopRep k G) [DiscreteTopology ↑Y] (ι : Y ⟶ X), Function.Injective ⇑(TopRep.Hom.hom ι) → S ⊆ Set.range ⇑(TopRep.Hom.hom ι) → x ∈ Set.range ⇑(TopModuleCat.Hom.hom (coeffMap ι n))

Every continuous cohomology class of a discrete representation of a compact group comes from finitely many values. For each class x ∈ Hⁿ(G, X) there is a finite set S ⊆ X such that x lies in the image of Hⁿ(G, Y) under coeffMap ι n for every injective morphism ι : Y ⟶ X from a discrete representation whose range contains S.

Discrete torsion modules: every class comes from a finite stable subgroup

theorem TauCeti.ContinuousCohomology.exists_finite_addSubgroup_coeffMap_eq {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type (max v w)} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hM : IsAddTorsion M) (n : ℕ) (x : ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat) : ∃ (N : AddSubgroup M) (hN : ∀ (g : G), ∀ m ∈ N, g • m ∈ N), Finite ↥N ∧ ∃ (y : ↑(continuousCohomology n (ofDiscreteModule ℤ G ↥N)).toModuleCat), (CategoryTheory.ConcreteCategory.hom (coeffMap (ofDiscreteModuleMap N.subtype.toIntLinearMap ⋯) n)) y = x

Every class of Hⁿ(G, M) comes from a finite G-stable subgroup. Let G be a compact group and M a discrete torsion G-module with continuous action. Every class of Hⁿ(G, M) is the image of a class of Hⁿ(G, N) for some finite G-stable additive subgroup N ≤ M, under the coefficient map of the inclusion. The subgroup is generated by the finitely many values of a representing cocycle and their G-translates; it is finite because each orbit is finite and M is torsion.

theorem TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_forall_finite_addSubgroup {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type (max v w)} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (hM : IsAddTorsion M) (n : ℕ) (h : ∀ (N : AddSubgroup M) (hN : ∀ (g : G), ∀ m ∈ N, g • m ∈ N), Finite ↥N → Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G ↥N)).toModuleCat) : Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat

Vanishing of continuous cohomology is detected on finite stable subgroups. Let G be a compact group and M a discrete torsion G-module with continuous action. If Hⁿ(G, N) vanishes for every finite G-stable additive subgroup N ≤ M, then Hⁿ(G, M) vanishes.

theorem TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_forall_finite {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type (max v w)} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] {p : ℕ} (hp : p ≠ 0) (hM : IsPPrimaryTorsion p M) (n : ℕ) (h : ∀ (N : Type (max v w)) [inst : AddCommGroup N] [inst_1 : TopologicalSpace N] [inst_2 : DiscreteTopology N] [inst_3 : DistribMulAction G N] [ContinuousSMul G N] [Finite N], IsPPrimaryTorsion p N → Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G N)).toModuleCat) : Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat

Vanishing of continuous cohomology is detected on finite p-primary coefficients, in a fixed degree. Let G be a compact group, p ≠ 0, and M a discrete p-primary torsion G-module with continuous action. If Hⁿ(G, N) vanishes for every finite discrete p-primary G-module N, then Hⁿ(G, M) vanishes.

Cohomological dimension is detected on finite coefficient modules

theorem TauCeti.cohomologicalDimensionLE_iff_forall_finite {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hp : p ≠ 0) {n : ℕ} : CohomologicalDimensionLE p G n ↔ ∀ (M : Type (max u v)) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M] [Finite M], IsPPrimaryTorsion p M → ∀ (i : ℕ), n < i → Subsingleton ↑(continuousCohomology i (ofDiscreteModule ℤ G M)).toModuleCat

The finite-coefficient test for the vanishing predicate of cohomological dimension (NSW (3.3.2), coefficient reduction). For a compact group G and p ≠ 0, the predicate CohomologicalDimensionLE p G n holds exactly when Hⁱ(G, M) vanishes for every i > n and every finite discrete p-primary G-module M.

theorem TauCeti.cohomologicalDimensionAt_le_iff_forall_finite {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hp : p ≠ 0) (n : ℕ) : cohomologicalDimensionAt p G ≤ ↑n ↔ ∀ (M : Type (max u v)) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M] [Finite M], IsPPrimaryTorsion p M → ∀ (i : ℕ), n < i → Subsingleton ↑(continuousCohomology i (ofDiscreteModule ℤ G M)).toModuleCat

The p-cohomological dimension of a compact group is detected on finite coefficients (NSW (3.3.2), coefficient reduction). For p ≠ 0, cd_p G ≤ n exactly when Hⁱ(G, M) vanishes for every i > n and every finite discrete p-primary G-module M.