Recognizing smooth homomorphisms through the exponential #
A group homomorphism between finite-dimensional real Lie groups is smooth if it intertwines exponential maps through a linear map of their Lie algebras. No continuity or connectedness assumption is needed. This criterion recognizes homomorphisms between intrinsic immersed subgroup presentations from the linear maps between their Lie algebras.
Main results #
TauCeti.Lie.contMDiff_of_map_lieExp: exponential intertwining implies smoothness.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer (2013), Proposition 20.8(a, f), pp.519–521, for smoothness of the exponential and its local smooth inverse.
theorem
TauCeti.Lie.contMDiff_of_map_lieExp
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I (↑⊤) G]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[FiniteDimensional ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{G' : Type u_6}
[TopologicalSpace G']
[ChartedSpace H' G']
[Group G']
[LieGroup I' (↑⊤) G']
{F : Type u_7}
[FunLike F G G']
[MonoidHomClass F G G']
(f : F)
(L : LeftInvariantDerivation I G →ₗ[ℝ] LeftInvariantDerivation I' G')
(h :
have x := ⋯;
have x_1 := ⋯;
∀ (X : LeftInvariantDerivation I G), f (lieExp X) = lieExp (L X))
:
A group homomorphism intertwining the exponential maps through a linear map of Lie algebras is smooth. Continuity of the homomorphism is not required.