Extensions of a projective pro-p group split

Let G be a projective pro-p group: every continuous homomorphism from G into a quotient of a profinite pro-p group lifts continuously (TauCeti.IsProjective). An extension 1 → M → E → G → 1 of topological groups with profinite total group E and pro-p kernel M has pro-p total group, so projectivity lifts the identity of G through the projection E ↠ G to a continuous homomorphic section: the extension splits (GroupExtension.exists_splitting_continuous_of_isProjective). Only the Hausdorff topological group structure of G enters; profiniteness of G is not needed.

Read through the classification of profinite extensions by continuous H², the splitting is the vanishing of H²(G, M) for every profinite pro-p abelian G-module M, proved in TauCeti.Topology.Algebra.Group.Profinite.EmbeddingProblem.Cohomology. The free pro-p groups, on a type or on a pointed profinite space, are projective, and the splitting of their extensions in TauCeti.Topology.Algebra.Group.Profinite.Free.Extension is the instance of this statement at freeProP p X.

Main results

• GroupExtension.exists_splitting_continuous_of_isProjective: every profinite extension of a projective pro-p group by a pro-p group splits by a continuous homomorphic section.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §5.9.
• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Section 7.6.

Extensions split

theorem GroupExtension.exists_splitting_continuous_of_isProjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {M : Type u_1} [Group M] [TopologicalSpace M] {E : Type v} [Group E] [TopologicalSpace E] [IsTopologicalGroup E] [CompactSpace E] [TotallyDisconnectedSpace E] (S : GroupExtension M E G) (hinl : Continuous ⇑S.inl) (hrh : Continuous ⇑S.rightHom) (hM : TauCeti.IsProP p M) (hG : TauCeti.IsProP p G) (hproj : TauCeti.IsProjective p G) : ∃ (s : S.Splitting), Continuous ⇑s

Extensions of a projective pro-p group by a pro-p group split. An extension 1 → M → E → G → 1 of topological groups with profinite total group and pro-p kernel, over a projective pro-p Hausdorff group G, has a continuous homomorphic section: the total group is pro-p, and projectivity lifts the identity of G through the projection.