Continuous splittings of group extensions

Let 1 → N → E → G → 1 be an extension of groups with E and G topological and continuous projection. A continuous homomorphism σ : G →ₜ* E whose composite with the projection, bundled as a continuous homomorphism, is the identity of G is a splitting of the extension, and a continuous one (GroupExtension.exists_splitting_continuous_of_comp_eq_id). Universal properties of topological groups produce continuous homomorphisms G →ₜ* E and characterize them by an equality of continuous homomorphisms out of G; this lemma turns such an equality into a continuous splitting.

Main results

• GroupExtension.exists_splitting_continuous_of_comp_eq_id: a continuous homomorphic right inverse of the projection is a continuous splitting.

theorem GroupExtension.exists_splitting_continuous_of_comp_eq_id {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [TopologicalSpace E] [Group G] [TopologicalSpace G] (S : GroupExtension N E G) (hrh : Continuous ⇑S.rightHom) (σ : G →ₜ* E) (hσ : { toMonoidHom := S.rightHom, continuous_toFun := hrh }.comp σ = ContinuousMonoidHom.id G) : ∃ (s : S.Splitting), Continuous ⇑s ∧ ∀ (g : G), s g = σ g

A continuous homomorphic right inverse of the projection splits the extension continuously. If σ : G →ₜ* E composed with the projection of 1 → N → E → G → 1, bundled with its continuity, is the identity of G, then σ is a continuous splitting of the extension.