The differential at the identity of a group homomorphism

A group homomorphism φ : K →* G between groups modelled on manifolds has a differential at the identity dφ : Lie(K) → Lie(G), a continuous linear map between the tangent Lie algebras. This file names that map and proves its functor laws: the identity homomorphism has identity differential, and the chain rule holds at the identity for homomorphisms differentiable there.

Main definitions

• MonoidHom.groupLieAlgebraMap: the differential at the identity of a group homomorphism, as a continuous linear map between tangent Lie algebras.

Main results

• MonoidHom.groupLieAlgebraMap_id: the differential of the identity is the identity.
• MonoidHom.groupLieAlgebraMap_comp: the chain rule at the identity.

noncomputable def MonoidHom.groupLieAlgebraMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] {F : Type u_5} {HK : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace HK] {K : Type u_7} [TopologicalSpace K] [ChartedSpace HK K] [Group K] (φ : K →* G) (J : ModelWithCorners 𝕜 F HK) (I : ModelWithCorners 𝕜 E H) : GroupLieAlgebra J K →L[𝕜] GroupLieAlgebra I G

The differential dφ : Lie(K) → Lie(G) at the identity of a group homomorphism φ : K →* G, as a continuous linear map between the tangent Lie algebras. It is zero when φ is not differentiable at the identity.

theorem MonoidHom.groupLieAlgebraMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} {HK : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace HK] {K : Type u_7} [TopologicalSpace K] [ChartedSpace HK K] [Group K] (φ : K →* G) (J : ModelWithCorners 𝕜 F HK) (ξ : GroupLieAlgebra J K) : (φ.groupLieAlgebraMap J I) ξ = (mfderiv% ⇑φ 1) ξ

The differential at the identity of φ, applied to ξ.

@[simp]

theorem MonoidHom.groupLieAlgebraMap_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] : (id G).groupLieAlgebraMap I I = ContinuousLinearMap.id 𝕜 (GroupLieAlgebra I G)

The differential of the identity homomorphism is the identity.

theorem MonoidHom.groupLieAlgebraMap_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {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] {F : Type u_5} {HK : Type u_6} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace HK] {K : Type u_7} [TopologicalSpace K] [ChartedSpace HK K] [Group K] {F' : Type u_8} {HK' : Type u_9} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [TopologicalSpace HK'] {J' : ModelWithCorners 𝕜 F' HK'} {K' : Type u_10} [TopologicalSpace K'] [ChartedSpace HK' K'] [Group K'] {J : ModelWithCorners 𝕜 F HK} (ψ : K →* G) (φ : K' →* K) (hψ : MDiffAt ⇑ψ 1) (hφ : MDiffAt ⇑φ 1) : (ψ.comp φ).groupLieAlgebraMap J' I = ψ.groupLieAlgebraMap J I ∘SL φ.groupLieAlgebraMap J' J

The chain rule at the identity. The differential of a composite of homomorphisms that are differentiable at the identity is the composite of their differentials.