Smooth subgroup slice charts #
An ambient smooth chart that identifies a subgroup with a linear slice induces a smooth atlas on
the subgroup. The transition between the preferred charts at g and h is obtained by inserting
the zero transverse coordinate, applying the ambient inverse chart, translating by h⁻¹ * g, and
then reading the tangential coordinate of the ambient chart.
Main results #
Subgroup.contDiffOn_preferredSliceChart_transitionproves that transitions between preferred subgroup slice charts are smooth.Subgroup.isManifold_chartedSpaceOfIsSliceChartequips the charted subgroup with a smooth manifold structure.
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
Subgroup.preferredSliceChart_transition_apply
{G : Type u_1}
{F : Type u_2}
{F' : Type u_3}
[Group G]
[TopologicalSpace G]
[TopologicalSpace F]
[TopologicalSpace F']
[Zero F']
[ContinuousConstSMul G G]
(K : Subgroup G)
(e : OpenPartialHomeomorph G (F × F'))
(he : TauCeti.IsSliceChart e (Set.univ ×ˢ {0}) ↑K)
(g h : ↥K)
{y : F}
(hy : y ∈ ((K.preferredSliceChart e he g).symm.trans (K.preferredSliceChart e he h)).source)
:
The transition from the preferred chart at g to the preferred chart at h is the
tangential coordinate of ambient translation by h⁻¹ * g, restricted to the zero transverse
slice.
theorem
Subgroup.contDiffOn_preferredSliceChart_transition
{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)
(he' : ContMDiffOn I (modelWithCornersSelf ℝ (F × F')) n (↑e) e.source)
(he_symm : ContMDiffOn (modelWithCornersSelf ℝ (F × F')) I n (↑e.symm) e.target)
(g h : ↥K)
:
have x := ⋯;
ContDiffOn ℝ n (↑((K.preferredSliceChart e he g).symm.trans (K.preferredSliceChart e he h)))
((K.preferredSliceChart e he g).symm.trans (K.preferredSliceChart e he h)).source
Transitions between preferred subgroup slice charts are smooth when the ambient slice chart and its inverse are smooth.
theorem
Subgroup.isManifold_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)
:
have x := ⋯;
have x := K.chartedSpaceOfIsSliceChart e he h1;
IsManifold (modelWithCornersSelf ℝ F) n ↥K
The preferred charts induced by a smooth ambient slice chart make the subgroup a smooth manifold.