Connectedness of topological groups

This file derives connectedness of a group from preconnectedness of a subgroup and its coset quotient, and develops the identity component Subgroup.connectedComponentOfOne G of a topological group G: it is a closed normal subgroup, it lies in every open subgroup, continuous homomorphisms preserve it, a continuous homomorphism from a connected group with open range is onto it, and the quotient of G by it is totally disconnected. Thus a group whose quotient by its identity component is compact is an extension of a profinite group by a connected one.

Main results

• Subgroup.connectedSpace_of_quotient: a group with continuous left translations is connected when a subgroup and the corresponding coset quotient are preconnected.
• Subgroup.connectedComponentOfOne_le_of_isOpen: an open subgroup contains the identity component.
• Subgroup.closure_eq_connectedComponentOfOne_of_mem_nhds_one_of_subset: a neighbourhood of 1 inside the identity component generates it.
• Subgroup.closure_eq_top_of_mem_nhds_one: a preconnected topological group is generated by any neighbourhood of 1.
• Subgroup.map_connectedComponentOfOne_le: a continuous homomorphism maps the identity component into the identity component.
• MonoidHom.range_eq_connectedComponentOfOne: a continuous homomorphism with open range, whose kernel and the identity component of its source generate the source, is onto the identity component of its target.
• ContinuousMulEquiv.map_connectedComponentOfOne: a continuous multiplicative equivalence maps the identity component onto the identity component.
• QuotientGroup.totallyDisconnectedSpace_connectedComponentOfOne: the quotient of a topological group by its identity component is totally disconnected.

References

• E. Hewitt and K. A. Ross, Abstract Harmonic Analysis I, Theorem 7.3.
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Proposition 7.14 (a connected Lie group is generated by any neighbourhood of the identity; the argument is purely topological).

theorem Subgroup.connectedSpace_of_quotient {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousConstSMul G G] (H : Subgroup G) [PreconnectedSpace ↥H] [PreconnectedSpace (G ⧸ H)] : ConnectedSpace G

A group with continuous left translations is connected when a subgroup and its coset quotient are preconnected.

@[simp]

theorem Subgroup.coe_connectedComponentOfOne {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ↑(connectedComponentOfOne G) = connectedComponent 1

The underlying set of the identity component is the connected component of 1.

@[simp]

theorem Subgroup.mem_connectedComponentOfOne_iff {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G} : g ∈ connectedComponentOfOne G ↔ g ∈ connectedComponent 1

An element lies in the identity component exactly when it lies in the connected component of 1.

instance Subgroup.isClosed_connectedComponentOfOne {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed ↑(connectedComponentOfOne G)

The identity component of a topological group is closed.

instance Subgroup.normal_connectedComponentOfOne {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (connectedComponentOfOne G).Normal

The identity component of a topological group is normal.

theorem Subgroup.connectedComponentOfOne_le_of_isOpen {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} (hH : IsOpen ↑H) : connectedComponentOfOne G ≤ H

An open subgroup of a topological group contains the identity component.

@[simp]

theorem Subgroup.connectedComponentOfOne_eq_top {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [PreconnectedSpace G] : connectedComponentOfOne G = ⊤

In a preconnected topological group the identity component is the whole group.

theorem Subgroup.connectedComponentOfOne_le_of_mem_nhds_one {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Subgroup G} (hH : ↑H ∈ nhds 1) : connectedComponentOfOne G ≤ H

A subgroup that is a neighbourhood of 1 contains the identity component.

theorem Subgroup.closure_eq_connectedComponentOfOne_of_mem_nhds_one_of_subset {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Set G} (hs : s ∈ nhds 1) (hsub : s ⊆ ↑(connectedComponentOfOne G)) : closure s = connectedComponentOfOne G

A neighbourhood of 1 contained in the identity component generates the identity component.

theorem Subgroup.closure_eq_top_of_mem_nhds_one {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [PreconnectedSpace G] {s : Set G} (hs : s ∈ nhds 1) : closure s = ⊤

A preconnected topological group is generated by any neighbourhood of 1.

theorem Subgroup.map_connectedComponentOfOne_le {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {G' : Type u_3} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] {f : G →* G'} (hf : Continuous ⇑f) : map f (connectedComponentOfOne G) ≤ connectedComponentOfOne G'

A continuous homomorphism maps the identity component into the identity component.

theorem MonoidHom.range_eq_connectedComponentOfOne {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {G' : Type u_3} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] {f : G →* G'} (hf : Continuous ⇑f) (hopen : IsOpen ↑f.range) (hgen : Subgroup.connectedComponentOfOne G ⊔ f.ker = ⊤) : f.range = Subgroup.connectedComponentOfOne G'

A continuous homomorphism with open range is onto the identity component of its target, provided its kernel and the identity component of its source generate the source. The latter holds, for instance, when the source is connected.

theorem ContinuousMulEquiv.map_connectedComponentOfOne {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {G' : Type u_3} [Group G'] [TopologicalSpace G'] [IsTopologicalGroup G'] (e : G ≃ₜ* G') : Subgroup.map e.toMonoidHom (Subgroup.connectedComponentOfOne G) = Subgroup.connectedComponentOfOne G'

A continuous multiplicative equivalence maps identity components onto each other.

instance QuotientGroup.totallyDisconnectedSpace_connectedComponentOfOne {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : TotallyDisconnectedSpace (G ⧸ Subgroup.connectedComponentOfOne G)

The quotient of a topological group by its identity component is totally disconnected.