Translating a subgroup slice chart

An identity-neighbourhood slice chart for a subgroup can be transported to every subgroup point by left translation. Using the topology-level ambient chart translation, this file proves that translation by a subgroup point preserves the subgroup slice.

Main result

• Subgroup.isSliceChart_smul_symm_transOpenPartialHomeomorph shows that translation preserves the subgroup slice.

The result is purely topological. It does not install a manifold structure on the subgroup or assert smoothness of the translated charts.

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.isSliceChart_smul_symm_transOpenPartialHomeomorph {G : Type u_1} {P : Type u_2} [Group G] [TopologicalSpace G] [ContinuousConstSMul G G] [TopologicalSpace P] (K : Subgroup G) (φ : OpenPartialHomeomorph G P) {S : Set P} (hφ : TauCeti.IsSliceChart φ S ↑K) (g : ↥K) : TauCeti.IsSliceChart ((Homeomorph.smul ↑g).symm.transOpenPartialHomeomorph φ) S ↑K

Translating a slice chart for a subgroup by a subgroup point preserves the subgroup slice.