The cohomological dimension of a pro-p group is detected on 𝔽_p

Let G be a compact pro-p group. Its p-cohomological dimension cd_p G asks for the vanishing of Hⁱ(G, M) in every degree i > n and for every discrete p-primary torsion G-module M. For a pro-p group the single module 𝔽_p with trivial action suffices:

cd_p G ≤ n if and only if Hⁿ⁺¹(G, 𝔽_p) = 0.

Two reductions compose. Cohomological dimension is detected in the single degree n + 1 on the finite discrete p-primary modules (TauCeti.cohomologicalDimensionAt_le_iff_forall_finite_subsingleton_succ, by dimension shifting), and for a pro-p group the vanishing of a fixed degree on those modules is detected on the trivial modules of order p (TauCeti.IsProP.forall_subsingleton_continuousCohomology_iff_forall_natCard_eq, by dévissage along the trivial filtration). A trivial discrete G-module of order p is 𝔽_p up to a G-equivariant isomorphism, so its cohomology is cohomFp p G (n + 1) (TauCeti.subsingleton_continuousCohomology_iff_subsingleton_cohomFp_of_natCard_eq).

This is a reduction and not a definition: cd_p G is the standard invariant, and the equivalence is the content of dévissage. The pro-p hypothesis is used. For the symmetric group S₃ at p = 3, H¹(S₃, 𝔽₃) = Hom(S₃, 𝔽₃) vanishes, while cd_3 S₃ is not 0: by Shapiro's lemma H¹(S₃, 𝔽₃[S₃/C₃]) = H¹(C₃, 𝔽₃) ≠ 0, and 𝔽₃[S₃/C₃] is a finite 3-primary module.

The equivalence is restated for <, = and = ⊤: n < cd_p G exactly when Hⁿ⁺¹(G, 𝔽_p) ≠ 0, cd_p G = n exactly when Hⁿ⁺¹(G, 𝔽_p) = 0 and Hⁿ(G, 𝔽_p) ≠ 0, and cd_p G = ⊤ exactly when Hⁿ(G, 𝔽_p) ≠ 0 for every n.

The file also records Tate's criterion for a profinite pro-p group: if Hⁿ(G, -) is right exact on the finite discrete G-modules killed by p, then cd_p G ≤ n. The vanishing of Hⁿ⁺¹ on those modules is TauCeti.subsingleton_continuousCohomology_succ_of_forall_coeffMap_proj_surjective, and dévissage extends it to all finite p-primary modules. In degree 2 the right exactness follows from duality: if Tate's duality map α₂ : H²(G, M) → Hom(H⁰(G, Hom(M, N)), H²(G, N)) is bijective for every finite discrete M killed by p, then cd_p G ≤ 2 (TauCeti.IsProP.cohomologicalDimensionAt_le_two_of_forall_dualityMap2_bijective). This is how the cohomological dimension of a Demushkin group is bounded (Serre, Structure de certains pro-p-groupes, §9.1).

Conversely, cd_p G ≤ 2 makes H²(G, -) right exact on the twisted coefficients I(χ)/pⁱ of a continuous character χ : G →ₜ* ℤ_pˣ of a compact group G: every reduction H²(G, I(χ)/pⁿ) → H²(G, I(χ)/pʲ) is surjective, because the next term H³ of the long exact sequence vanishes (TauCeti.ZModTwist.surjective_explicitCoeff2_reduce_of_cohomologicalDimensionAt_le_two).

Main results

• TauCeti.IsProP.cohomologicalDimensionAt_le_iff_forall_smul_eq_self, TauCeti.IsProP.cohomologicalDimensionAt_le_iff_forall_natCard_eq_smul_eq_self: the pro-p reduction of cd_p G ≤ n to the finite trivial modules killed by p, resp. of order p.
• TauCeti.IsProP.cohomologicalDimensionAt_le_iff_subsingleton_cohomFp: the pro-p reduction of cd_p, cd_p G ≤ n ↔ Hⁿ⁺¹(G, 𝔽_p) = 0.
• TauCeti.IsProP.lt_cohomologicalDimensionAt_iff_nontrivial_cohomFp, TauCeti.IsProP.cohomologicalDimensionAt_eq_iff, TauCeti.IsProP.cohomologicalDimensionAt_eq_top_iff: the <, = and = ⊤ forms.
• TauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective: Tate's criterion: right exactness of Hⁿ(G, -) on the finite discrete G-modules killed by p gives cd_p G ≤ n.
• TauCeti.IsProP.cohomologicalDimensionAt_le_two_of_forall_dualityMap2_bijective: Tate's duality criterion: bijectivity of α₂ on the finite discrete G-modules killed by p gives cd_p G ≤ 2.
• TauCeti.ZModTwist.surjective_explicitCoeff2_reduce_of_cohomologicalDimensionAt_le_two: for a compact group with cd_p G ≤ 2, every reduction H²(G, I(χ)/pⁿ) → H²(G, I(χ)/pʲ) of the twisted coefficients is surjective.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §4.1, Prop. 21.
• J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki, exp. 252 (1963), §9.1.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.3.2).
• H. Koch, Galois Theory of p-Extensions, Springer (2002), Definition 5.1.

theorem TauCeti.IsProP.cohomologicalDimensionAt_le_iff_forall_natCard_eq_smul_eq_self {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : cohomologicalDimensionAt p G ≤ ↑n ↔ ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A], Nat.card A = p → (∀ (g : G) (a : A), g • a = a) → Subsingleton ↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G A)).toModuleCat

The pro-p reduction of cd_p, on the trivial modules of order p. For a compact pro-p group G, cd_p G ≤ n exactly when Hⁿ⁺¹(G, A) vanishes for every discrete G-module A of order p with trivial action.

theorem TauCeti.IsProP.cohomologicalDimensionAt_le_iff_forall_smul_eq_self {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : cohomologicalDimensionAt p G ≤ ↑n ↔ ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A], (∀ (a : A), p • a = 0) → (∀ (g : G) (a : A), g • a = a) → Subsingleton ↑(continuousCohomology (n + 1) (ofDiscreteModule ℤ G A)).toModuleCat

The pro-p reduction of cd_p, on the finite trivial modules killed by p. For a compact pro-p group G, cd_p G ≤ n exactly when Hⁿ⁺¹(G, A) vanishes for every finite discrete G-module A killed by p with trivial action, that is for every finite elementary abelian p-group with trivial action.

theorem TauCeti.IsProP.cohomologicalDimensionAt_le_iff_subsingleton_cohomFp {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : cohomologicalDimensionAt p G ≤ ↑n ↔ Subsingleton ↑(cohomFp p G (n + 1)).toModuleCat

The pro-p reduction of cd_p to the single module 𝔽_p. For a compact pro-p group G, cd_p G ≤ n exactly when Hⁿ⁺¹(G, 𝔽_p) vanishes.

theorem TauCeti.IsProP.cohomologicalDimensionAt_le_iff_forall_subsingleton_cohomFp {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : cohomologicalDimensionAt p G ≤ ↑n ↔ ∀ (m : ℕ), n < m → Subsingleton ↑(cohomFp p G m).toModuleCat

For a compact pro-p group G, cd_p G ≤ n exactly when Hᵐ(G, 𝔽_p) vanishes for every m > n.

theorem TauCeti.IsProP.lt_cohomologicalDimensionAt_iff_nontrivial_cohomFp {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : ↑n < cohomologicalDimensionAt p G ↔ Nontrivial ↑(cohomFp p G (n + 1)).toModuleCat

For a compact pro-p group G, n < cd_p G exactly when Hⁿ⁺¹(G, 𝔽_p) is nontrivial.

theorem TauCeti.IsProP.le_cohomologicalDimensionAt_iff_nontrivial_cohomFp {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : ↑(n + 1) ≤ cohomologicalDimensionAt p G ↔ Nontrivial ↑(cohomFp p G (n + 1)).toModuleCat

For a compact pro-p group G, n + 1 ≤ cd_p G exactly when Hⁿ⁺¹(G, 𝔽_p) is nontrivial.

theorem TauCeti.IsProP.cohomologicalDimensionAt_eq_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) (n : ℕ) : cohomologicalDimensionAt p G = ↑n ↔ Subsingleton ↑(cohomFp p G (n + 1)).toModuleCat ∧ Nontrivial ↑(cohomFp p G n).toModuleCat

cd_p G = n on 𝔽_p. For a compact pro-p group G, cd_p G = n exactly when Hⁿ⁺¹(G, 𝔽_p) vanishes and Hⁿ(G, 𝔽_p) does not.

theorem TauCeti.IsProP.cohomologicalDimensionAt_eq_top_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) : cohomologicalDimensionAt p G = ⊤ ↔ ∀ (n : ℕ), Nontrivial ↑(cohomFp p G n).toModuleCat

Infinite cd_p on 𝔽_p. For a compact pro-p group G, cd_p G = ⊤ exactly when Hⁿ(G, 𝔽_p) is nontrivial in every degree.

theorem TauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) [TotallyDisconnectedSpace G] (n : ℕ) (h : ∀ (A B C : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A] [inst_6 : AddCommGroup B] [inst_7 : TopologicalSpace B] [inst_8 : DiscreteTopology B] [inst_9 : DistribMulAction G B] [ContinuousSMul G B] [Finite B] [inst_12 : AddCommGroup C] [inst_13 : TopologicalSpace C] [inst_14 : DiscreteTopology C] [inst_15 : DistribMulAction G C] [ContinuousSMul G C] [Finite C] (S : ContCohomology.DiscreteShortExact G A B C), (∀ (a : A), p • a = 0) → (∀ (b : B), p • b = 0) → (∀ (c : C), p • c = 0) → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap S.proj.toIntLinearMap ⋯) n))) : cohomologicalDimensionAt p G ≤ ↑n

Tate's criterion for the cohomological dimension of a pro-p group. Let G be a profinite pro-p group. If for every short exact sequence 0 → A → B → C → 0 of finite discrete G-modules killed by p the map Hⁿ(G, B) → Hⁿ(G, C) is surjective, then cd_p G ≤ n: right exactness kills Hⁿ⁺¹ on those modules, and dévissage extends the vanishing to every finite discrete p-primary module.

theorem TauCeti.IsProP.cohomologicalDimensionAt_le_two_of_forall_dualityMap2_bijective {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsProP p G) [TotallyDisconnectedSpace G] (N : Type v) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (h : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M] [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [inst_4 : ContinuousSMul G M] [Finite M], (∀ (m : M), p • m = 0) → Function.Bijective ⇑(ContCohomology.dualityMap2 G M N)) : cohomologicalDimensionAt p G ≤ 2

Tate's duality criterion for cd_p G ≤ 2. Let G be a profinite pro-p group and N a discrete G-module. If Tate's duality map in degree two, α₂ : H²(G, M) → Hom(H⁰(G, InternalHom G M N), H²(G, N)), is bijective for every finite discrete G-module M killed by p, then cd_p G ≤ 2: duality makes H²(G, -) right exact on those modules (TauCeti.ContCohomology.DiscreteShortExact.coeffMap_proj_surjective_of_dualityMap2), and right exactness bounds the dimension. For an infinite Demushkin group and N = 𝔽_p the hypothesis is Tate's perfect duality, and the conclusion is the upper bound in cd_p G = 2.

theorem TauCeti.ZModTwist.surjective_explicitCoeff2_reduce_of_cohomologicalDimensionAt_le_two {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (χ : G →ₜ* ℤ_[p]ˣ) (h : cohomologicalDimensionAt p G ≤ 2) {j n : ℕ} (hj : j ≤ n) : Function.Surjective ⇑(ContCohomology.explicitCoeff2 G (ZModTwist χ n) (reduce χ hj) ⋯)

cd_p G ≤ 2 makes H²(G, -) right exact on the twisted coefficients: for a compact group G with cd_p G ≤ 2, every reduction H²(G, I(χ)/pⁿ) → H²(G, I(χ)/pʲ), j ≤ n, is surjective, because the next term H³(G, I(χ)/pⁿ⁻ʲ) of the long exact sequence vanishes.