Documentation

TauCeti.Geometry.Lie.UniversalCover

The Lie algebra of the universal covering group #

Let G be a finite-dimensional real Lie group that is locally path-connected and semilocally simply connected. Its universal cover UniversalCover (1 : G) is a Lie group, and the covering homomorphism UniversalCover.projHom is a smooth local diffeomorphism. Its differential at the identity is therefore a linear isomorphism, so the Lie functor sends the covering homomorphism to a Lie-algebra isomorphism: the universal covering group and G have the same Lie algebra.

Main results #

References #

source
theorem TauCeti.UniversalCover.isLocalDiffeomorphAt_projHom_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (G : Type u_3) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I (↑⊤) G] :
IsLocalDiffeomorphAt I I (↑⊤) (⇑(ContinuousMonoidHom.toContMDiffMonoidMorphism I I projHom)) 1

The universal covering projection of a Lie group is a local diffeomorphism at the identity.

source
noncomputable def TauCeti.UniversalCover.lieEquivProjHom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (G : Type u_3) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I (↑⊤) G] :
LeftInvariantDerivation I (UniversalCover 1) ≃ₗ⁅ℝ⁆ LeftInvariantDerivation I G

The universal covering projection induces an equivalence between the Lie algebra of the universal covering group and the Lie algebra of the base group.

Instances For
    source
    @[simp]
    theorem TauCeti.UniversalCover.lieEquivProjHom_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I (↑⊤) G] (X : LeftInvariantDerivation I (UniversalCover 1)) :
    (lieEquivProjHom I G) X = (lieMap (ContinuousMonoidHom.toContMDiffMonoidMorphism I I projHom)) X

    The Lie-algebra equivalence induced by the universal covering projection acts by the Lie functor.

    source
    @[simp]
    theorem TauCeti.UniversalCover.lieEquivProjHom_toLieHom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I (↑⊤) G] :
    (lieEquivProjHom I G).toLieHom = lieMap (ContinuousMonoidHom.toContMDiffMonoidMorphism I I projHom)

    The Lie homomorphism underlying the universal-cover Lie-algebra equivalence is the Lie map of the covering projection.

    source
    theorem TauCeti.UniversalCover.lieMap_projHom_bijective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (G : Type u_3) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I (↑⊤) G] :
    Function.Bijective ⇑(lieMap (ContinuousMonoidHom.toContMDiffMonoidMorphism I I projHom))

    The covering homomorphism of the universal cover of a Lie group induces a bijection, hence a Lie-algebra isomorphism, between the Lie algebras of left-invariant derivations.

    source
    @[simp]
    theorem TauCeti.UniversalCover.lieEquivProjHom_symm_apply_lieMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I (↑⊤) G] (X : LeftInvariantDerivation I (UniversalCover 1)) :
    (lieEquivProjHom I G).symm ((lieMap (ContinuousMonoidHom.toContMDiffMonoidMorphism I I projHom)) X) = X

    The inverse of the Lie-algebra equivalence induced by the universal covering projection sends the Lie map of a derivation back to that derivation.

    source
    @[simp]
    theorem TauCeti.UniversalCover.lieMap_projHom_lieEquivProjHom_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [ChartedSpace H G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [LieGroup I (↑⊤) G] (Y : LeftInvariantDerivation I G) :
    (lieMap (ContinuousMonoidHom.toContMDiffMonoidMorphism I I projHom)) ((lieEquivProjHom I G).symm Y) = Y

    The Lie map of the universal covering projection sends the inverse Lie-algebra equivalence of a derivation back to that derivation.