Lie groups covered by local diffeomorphisms

Let π : G →* G' be a surjective group homomorphism out of a C^n Lie group G which is a C^n local diffeomorphism onto a C^n manifold G'. Then G' is a C^n Lie group. Near a pair of points of G', multiplication is the image under π of the product of two local inverses of π, which are C^n; inversion on G' is the descent of inversion on G. This covers quotients of Lie groups by discrete normal subgroups, such as tori E ⧸ L and circles AddCircle p.

The charts of a Lie group can also be pulled back along a locally homeomorphic homomorphism from a topological group, giving the source a Lie-group structure over the same model.

This file also proves that the integer power maps of a C^n Lie group are C^n.

Main results

• IsLocalDiffeomorph.lieGroup, IsLocalDiffeomorph.lieAddGroup: the image of a Lie group under a surjective homomorphism which is a local diffeomorphism is a Lie group.
• IsLocalHomeomorph.lieGroup_chartedSpaceComap, IsLocalHomeomorph.lieAddGroup_chartedSpaceComap: Lie-group structures for pulled-back charts.
• TauCeti.contMDiff_zpow, TauCeti.contMDiff_zsmul: integer powers, and integer multiples, in a Lie group are C^n.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Proposition 4.40 and Theorem 7.7.

theorem IsLocalDiffeomorph.lieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [TopologicalSpace G'] [ChartedSpace H' G'] [IsManifold I' n G'] [Group G'] (π : G →* G') (hπ : IsLocalDiffeomorph I I' n ⇑π) (hsurj : Function.Surjective ⇑π) : LieGroup I' n G'

If a surjective group homomorphism π : G →* G' out of a C^n Lie group is a C^n local diffeomorphism, then G' is a C^n Lie group.

theorem IsLocalDiffeomorph.lieAddGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I n G] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [TopologicalSpace G'] [ChartedSpace H' G'] [IsManifold I' n G'] [AddGroup G'] (π : G →+ G') (hπ : IsLocalDiffeomorph I I' n ⇑π) (hsurj : Function.Surjective ⇑π) : LieAddGroup I' n G'

If a surjective additive group homomorphism π : G →+ G' out of a C^n additive Lie group is a C^n local diffeomorphism, then G' is a C^n additive Lie group.

theorem IsLocalHomeomorph.lieGroup_chartedSpaceComap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {A : Type u_8} {B : Type u_9} [TopologicalSpace A] [Group A] [IsTopologicalGroup A] [TopologicalSpace B] [Group B] [ChartedSpace H B] [LieGroup I n B] {p : A → B} (hp : IsLocalHomeomorph p) (hmul : ∀ (x y : A), p (x * y) = p x * p y) : have x := hp.chartedSpaceComap; LieGroup I n A

Charts pulled back through a locally homeomorphic homomorphism from a topological group form a Lie-group structure over the target's model.

theorem IsLocalHomeomorph.lieAddGroup_chartedSpaceComap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {A : Type u_8} {B : Type u_9} [TopologicalSpace A] [AddGroup A] [IsTopologicalAddGroup A] [TopologicalSpace B] [AddGroup B] [ChartedSpace H B] [LieAddGroup I n B] {p : A → B} (hp : IsLocalHomeomorph p) (hadd : ∀ (x y : A), p (x + y) = p x + p y) : have x := hp.chartedSpaceComap; LieAddGroup I n A

Charts pulled back through a locally homeomorphic additive homomorphism from a topological additive group form an additive Lie-group structure over the target's model.

theorem TauCeti.contMDiff_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [LieGroup I n G] (k : ℤ) : ContMDiff I I n fun (a : G) => a ^ k

In a C^n Lie group, every integer power map is C^n.

theorem TauCeti.contMDiff_zsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G] [LieAddGroup I n G] (k : ℤ) : ContMDiff I I n fun (a : G) => k • a

In a C^n additive Lie group, multiplication by every integer is C^n.