Lie-group structures from subgroup slice charts #
A smooth ambient chart which identifies a subgroup with the zero transverse slice gives more than a smooth atlas on the subgroup: the inclusion is smooth, and smoothness of a map into the subgroup can be checked after composing with that inclusion. Consequently, the group operations inherited from an ambient Lie group are smooth for the slice-chart manifold structure.
Main results #
Subgroup.contMDiff_subtypeVal_chartedSpaceOfIsSliceChartproves that the subgroup inclusion is smooth.Subgroup.contMDiff_iff_comp_subtypeVal_chartedSpaceOfIsSliceChartcharacterizes smooth maps into the subgroup by their composites with the inclusion.Subgroup.contMDiffMul_chartedSpaceOfIsSliceChartmakes inherited multiplication smooth.Subgroup.lieGroup_chartedSpaceOfIsSliceChartequips the charted subgroup with the inherited Lie-group operations.
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.contMDiff_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']
(K : Subgroup G)
(e : OpenPartialHomeomorph G (F × F'))
(he : TauCeti.IsSliceChart e (Set.univ ×ˢ {0}) ↑K)
(h1 : 1 ∈ e.source)
(he_symm : ContMDiffOn (modelWithCornersSelf ℝ (F × F')) I n (↑e.symm) e.target)
[ContMDiffMul I n G]
:
have x := ⋯;
have x := K.chartedSpaceOfIsSliceChart e he h1;
ContMDiff (modelWithCornersSelf ℝ F) I n fun (x : ↥K) => ↑x
The inclusion of a subgroup carrying its slice-chart manifold structure into the ambient smooth group is smooth.
theorem
Subgroup.contMDiff_iff_comp_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']
(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)
[ContMDiffMul I n G]
{E₀ : Type u_6}
{H₀ : Type u_7}
{M : Type u_8}
[NormedAddCommGroup E₀]
[NormedSpace ℝ E₀]
[TopologicalSpace H₀]
{J : ModelWithCorners ℝ E₀ H₀}
[TopologicalSpace M]
[ChartedSpace H₀ M]
(f : M → ↥K)
:
have x := ⋯;
let x := K.chartedSpaceOfIsSliceChart e he h1;
have x_1 := ⋯;
ContMDiff J (modelWithCornersSelf ℝ F) n f ↔ ContMDiff J I n ((fun (x : ↥K) => ↑x) ∘ f)
A map into a subgroup with its slice-chart manifold structure is smooth exactly when its composite with the inclusion into the ambient smooth group is smooth.
theorem
Subgroup.contMDiffMul_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']
(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)
[ContMDiffMul I n G]
:
have x := ⋯;
let x := K.chartedSpaceOfIsSliceChart e he h1;
have x_1 := ⋯;
ContMDiffMul (modelWithCornersSelf ℝ F) n ↥K
Multiplication inherited by a subgroup is smooth for its slice-chart manifold structure.
theorem
Subgroup.lieGroup_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']
(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)
[LieGroup I n G]
:
have x := ⋯;
let x := K.chartedSpaceOfIsSliceChart e he h1;
have x_1 := ⋯;
LieGroup (modelWithCornersSelf ℝ F) n ↥K
A subgroup carrying the manifold structure induced by a smooth slice chart inherits the Lie-group structure of the ambient Lie group.