Generation of a Lie group by its exponential image

The exponential image of a finite-dimensional real Lie group is a neighbourhood of the identity, and every value of the exponential lies on a one-parameter subgroup, hence in the identity component. Since a neighbourhood of the identity generates the identity component, the subgroup generated by the exponential image is exactly the identity component, and it is the whole group when the group is preconnected.

Main results

• lieExp_mem_connectedComponent_one: the exponential takes values in the connected component of the identity.
• range_lieExp_mem_nhds_one: the exponential image is a neighbourhood of the identity.
• closure_range_lieExp_eq_connectedComponentOfOne: the subgroup generated by the exponential image is the identity component.
• closure_range_lieExp_eq_top: a preconnected Lie group is generated by its exponential image.

The identity component Subgroup.connectedComponentOfOne G is only defined for a topological group, so the last two results carry [IsTopologicalGroup G] explicitly (as TauCeti/Geometry/Lie/UniversalCover.lean does); for a Lie group this instance is topologicalGroup_of_lieGroup I ∞.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Proposition 7.14 (a connected Lie group is generated by any neighbourhood of the identity) and Proposition 20.8 (properties of the exponential map).

@[simp]

theorem TauCeti.lieExp_mem_connectedComponent_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] (X : LeftInvariantDerivation I G) : lieExp X ∈ connectedComponent 1

The exponential takes values in the connected component of the identity.

theorem TauCeti.range_lieExp_mem_nhds_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : Set.range lieExp ∈ nhds 1

The exponential image is a neighbourhood of the identity.

theorem TauCeti.closure_range_lieExp_eq_connectedComponentOfOne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] [IsTopologicalGroup G] : Subgroup.closure (Set.range lieExp) = Subgroup.connectedComponentOfOne G

The identity component is generated by the exponential image.

theorem TauCeti.closure_range_lieExp_eq_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] [IsTopologicalGroup G] [PreconnectedSpace G] : Subgroup.closure (Set.range lieExp) = ⊤

A preconnected Lie group is generated by its exponential image.