Splitting a commutative topological group along a continuous section

Let f : G →ₜ* H be a continuous homomorphism from a commutative topological group, and let s : H →ₜ* G be a continuous homomorphic right inverse of f. Then G is isomorphic as a topological group to the product of the kernel of f with H: an element x corresponds to its kernel part x · s(f x)⁻¹ and its image f x, with inverse (k, t) ↦ k · s(t).

The kernel is given as any subgroup N with the same members as f.ker, so that a kernel with its own name can be used directly.

Main definitions

• ContinuousMulEquiv.kerProdOfRightInverse and ContinuousAddEquiv.kerProdOfRightInverse: the splitting G ≃ₜ* N × H determined by the section s.

References

• N. Bourbaki, General Topology, Chapters 1–4, Springer (1989), Chapter III (Topological groups), § 6 (Products and direct sums).

theorem MonoidHom.mul_inv_apply_mem_of_rightInverse {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (s : H →* G) (hs : Function.RightInverse ⇑s ⇑f) {N : Subgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 1) (x : G) : x * (s (f x))⁻¹ ∈ N

The kernel part x · s(f x)⁻¹ of x lies in the kernel N of f.

theorem AddMonoidHom.add_neg_apply_mem_of_rightInverse {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) (s : H →+ G) (hs : Function.RightInverse ⇑s ⇑f) {N : AddSubgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 0) (x : G) : x + -s (f x) ∈ N

The kernel part x - s(f x) of x lies in the kernel N of f.

def ContinuousMulEquiv.kerProdOfRightInverse {G : Type u_1} {H : Type u_2} [CommGroup G] [Group H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] (f : G →ₜ* H) (s : H →ₜ* G) (hs : Function.RightInverse ⇑s ⇑f) {N : Subgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 1) : G ≃ₜ* ↥N × H

Splitting along a continuous section. For a continuous homomorphism f : G →ₜ* H of a commutative topological group with a continuous homomorphic right inverse s, the map x ↦ (x · s(f x)⁻¹, f x) is an isomorphism of topological groups G ≃ₜ* N × H, where N is the kernel of f.

def ContinuousAddEquiv.kerProdOfRightInverse {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] (f : G →ₜ+ H) (s : H →ₜ+ G) (hs : Function.RightInverse ⇑s ⇑f) {N : AddSubgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 0) : G ≃ₜ+ ↥N × H

Splitting along a continuous section. For a continuous homomorphism f : G →ₜ+ H of a commutative topological additive group with a continuous homomorphic right inverse s, the map x ↦ (x - s(f x), f x) is an isomorphism of topological additive groups G ≃ₜ+ N × H, where N is the kernel of f.

@[simp]

theorem ContinuousMulEquiv.coe_kerProdOfRightInverse_apply_fst {G : Type u_1} {H : Type u_2} [CommGroup G] [Group H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] (f : G →ₜ* H) (s : H →ₜ* G) (hs : Function.RightInverse ⇑s ⇑f) {N : Subgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 1) (x : G) : ↑((kerProdOfRightInverse f s hs hN) x).1 = x * (s (f x))⁻¹

The kernel component of the splitting is x · s(f x)⁻¹.

@[simp]

theorem ContinuousAddEquiv.coe_kerProdOfRightInverse_apply_fst {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] (f : G →ₜ+ H) (s : H →ₜ+ G) (hs : Function.RightInverse ⇑s ⇑f) {N : AddSubgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 0) (x : G) : ↑((kerProdOfRightInverse f s hs hN) x).1 = x + -s (f x)

The kernel component of the splitting is x - s(f x).

@[simp]

theorem ContinuousMulEquiv.kerProdOfRightInverse_apply_snd {G : Type u_1} {H : Type u_2} [CommGroup G] [Group H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] (f : G →ₜ* H) (s : H →ₜ* G) (hs : Function.RightInverse ⇑s ⇑f) {N : Subgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 1) (x : G) : ((kerProdOfRightInverse f s hs hN) x).2 = f x

The second component of the splitting is f.

@[simp]

theorem ContinuousAddEquiv.kerProdOfRightInverse_apply_snd {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] (f : G →ₜ+ H) (s : H →ₜ+ G) (hs : Function.RightInverse ⇑s ⇑f) {N : AddSubgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 0) (x : G) : ((kerProdOfRightInverse f s hs hN) x).2 = f x

The second component of the splitting is f.

@[simp]

theorem ContinuousMulEquiv.kerProdOfRightInverse_symm_apply {G : Type u_1} {H : Type u_2} [CommGroup G] [Group H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalGroup G] (f : G →ₜ* H) (s : H →ₜ* G) (hs : Function.RightInverse ⇑s ⇑f) {N : Subgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 1) (p : ↥N × H) : (kerProdOfRightInverse f s hs hN).symm p = ↑p.1 * s p.2

The inverse of the splitting multiplies a kernel element by the section.

@[simp]

theorem ContinuousAddEquiv.kerProdOfRightInverse_symm_apply {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddGroup H] [TopologicalSpace G] [TopologicalSpace H] [IsTopologicalAddGroup G] (f : G →ₜ+ H) (s : H →ₜ+ G) (hs : Function.RightInverse ⇑s ⇑f) {N : AddSubgroup G} (hN : ∀ (x : G), x ∈ N ↔ f x = 0) (p : ↥N × H) : (kerProdOfRightInverse f s hs hN).symm p = ↑p.1 + s p.2

The inverse of the splitting adds a kernel element to the section.