The differential of a slice-chart subgroup inclusion

A smooth ambient chart identifying a subgroup with the zero transverse slice makes the subgroup inclusion smooth. This file records that the inclusion is moreover an immersion in the sense of differentials: at every point its differential admits a continuous left inverse, hence is injective.

The reason is that the inclusion has a smooth left inverse in charts. The preferred chart of the subgroup at g is the tangential coordinate x ↦ (e (g⁻¹ * x)).1 of the translated ambient chart, and that same formula is a smooth function on a neighbourhood of g in the ambient group. Composing it with the inclusion returns the subgroup chart itself, whose differential at its own base point is the identity, so the differential of the ambient tangential coordinate splits the differential of the inclusion.

Since the subgroup carries its subspace topology, the inclusion is also a topological embedding, so together these say the inclusion is an embedding of smooth manifolds. What is recorded here is the differential form of being an immersion, IsDiffImmersionAt; the chart form, Manifold.IsImmersion, which asks for charts of the subgroup and of the ambient group in which the inclusion reads as u ↦ (u, 0), is not derived from it.

Main result

• Subgroup.isDiffImmersionAt_subtypeVal_chartedSpaceOfIsSliceChart: the differential of the subgroup inclusion has a continuous left inverse at every point.

References

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

theorem Subgroup.isDiffImmersionAt_subtypeVal_chartedSpaceOfIsSliceChart {E : Type u_1} {H : Type u_2} {G : Type u_3} {F : Type u_4} {F' : Type u_5} {n : WithTop ℕ∞} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace G] [ChartedSpace H G] [Group G] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup F'] [NormedSpace ℝ F'] [ContMDiffMul I n G] (K : Subgroup G) (e : OpenPartialHomeomorph G (F × F')) (he : TauCeti.IsSliceChart e (Set.univ ×ˢ {0}) ↑K) (h1 : 1 ∈ e.source) (he' : ContMDiffOn I (modelWithCornersSelf ℝ (F × F')) n (↑e) e.source) (he_symm : ContMDiffOn (modelWithCornersSelf ℝ (F × F')) I n (↑e.symm) e.target) (hn : 1 ≤ n) (k : ↥K) : have x := ⋯; have x := K.chartedSpaceOfIsSliceChart e he h1; IsDiffImmersionAt (modelWithCornersSelf ℝ F) I (fun (x : ↥K) => ↑x) k

The inclusion of a subgroup carrying its slice-chart manifold structure into the ambient smooth group is an immersion in the sense of differentials: its differential at each point has a continuous left inverse, and so is injective.