Cohomological dimension and trivial 𝔽_p coefficients

The vanishing predicate behind the p-cohomological dimension cd_p G = cohomologicalDimensionAt p G quantifies over all discrete p-primary torsion G-modules M, with the continuous cohomology of ofDiscreteModule ℤ G M, while the coefficient object of the pro-p theory is the representation trivialFp p G of G on 𝔽_p over the scalars ZMod p, with cohomology cohomFp p G n. This file connects the two. The carrier of trivialFp p G is a discrete trivial G-module whose Nat.card is p, hence p-primary torsion, and its ℤ-cohomology vanishes exactly when cohomFp p G n does (TauCeti.ContCohomology.subsingleton_continuousCohomology_ofDiscreteModule_iff). Hence cd_p G ≤ n forces Hᵐ(G, 𝔽_p) = 0 for every m > n, and, contrapositively, a nonvanishing Hⁿ(G, 𝔽_p) bounds cd_p G from below by n.

These are the two implications valid for every topological group. For a pro-p group the first one is an equivalence, by dévissage; that is the pro-p reduction of cd_p in TauCeti.Topology.Algebra.Group.Profinite.ProP.CohomologicalDimension. The dévissage runs on the trivial discrete G-modules of prime order p, and the results here identify their cohomology with cohomFp p G n: such a module is cyclic of order p, hence G-equivariantly isomorphic to the carrier of trivialFp p G, so its cohomology is additively equivalent to cohomFp p G n (TauCeti.nonempty_cohomFp_addEquiv_of_natCard_eq), and in particular vanishes, or is finite, exactly when cohomFp p G n does. The equivalence depends on a choice of generator of the module, and only its existence is recorded.

Main results

• TauCeti.isAddPGroup_trivialFp_V: the carrier of trivialFp p G is p-primary torsion.
• TauCeti.nonempty_cohomFp_addEquiv_of_natCard_eq: the cohomology of 𝔽_p is additively equivalent to the cohomology of any trivial discrete G-module of prime order p.
• TauCeti.subsingleton_continuousCohomology_iff_subsingleton_cohomFp_of_natCard_eq, TauCeti.finite_continuousCohomology_iff_finite_cohomFp_of_natCard_eq: the cohomology of a trivial discrete G-module of prime order p vanishes, resp. is finite, exactly when that of 𝔽_p does.
• TauCeti.CohomologicalDimensionLE.subsingleton_cohomFp, TauCeti.subsingleton_cohomFp_of_cohomologicalDimensionAt_le: cd_p G ≤ n gives Hᵐ(G, 𝔽_p) = 0 for m > n.
• TauCeti.le_cohomologicalDimensionAt_of_nontrivial_cohomFp: Hⁿ(G, 𝔽_p) ≠ 0 gives n ≤ cd_p G.

References

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

theorem TauCeti.isAddPGroup_trivialFp_V (p : ℕ) (G : Type u) [Monoid G] : IsAddPGroup p ↑(trivialFp p G)

The carrier of trivialFp p G is p-primary torsion, its Nat.card being p.

theorem TauCeti.nonempty_cohomFp_addEquiv_of_natCard_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Fact (Nat.Prime p)] (A : Type u) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] (hA : Nat.card A = p) (htriv : ∀ (g : G) (a : A), g • a = a) (n : ℕ) : Nonempty (↑(cohomFp p G n).toModuleCat ≃+ ↑(continuousCohomology n (ofDiscreteModule ℤ G A)).toModuleCat)

The cohomology of 𝔽_p is that of any trivial discrete G-module of prime order p. Such a module A is cyclic of order p, hence G-equivariantly isomorphic to the carrier of trivialFp p G once a generator is chosen, and the cohomology of that carrier as a discrete ℤ-module is cohomFp p G n. The equivalence depends on the choice of generator, so only its existence is recorded.

theorem TauCeti.subsingleton_continuousCohomology_iff_subsingleton_cohomFp_of_natCard_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Fact (Nat.Prime p)] (A : Type u) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] (hA : Nat.card A = p) (htriv : ∀ (g : G) (a : A), g • a = a) (n : ℕ) : Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G A)).toModuleCat ↔ Subsingleton ↑(cohomFp p G n).toModuleCat

The cohomology of a trivial discrete G-module of prime order p vanishes exactly when that of 𝔽_p does.

theorem TauCeti.finite_continuousCohomology_iff_finite_cohomFp_of_natCard_eq {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Fact (Nat.Prime p)] (A : Type u) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] (hA : Nat.card A = p) (htriv : ∀ (g : G) (a : A), g • a = a) (n : ℕ) : Finite ↑(continuousCohomology n (ofDiscreteModule ℤ G A)).toModuleCat ↔ Finite ↑(cohomFp p G n).toModuleCat

The cohomology of a trivial discrete G-module of prime order p is finite exactly when that of 𝔽_p is.

theorem TauCeti.CohomologicalDimensionLE.subsingleton_cohomFp {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {n : ℕ} (h : CohomologicalDimensionLE p G n) {m : ℕ} (hm : n < m) : Subsingleton ↑(cohomFp p G m).toModuleCat

If Hⁱ(G, M) vanishes for every i > n and every discrete p-primary torsion G-module M, then Hᵐ(G, 𝔽_p) vanishes for every m > n.

theorem TauCeti.subsingleton_cohomFp_of_cohomologicalDimensionAt_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {n : ℕ} (h : cohomologicalDimensionAt p G ≤ ↑n) {m : ℕ} (hm : n < m) : Subsingleton ↑(cohomFp p G m).toModuleCat

cd_p G ≤ n kills Hᵐ(G, 𝔽_p) above n.

theorem TauCeti.le_cohomologicalDimensionAt_of_nontrivial_cohomFp {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {n : ℕ} (h : Nontrivial ↑(cohomFp p G n).toModuleCat) : ↑n ≤ cohomologicalDimensionAt p G

A nonvanishing Hⁿ(G, 𝔽_p) bounds cd_p G from below: n ≤ cd_p G.