The local Cartan chart of a closed subgroup

For a closed subgroup K of a finite-dimensional Lie group, this file gives a neighborhood of the identity on which membership in K is equivalent to being the exponential of an element of lieSubalgebraOfSubgroup K. This local characterization is the membership criterion used by the embedded Lie-subgroup chart.

Main result

• The local characterization theorem below: a closed subgroup is locally the exponential image of its Lie algebra.

• TauCeti.Lie.isOpen_subgroupOf_of_lieSubalgebraOfSubgroup_le: a closed subgroup of a closed subgroup K whose Lie algebra contains that of K is open in K.

• TauCeti.Lie.le_of_lieSubalgebraOfSubgroup_le: a closed connected subgroup lies in any closed subgroup whose Lie algebra contains its own.

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_complement_data_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)) (ε : ℝ), IsCompl (lieSubalgebraOfSubgroup K).toSubmodule q ∧ 0 < ε ∧ (∀ X ∈ q, ‖X‖ < ε → (lieExp X ∈ K ↔ X = 0)) ∧ IsLocalDiffeomorphAt (modelWithCornersSelf ℝ (↥(lieSubalgebraOfSubgroup K).toSubmodule × ↥q)) I (↑⊤) ((lieSubalgebraOfSubgroup K).lieExpMulLieExp q) 0

For a closed subgroup, there are a complementary submodule and positive radius such that small transverse exponentials lie in the subgroup exactly at zero, while the complementary exponential product is a local diffeomorphism at the identity.

theorem TauCeti.Lie.exists_mem_nhds_one_iff_exists_mem_lieSubalgebraOfSubgroup_and_lieExp_eq_of_isClosed {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 := ⋯; ∃ U ∈ nhds 1, ∀ x_1 ∈ U, x_1 ∈ K ↔ ∃ X ∈ lieSubalgebraOfSubgroup K, lieExp X = x_1

Near the identity, a closed subgroup is exactly the exponential image of its Lie algebra. This is the local membership criterion for the embedded Lie-subgroup chart.

theorem TauCeti.Lie.isOpen_subgroupOf_of_lieSubalgebraOfSubgroup_le {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] {T K : Subgroup G} (hT : IsClosed ↑T) (hK : IsClosed ↑K) (h : lieSubalgebraOfSubgroup K ≤ lieSubalgebraOfSubgroup T) : IsOpen ↑(T.subgroupOf K)

A closed subgroup T whose Lie algebra contains that of a closed subgroup K is open in K: T ∩ K is an open subgroup of K.

theorem TauCeti.Lie.le_of_lieSubalgebraOfSubgroup_le {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] {K L : Subgroup G} (hK : IsClosed ↑K) (hconn : IsPreconnected ↑K) (hL : IsClosed ↑L) (h : lieSubalgebraOfSubgroup K ≤ lieSubalgebraOfSubgroup L) : K ≤ L

A closed connected subgroup lies in any closed subgroup containing its Lie algebra.