Cohomological dimension at most one is projectivity

A profinite group G with cd_p G ≤ 1 has vanishing H²(G, M) for every finite discrete G-module M killed by p, since such an M is p-primary torsion. Through the cohomological obstruction to a finite embedding problem, every finite embedding problem for G with elementary abelian p-kernel is therefore solvable; climbing the lower p-central series of a finite p-group kernel extends this to p-group kernels, and the inverse-limit assembly of compatible finite solutions makes G projective: every continuous homomorphism into a quotient of a profinite pro-p group lifts continuously.

Conversely, a projective pro-p group has vanishing H² on every finite discrete p-primary module, because every profinite extension of it by such a module splits (TauCeti.IsProjective.subsingleton_continuousCohomology_two_of_isPPrimaryTorsion), and the p-cohomological dimension of a compact group is detected in degree two on finite coefficients (TauCeti.cohomologicalDimensionLE_iff_forall_finite_subsingleton_succ). So for a pro-p group projectivity and cd_p ≤ 1 are the same condition.

This is the cohomological half of Serre's theorem that a pro-p group with cd_p ≤ 1 is free pro-p, proved in TauCeti.Topology.Algebra.Group.Profinite.Free.Serre at finite rank and in TauCeti.Topology.Algebra.Group.Profinite.Free.Pointed.Serre at arbitrary rank.

Main results

• TauCeti.CohomologicalDimensionLE.hasElementaryAbelianSolutions: cd_p G ≤ 1 solves the finite embedding problems with elementary abelian p-kernel.
• TauCeti.CohomologicalDimensionLE.isProjective: cd_p G ≤ 1 makes G projective.
• TauCeti.IsProjective.cohomologicalDimensionLE_one, TauCeti.IsProjective.cohomologicalDimensionAt_le_one: a projective pro-p group has cd_p G ≤ 1.
• TauCeti.IsProP.isProjective_iff_cohomologicalDimensionLE_one, TauCeti.IsProP.isProjective_iff_cohomologicalDimensionAt_le_one: a pro-p group is projective if and only if cd_p G ≤ 1.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §3.4 and §5.9.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. III, §5.

From cd_p G ≤ 1 to projectivity

theorem TauCeti.CohomologicalDimensionLE.hasElementaryAbelianSolutions {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (h : CohomologicalDimensionLE p G 1) : HasElementaryAbelianSolutions p G

A profinite group with cd_p G ≤ 1 solves every finite embedding problem whose kernel is commutative and killed by p, such a kernel being a finite discrete p-primary torsion module.

theorem TauCeti.CohomologicalDimensionLE.isProjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)] (h : CohomologicalDimensionLE p G 1) : IsProjective p G

Cohomological dimension at most one gives projectivity. A profinite group with cd_p G ≤ 1 is projective: every continuous homomorphism into a quotient of a profinite pro-p group lifts continuously.

From projectivity to cd_p G ≤ 1

theorem TauCeti.IsProjective.cohomologicalDimensionLE_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : p ≠ 0) (hproj : IsProjective p G) (hG : IsProP p G) : CohomologicalDimensionLE p G 1

A projective pro-p group has cd_p ≤ 1, as the vanishing predicate: for p ≠ 0, Hⁱ(G, M) vanishes for every i ≥ 2 and every discrete p-primary torsion G-module M.

theorem TauCeti.IsProjective.cohomologicalDimensionAt_le_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hp : p ≠ 0) (hproj : IsProjective p G) (hG : IsProP p G) : cohomologicalDimensionAt p G ≤ 1

A projective pro-p group has cohomological dimension at most one: cd_p G ≤ 1 for a projective pro-p group G and p ≠ 0.

theorem TauCeti.IsProP.isProjective_iff_cohomologicalDimensionLE_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)] (hG : IsProP p G) : IsProjective p G ↔ CohomologicalDimensionLE p G 1

A pro-p group is projective if and only if cd_p G ≤ 1, as the vanishing predicate.

theorem TauCeti.IsProP.isProjective_iff_cohomologicalDimensionAt_le_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Fact (Nat.Prime p)] (hG : IsProP p G) : IsProjective p G ↔ cohomologicalDimensionAt p G ≤ 1

A pro-p group is projective if and only if cd_p G ≤ 1.