The strict cohomological dimension through integral coefficients

Let G be a profinite group and p a prime. Then scd_p G ≤ n if and only if cd_p G ≤ n and the p-primary component of Hⁿ⁺¹(U, ℤ) vanishes for every open subgroup U, the integers carrying the trivial action (NSW (3.3.4)). NSW states the criterion as "if cd_p G = n is finite, then scd_p G = n if and only if …"; the inequality form below holds for every n.

The forward direction is cd_p G ≤ scd_p G together with scd_p U ≤ scd_p G for the closed subgroup U, read on the trivial module ℤ through TauCeti.StrictCohomologicalDimensionLE.primaryComponent_eq_bot_of_isSmoothDiscrete. For the converse, scd_p G ≤ cd_p G + 1 disposes of every degree above n + 1, and the work is in degree n + 1, where the p-primary component of Hⁿ⁺¹(G, M) has to vanish for every discrete G-module M.

• Exactness on p-primary components. For a short exact sequence 0 → A → B → C → 0 of discrete modules over a compact group, cohomology in positive degree is torsion, and a p-primary class in the image of a map of torsion groups has a p-primary preimage (TauCeti.exists_mem_primaryComponent_apply_eq). So the long exact sequence stays exact on p-primary components: if those of Hⁱ(G, A) and Hⁱ(G, C) vanish, so does that of Hⁱ(G, B), and if those of Hⁱ(G, B) and Hⁱ⁺¹(G, A) vanish, so does that of Hⁱ(G, C) (TauCeti.ContCohomology.DiscreteShortExact.primaryComponent_middle_eq_bot and TauCeti.ContCohomology.DiscreteShortExact.primaryComponent_right_eq_bot).
• Cyclic modules. A discrete G-module Q generated by the orbit of one element q is a quotient of Coind_U^G ℤ for the stabilizer U of q, by the trace of the coinduction of the map ℤ → Q, 1 ↦ q. Shapiro's lemma identifies Hⁿ⁺¹(G, Coind_U^G ℤ) with Hⁿ⁺¹(U, ℤ), and Hⁿ⁺² of the kernel has vanishing p-primary component because scd_p G ≤ n + 1.
• Finitely generated modules. A module generated by the orbits of finitely many elements is an extension of a cyclic module by a module generated by fewer orbits.
• All modules. Every class of Hⁿ⁺¹(G, M) comes from a submodule generated by the orbits of the finitely many values of a representing cocycle (TauCeti.ContinuousCohomology.exists_finite_forall_mem_range_coeffMap).

Main results

• TauCeti.CohomologicalDimensionLE.strictCohomologicalDimensionLE_of_forall_openSubgroup: the converse direction, as vanishing predicates.
• TauCeti.strictCohomologicalDimensionLE_iff_forall_openSubgroup, TauCeti.strictCohomologicalDimensionAt_le_iff_forall_openSubgroup: the criterion, scd_p G ≤ n ↔ cd_p G ≤ n ∧ ∀ U open, Hⁿ⁺¹(U, ℤ)(p) = 0.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.3.4) and its proof.

Cyclic modules

Finitely generated modules

The criterion

theorem TauCeti.CohomologicalDimensionLE.strictCohomologicalDimensionLE_of_forall_openSubgroup {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (hp : Nat.Prime p) (h : CohomologicalDimensionLE p G n) (hZ : ∀ (U : OpenSubgroup G), AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (TopRep.of (ContRepresentation.trivial ℤ (↥↑U) (ULift.{u, 0} ℤ)))).toModuleCat) p = ⊥) : StrictCohomologicalDimensionLE p G n

The converse half of NSW (3.3.4), as vanishing predicates. For a profinite group G and a prime p, if CohomologicalDimensionLE p G n holds and the p-primary component of Hⁿ⁺¹(U, ℤ) vanishes for every open subgroup U, the integers carrying the trivial action, then StrictCohomologicalDimensionLE p G n holds.

theorem TauCeti.strictCohomologicalDimensionLE_iff_forall_openSubgroup {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (hp : Nat.Prime p) : StrictCohomologicalDimensionLE p G n ↔ CohomologicalDimensionLE p G n ∧ ∀ (U : OpenSubgroup G), AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (TopRep.of (ContRepresentation.trivial ℤ (↥↑U) (ULift.{u, 0} ℤ)))).toModuleCat) p = ⊥

The strict cohomological dimension through integral coefficients (NSW (3.3.4)), as vanishing predicates. For a profinite group G and a prime p, StrictCohomologicalDimensionLE p G n holds if and only if CohomologicalDimensionLE p G n holds and the p-primary component of Hⁿ⁺¹(U, ℤ) vanishes for every open subgroup U, the integers carrying the trivial action.

theorem TauCeti.strictCohomologicalDimensionAt_le_iff_forall_openSubgroup {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : Nat.Prime p) (n : ℕ) : strictCohomologicalDimensionAt p G ≤ ↑n ↔ cohomologicalDimensionAt p G ≤ ↑n ∧ ∀ (U : OpenSubgroup G), AddCommGroup.primaryComponent (↑(continuousCohomology (n + 1) (TopRep.of (ContRepresentation.trivial ℤ (↥↑U) (ULift.{u, 0} ℤ)))).toModuleCat) p = ⊥

The strict cohomological dimension through integral coefficients (NSW (3.3.4)). For a profinite group G and a prime p, scd_p G ≤ n if and only if cd_p G ≤ n and the p-primary component of Hⁿ⁺¹(U, ℤ) vanishes for every open subgroup U, the integers carrying the trivial action.