The Lie functor on smooth homomorphisms #
The differential at the identity of a smooth Lie-group homomorphism induces a Lie-algebra
homomorphism between left-invariant derivations. Smooth homomorphisms carry their differentiability
proof in ContMDiffMonoidMorphism; identity and composition complete that bundled morphism API.
The resulting Lie map preserves identities and composition and is natural with respect to the
Lie-group exponential.
References #
- The exponential-naturality proof generalizes the integral-curve argument in
TauCeti.Lie.conj_mulInvariantIntegralCurveandTauCeti.Lie.conj_mulInvariantExp.
Main results #
lieMap: the Lie-algebra homomorphism induced by a smooth monoid morphism.ContMDiffMonoidMorphism.groupLieAlgebraMap_lie: the differential at the identity of a smooth homomorphism preserves the Lie bracket.lieMap_id,lieMap_comp: the identity and composition laws.map_lieExp: naturality with respect to the Lie-group exponential.continuous_lieMap: the Lie map is continuous.ContMDiffMonoidMorphism.isLocalDiffeomorph_iff_lieMap_bijectiveandContMDiffMonoidMorphism.isLocalDiffeomorph_of_lieMap_bijective: the local-diffeomorphism criterion at every point.ContMDiffMonoidMorphism.lieMap_injective_of_mfderiv_injective: injectivity of the identity differential implies injectivity of the Lie map.TauCeti.Lie.lieEquivOfIsLocalDiffeomorphAt: the Lie-algebra equivalence induced by a smooth homomorphism that is a local diffeomorphism at the identity.ContMDiffMonoidMorphism.lieMap_bijective_of_isLocalDiffeomorphAt: the Lie map of a homomorphism that is a local diffeomorphism at the identity is bijective.ContMDiffMonoidMorphism.isLocalDiffeomorphAt_of_lieMap_bijective: a smooth homomorphism with bijective Lie map is a local diffeomorphism at the identity.ContMDiffMonoidMorphism.isLocalDiffeomorphAt_iff_lieMap_bijective: the corresponding characterization.
theorem
ContMDiffMonoidMorphism.groupLieAlgebraMap_lie
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[CompleteSpace E]
[CompleteSpace E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(X Y : GroupLieAlgebra I G)
:
The differential at the identity of a smooth homomorphism preserves the Lie bracket of the tangent Lie algebras.
noncomputable def
lieMap
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
:
The Lie functor on morphisms: the differential at the identity of a smooth homomorphism.
Instances For
@[simp]
theorem
leftInvariantDerivationLieEquivGroupLieAlgebra_lieMap
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(D : LeftInvariantDerivation I G)
:
(leftInvariantDerivationLieEquivGroupLieAlgebra ⋯) ((lieMap φ) D) = (mfderiv% ⇑φ 1) ((leftInvariantDerivationLieEquivGroupLieAlgebra ⋯) D)
Under evaluation at the identity, lieMap is the manifold differential of the homomorphism.
@[simp]
theorem
lieMap_id
{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]
[LieGroup I (↑⊤) G]
[FiniteDimensional ℝ E]
:
The Lie map of the identity homomorphism is the identity Lie-algebra homomorphism.
@[simp]
theorem
lieMap_comp
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
{E'' : Type u_7}
[NormedAddCommGroup E'']
[NormedSpace ℝ E'']
{H'' : Type u_8}
[TopologicalSpace H'']
{I'' : ModelWithCorners ℝ E'' H''}
{G'' : Type u_9}
[TopologicalSpace G'']
[ChartedSpace H'' G'']
[Group G'']
[LieGroup I'' (↑⊤) G'']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
[FiniteDimensional ℝ E'']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(ψ : ContMDiffMonoidMorphism I' I'' (↑⊤) G' G'')
:
The Lie map of a composite is the composite of the two Lie maps.
@[simp]
theorem
map_lieExp
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(X : LeftInvariantDerivation I G)
:
A smooth group homomorphism intertwines the Lie-group exponentials through its Lie map.
theorem
continuous_lieMap
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
[T2Space G]
[T2Space G']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
:
Continuous ⇑(lieMap φ)
The Lie map of a smooth homomorphism is continuous, being a linear map between finite-dimensional real normed spaces.
theorem
ContMDiffMonoidMorphism.lieMap_injective_of_mfderiv_injective
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : Function.Injective ⇑(mfderiv% ⇑φ 1))
:
Function.Injective ⇑(lieMap φ)
A smooth homomorphism whose differential at the identity is injective induces an injective Lie-algebra homomorphism.
theorem
ContMDiffMonoidMorphism.lieMap_bijective_of_isLocalDiffeomorphAt
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : IsLocalDiffeomorphAt I I' (↑⊤) (⇑φ) 1)
:
Function.Bijective ⇑(lieMap φ)
The Lie map of a smooth homomorphism that is a local diffeomorphism at the identity is bijective: under evaluation at the identity it is the differential there, a linear equivalence.
theorem
ContMDiffMonoidMorphism.isLocalDiffeomorphAt_of_lieMap_bijective
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : Function.Bijective ⇑(lieMap φ))
:
IsLocalDiffeomorphAt I I' (↑⊤) (⇑φ) 1
A smooth homomorphism with bijective Lie map is a local diffeomorphism at the identity.
theorem
ContMDiffMonoidMorphism.isLocalDiffeomorphAt_iff_lieMap_bijective
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
:
A smooth homomorphism of finite-dimensional Lie groups is a local diffeomorphism at the identity if and only if its Lie map is bijective.
theorem
ContMDiffMonoidMorphism.isLocalDiffeomorph_iff_lieMap_bijective
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(f : ContMDiffMonoidMorphism I I' (↑⊤) G G')
:
A smooth homomorphism of finite-dimensional Lie groups is a local diffeomorphism if and only if its Lie map is bijective.
theorem
ContMDiffMonoidMorphism.isLocalDiffeomorph_of_lieMap_bijective
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(f : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hf : Function.Bijective ⇑(lieMap f))
:
IsLocalDiffeomorph I I' ↑⊤ ⇑f
A smooth homomorphism with bijective Lie map is a local diffeomorphism.
noncomputable def
TauCeti.Lie.lieEquivOfIsLocalDiffeomorphAt
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : IsLocalDiffeomorphAt I I' (↑⊤) (⇑φ) 1)
:
A smooth homomorphism that is a local diffeomorphism at the identity induces an equivalence of Lie algebras.
Instances For
@[simp]
theorem
TauCeti.Lie.lieEquivOfIsLocalDiffeomorphAt_apply
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : IsLocalDiffeomorphAt I I' (↑⊤) (⇑φ) 1)
(X : LeftInvariantDerivation I G)
:
The Lie-algebra equivalence induced by a local diffeomorphism acts by the Lie functor.
@[simp]
theorem
TauCeti.Lie.lieEquivOfIsLocalDiffeomorphAt_toLieHom
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : IsLocalDiffeomorphAt I I' (↑⊤) (⇑φ) 1)
:
The Lie homomorphism underlying the equivalence induced by a local diffeomorphism is its Lie map.
@[simp]
theorem
TauCeti.Lie.lieEquivOfIsLocalDiffeomorphAt_symm_apply_lieMap
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : IsLocalDiffeomorphAt I I' (↑⊤) (⇑φ) 1)
(X : LeftInvariantDerivation I G)
:
The inverse Lie-algebra equivalence of a local diffeomorphism sends the Lie map of a derivation back to that derivation.
@[simp]
theorem
TauCeti.Lie.lieMap_lieEquivOfIsLocalDiffeomorphAt_symm_apply
{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']
[LieGroup I (↑⊤) G]
[LieGroup I' (↑⊤) G']
[FiniteDimensional ℝ E]
[FiniteDimensional ℝ E']
(φ : ContMDiffMonoidMorphism I I' (↑⊤) G G')
(hφ : IsLocalDiffeomorphAt I I' (↑⊤) (⇑φ) 1)
(Y : LeftInvariantDerivation I' G')
:
The Lie map of a local diffeomorphism sends the inverse Lie-algebra equivalence of a derivation back to that derivation.