Cohomological dimension is detected in a single degree

For a compact group G, the vanishing predicate CohomologicalDimensionLE p G n, which asks for Hⁱ(G, M) = 0 in every degree i > n and for every discrete p-primary torsion G-module M, holds as soon as the single degree n + 1 vanishes for every such M. Dimension shifting supplies the induction step: Hⁱ⁺¹(G, M) ≅ Hⁱ(G, Coind_1^G M ⧸ M) for i ≥ 1 (TauCeti.ContCohomology.dimensionShiftIso), and the shifted module Coind_1^G M ⧸ M is again a discrete p-primary torsion module (TauCeti.ContCohomology.isPPrimaryTorsion_coindQuotient), so vanishing in degree i for every module of the class gives vanishing in degree i + 1 for every module of the class. The shifted module need not be finite even when M is, which is why the statement quantifies over all discrete p-primary torsion modules; the single-degree test on the finite modules then follows because, in each fixed degree, the vanishing of Hⁱ(G, M) for a discrete p-primary torsion M is detected on the finite discrete p-primary G-modules (TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_forall_finite).

The two tests are recorded for the predicate and for the invariant cd_p G. They are the standard reductions of Serre, Galois Cohomology, I §3.2, Prop. 11, and of Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, (3.3.2), before the passage to simple modules, which for a pro-p group is the further reduction to the single module 𝔽_p.

Main results

• TauCeti.cohomologicalDimensionLE_iff_forall_subsingleton_succ: CohomologicalDimensionLE p G n holds exactly when Hⁿ⁺¹(G, M) vanishes for every discrete p-primary torsion G-module M.
• TauCeti.cohomologicalDimensionLE_iff_forall_finite_subsingleton_succ: the same test on the finite modules, for p ≠ 0.
• TauCeti.cohomologicalDimensionAt_le_iff_forall_subsingleton_succ and TauCeti.cohomologicalDimensionAt_le_iff_forall_finite_subsingleton_succ: the two tests for cd_p G ≤ n.

References

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

theorem TauCeti.cohomologicalDimensionLE_iff_forall_subsingleton_succ {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (n : ℕ) : CohomologicalDimensionLE p G n ↔ ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M], IsPPrimaryTorsion p M → Subsingleton ↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G M)).toModuleCat

Vanishing in one degree gives vanishing above it. For a compact group G, the predicate CohomologicalDimensionLE p G n holds exactly when Hⁿ⁺¹(G, M) vanishes for every discrete p-primary torsion G-module M: dimension shifting through Coind_1^G M carries vanishing in degree n + 1 upward, one degree at a time.

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

The finite single-degree test. For a compact group G and p ≠ 0, the predicate CohomologicalDimensionLE p G n holds exactly when Hⁿ⁺¹(G, M) vanishes for every finite discrete p-primary G-module M.

theorem TauCeti.cohomologicalDimensionAt_le_iff_forall_subsingleton_succ (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (n : ℕ) : cohomologicalDimensionAt p G ≤ ↑n ↔ ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [ContinuousSMul G M], IsPPrimaryTorsion p M → Subsingleton ↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G M)).toModuleCat

cd_p G ≤ n is detected in degree n + 1: for a compact group G, cd_p G ≤ n exactly when Hⁿ⁺¹(G, M) vanishes for every discrete p-primary torsion G-module M.

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

cd_p G ≤ n is detected in degree n + 1 on finite coefficients: for a compact group G and p ≠ 0, cd_p G ≤ n exactly when Hⁿ⁺¹(G, M) vanishes for every finite discrete p-primary G-module M.