The identity slice chart of a closed subgroup

For a closed subgroup of a finite-dimensional Lie group, the complementary exponential-product map is a local chart at the identity. The local Cartan membership criterion and the transverse separation lemma identify the subgroup in this chart with the zero-complement slice, whose tangential factor is the Lie algebra that TauCeti.Lie.lieSubalgebraOfSubgroup assigns to the subgroup. Translating this identity chart gives the corresponding local models at other subgroup points.

The complement, transverse separation radius, and local product chart are supplied by TauCeti.Lie.exists_complement_data_of_isClosed_subgroup.

Main results

• TauCeti.Lie.exists_isSliceChart_of_isClosed_subgroup packages the identity slice chart.

The resulting chart retains the smoothness of both directions of the local diffeomorphism. A separate construction installs the induced manifold structure on the subgroup subtype.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Theorem 20.12.
• H. Hilgert and K.-H. Neeb, Structure and Geometry of Lie Groups (2012), Section 9.1.

theorem TauCeti.Lie.exists_isSliceChart_of_isClosed_subgroup {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] {K : Subgroup G} (hK : IsClosed ↑K) : have x := ⋯; ∃ (q : Submodule ℝ (LeftInvariantDerivation I G)) (Φ : OpenPartialHomeomorph G (↥(lieSubalgebraOfSubgroup K).toSubmodule × ↥q)), IsCompl (lieSubalgebraOfSubgroup K).toSubmodule q ∧ 1 ∈ Φ.source ∧ IsSliceChart Φ (Set.univ ×ˢ {0}) ↑K ∧ ContMDiffOn I (modelWithCornersSelf ℝ (↥(lieSubalgebraOfSubgroup K).toSubmodule × ↥q)) (↑⊤) (↑Φ) Φ.source ∧ ContMDiffOn (modelWithCornersSelf ℝ (↥(lieSubalgebraOfSubgroup K).toSubmodule × ↥q)) I (↑⊤) (↑Φ.symm) Φ.target

A closed subgroup is the zero-complement slice in a smooth complementary exponential chart at 1, the tangential factor of the chart being its Lie algebra.