Local separation from a closed subgroup

Let K be a closed subgroup of a finite-dimensional Lie group, and let M be a linear subspace of its Lie algebra which is disjoint from lieSubalgebraOfSubgroup K. Then the only sufficiently small X ∈ M whose exponential lies in K is 0.

This is the local-separation input for the subgroup chart: when M is a complement of lieSubalgebraOfSubgroup K, it forces the transverse coordinate of nearby points of K to vanish.

Main result

• TauCeti.Lie.exists_pos_forall_norm_lt_lieExp_mem_iff_eq_zero_of_disjoint: exponential membership near zero characterizes the zero vector on any subspace disjoint from the subgroup Lie algebra.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Theorem 20.12.

theorem TauCeti.Lie.exists_pos_forall_norm_lt_lieExp_mem_iff_eq_zero_of_disjoint {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 := ⋯; ∀ (M : Submodule ℝ (LeftInvariantDerivation I G)), Disjoint M (lieSubalgebraOfSubgroup K).toSubmodule → ∃ ε > 0, ∀ X ∈ M, ‖X‖ < ε → (lieExp X ∈ K ↔ X = 0)

Let K be a closed subgroup and M a linear subspace disjoint from its Lie algebra. In some positive-radius ball about zero, an element of M has exponential in K exactly when it is zero.

This needs only disjointness; in the closed-subgroup chart construction it applies in particular when M is chosen as a linear complement of lieSubalgebraOfSubgroup K.