Local diffeomorphisms and group homomorphisms #
For a group homomorphism, being a local diffeomorphism at one point implies being a local diffeomorphism everywhere. Only smoothness of individual translations is needed; neither finite dimensionality nor smooth inversion is required. This lets an inverse function theorem at the identity supply local inverses throughout a Lie group.
theorem
MonoidHom.isLocalDiffeomorph_iff_isLocalDiffeomorphAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{G : Type u_6}
[Group G]
[TopologicalSpace G]
[ChartedSpace H G]
{G' : Type u_7}
[Group G']
[TopologicalSpace G']
[ChartedSpace H' G']
{n : WithTop ℕ∞}
[ContMDiffConstSMul I n G G]
[ContMDiffConstSMul I' n G' G']
(f : G →* G')
(a : G)
:
A group homomorphism is a local diffeomorphism everywhere if and only if it is one at any chosen point. Smoothness of individual left translations suffices.