A limit criterion for the Lie algebra of a closed subgroup

Let K be a closed subgroup of a finite-dimensional Lie group. Its Lie algebra consists exactly of the limits X for which there are eventually positive real numbers tₙ → 0 and derivations Xₙ → X such that, eventually,

lieExp (tₙ • Xₙ) ∈ K.

This is the limit criterion used in the local-separation step of the closed-subgroup theorem. In that application, a hypothetical sequence of nonzero transverse coordinates Yₙ → 0 is written as

Yₙ = ‖Yₙ‖ • (‖Yₙ‖⁻¹ • Yₙ).

A convergent subsequence of the normalized directions therefore satisfies the criterion below, forcing its limit into the subgroup Lie algebra and contradicting transversality.

Main results

• TauCeti.Lie.mem_lieSubalgebraOfSubgroup_of_seq: a convergent sequence of rescaled infinitesimal elements whose exponentials lie in a closed subgroup has its limit in the subgroup Lie algebra.
• TauCeti.Lie.mem_lieSubalgebraOfSubgroup_iff_exists_seq: the resulting sequential characterization.

References

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

theorem TauCeti.Lie.mem_lieSubalgebraOfSubgroup_of_seq {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 : Subgroup G} (hK : IsClosed ↑K) {X : LeftInvariantDerivation I G} {t : ℕ → ℝ} (ht_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < t n) (ht : Filter.Tendsto t Filter.atTop (nhds 0)) {Xn : ℕ → LeftInvariantDerivation I G} (hXn : Filter.Tendsto Xn Filter.atTop (nhds X)) (hmem : ∀ᶠ (n : ℕ) in Filter.atTop, lieExp (t n • Xn n) ∈ K) : X ∈ lieSubalgebraOfSubgroup K

A limit criterion for the Lie algebra of a closed subgroup. Suppose eventually positive scales tₙ tend to zero, derivations Xₙ tend to X, and eventually lieExp (tₙ • Xₙ) lies in K. Then X belongs to the Lie algebra of K.

theorem TauCeti.Lie.mem_lieSubalgebraOfSubgroup_iff_exists_seq {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 : Subgroup G} (hK : IsClosed ↑K) {X : LeftInvariantDerivation I G} : X ∈ lieSubalgebraOfSubgroup K ↔ ∃ (t : ℕ → ℝ) (Xn : ℕ → LeftInvariantDerivation I G), (∀ᶠ (n : ℕ) in Filter.atTop, 0 < t n) ∧ Filter.Tendsto t Filter.atTop (nhds 0) ∧ Filter.Tendsto Xn Filter.atTop (nhds X) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, lieExp (t n • Xn n) ∈ K

Membership in the Lie algebra of a closed subgroup is equivalent to being a limit of derivations whose exponentials at eventually positive scales tending to zero eventually lie in the subgroup.