Continuous homomorphisms of Lie groups are smooth

Every continuous group homomorphism f : G → G' between finite-dimensional real Lie groups is smooth. Consequently a Lie-group homomorphism may be specified as a continuous homomorphism, and the Lie functor lieMap applies to every continuous homomorphism.

The argument

For a left-invariant derivation X of G, the composite t ↦ f (lieExp (t • X)) is a continuous one-parameter subgroup of G', so by the classification of continuous one-parameter subgroups it is t ↦ lieExp (t • L X) for a unique left-invariant derivation L X of G'. Uniqueness makes L homogeneous, and the Trotter product formula

lieExp (t • (X + Y)) = lim (lieExp ((t / n) • X) * lieExp ((t / n) • Y)) ^ n,

which f preserves because it is a continuous homomorphism, makes it additive. So L is linear between finite-dimensional spaces, hence smooth, and f (lieExp X) = lieExp (L X). Near the identity f = lieExp ∘ L ∘ lieLog, so f is smooth at the identity, and a homomorphism smooth at one point is smooth everywhere by translation (TauCeti.contMDiff_of_contMDiffAt_mulHom).

The linear map L is not exposed: once f is known to be smooth, it is the differential lieMap of the bundled smooth homomorphism, characterized by map_lieExp.

Main results

• TauCeti.Lie.contMDiff_of_continuous_monoidHom: automatic smoothness. A continuous homomorphism between finite-dimensional real Lie groups is smooth.
• ContinuousMonoidHom.toContMDiffMonoidMorphism: a continuous homomorphism of such Lie groups, bundled as a smooth monoid morphism.

References

• B. C. Hall, Lie Groups, Lie Algebras, and Representations, 2nd ed., Springer GTM 222 (2015), Chapter 3: a continuous homomorphism of matrix Lie groups intertwines the exponentials through a linear map, proved with one-parameter subgroups and the Lie product formula.

theorem TauCeti.Lie.contMDiff_of_continuous_monoidHom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {G' : Type u_6} [TopologicalSpace G'] [ChartedSpace H' G'] [Group G'] [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] [LieGroup I (↑⊤) G] [LieGroup I' (↑⊤) G'] {F : Type u_7} [FunLike F G G'] [MonoidHomClass F G G'] (f : F) (hf : Continuous ⇑f) : ContMDiff I I' ↑⊤ ⇑f

Automatic smoothness. A continuous homomorphism between finite-dimensional real Lie groups is smooth. Near the identity it is lieExp ∘ L ∘ lieLog for the linear map L sending a left-invariant derivation X to the generator of the one-parameter subgroup t ↦ f (lieExp (t • X)).

def ContinuousMonoidHom.toContMDiffMonoidMorphism {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') {G' : Type u_6} [TopologicalSpace G'] [ChartedSpace H' G'] [Group G'] [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] [LieGroup I (↑⊤) G] [LieGroup I' (↑⊤) G'] (f : G →ₜ* G') : ContMDiffMonoidMorphism I I' (↑⊤) G G'

A continuous homomorphism between finite-dimensional real Lie groups, as a smooth monoid morphism (TauCeti.Lie.contMDiff_of_continuous_monoidHom).

@[simp]

theorem ContinuousMonoidHom.coe_toContMDiffMonoidMorphism {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [TopologicalSpace G] [ChartedSpace H G] [Group G] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {G' : Type u_6} [TopologicalSpace G'] [ChartedSpace H' G'] [Group G'] [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] [LieGroup I (↑⊤) G] [LieGroup I' (↑⊤) G'] (f : G →ₜ* G') : ⇑(toContMDiffMonoidMorphism I I' f) = ⇑f