Charted spaces on subgroup slices

An ambient chart that identifies a subgroup with the coordinate slice F × {0} can first be translated from the identity to any subgroup point and then restricted to the subgroup subtype with values in F. These preferred charts equip the subgroup with a charted-space structure.

The construction is topological. Its atlas contains exactly the preferred charts obtained by translating the supplied identity chart; it does not by itself assert smooth compatibility, a manifold structure, or smoothness of the group operations.

Main definitions

• Subgroup.preferredSliceChart restricts the translated identity chart at a subgroup point.
• Subgroup.chartedSpaceOfIsSliceChart equips a subgroup with the resulting charted-space 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.

noncomputable def Subgroup.preferredSliceChart {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 : ↥K) : OpenPartialHomeomorph (↥K) F

The preferred subgroup chart at g, obtained by translating the given slice chart by g and then restricting it to the subgroup.

Equations

• K.preferredSliceChart e he g = ⋯.subtypeChart

@[simp]

theorem Subgroup.preferredSliceChart_source {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 : ↥K) : (K.preferredSliceChart e he g).source = Subtype.val ⁻¹' ((Homeomorph.smul ↑g).symm.transOpenPartialHomeomorph e).source

The preferred subgroup chart at g sees exactly the subgroup points in the source of its translated ambient chart.

@[simp]

theorem Subgroup.preferredSliceChart_target {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 : ↥K) : (K.preferredSliceChart e he g).target = (fun (y : F) => (y, 0)) ⁻¹' e.target

The target of a preferred subgroup chart is the zero-slice part of the original ambient target.

@[simp]

theorem Subgroup.preferredSliceChart_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 x : ↥K) : ↑(K.preferredSliceChart e he g) x = (↑e ((↑g)⁻¹ * ↑x)).1

A preferred subgroup chart first translates its argument back to the identity and then reads the tangential coordinate of the original ambient chart.

theorem Subgroup.preferredSliceChart_mk_zero_eq {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 : ↥K) {x : ↥K} (hx : x ∈ (K.preferredSliceChart e he g).source) : (↑(K.preferredSliceChart e he g) x, 0) = ↑e ((↑g)⁻¹ * ↑x)

On its source, a preferred subgroup chart recovers the translated ambient coordinates by reinserting the zero transverse coordinate.

@[simp]

theorem Subgroup.coe_preferredSliceChart_symm_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 : ↥K) {y : F} (hy : (y, 0) ∈ e.target) : ↑(↑(K.preferredSliceChart e he g).symm y) = ↑g * ↑e.symm (y, 0)

On its target, the inverse of a preferred subgroup chart applies the original ambient inverse on the zero slice and then translates by the chart's base point.

@[instance_reducible]

noncomputable def Subgroup.chartedSpaceOfIsSliceChart {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) (h1 : 1 ∈ e.source) : ChartedSpace F ↥K

One zero-slice chart around the identity equips a subgroup with a charted-space structure.

The atlas is exactly the range of the preferred charts obtained by translating the supplied identity chart.

Equations

• K.chartedSpaceOfIsSliceChart e he h1 = { atlas := Set.range (K.preferredSliceChart e he), chartAt := K.preferredSliceChart e he, mem_chart_source := ⋯, chart_mem_atlas := ⋯ }

@[simp]

theorem Subgroup.chartedSpaceOfIsSliceChart_atlas {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) (h1 : 1 ∈ e.source) : atlas F ↥K = Set.range (K.preferredSliceChart e he)

The atlas of chartedSpaceOfIsSliceChart is exactly the range of its preferred translated slice charts.

@[simp]

theorem Subgroup.chartedSpaceOfIsSliceChart_chartAt {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) (h1 : 1 ∈ e.source) (g : ↥K) : chartAt F g = K.preferredSliceChart e he g

The preferred chart installed by chartedSpaceOfIsSliceChart is the translated slice chart at the given subgroup point.