The exponential map of a commutative Lie group #
For a commutative finite-dimensional real Lie group G the exponential map lieExp : π€ β G is a
homomorphism from the additive group of the Lie algebra. Its image is the identity component of
G; when G is preconnected, lieExp is surjective. Its kernel is a discrete subgroup of π€.
The exponential of a commutative G is moreover an open map, so for a preconnected G it
identifies G with the quotient of π€ by the kernel as topological groups. When G is compact
the quotient of π€ by the kernel is the identity component, hence compact, so the kernel spans
π€ and is a lattice of full rank: a compact connected commutative Lie group is the quotient of
its Lie algebra by a lattice.
Main results #
TauCeti.lieExp_add: the exponential of a commutative Lie group is a homomorphism.TauCeti.lieExpAddMonoidHom: that homomorphism, bundled.TauCeti.range_lieExp: the exponential image is the identity component.TauCeti.lieExp_surjective_of_preconnectedSpace: the exponential of a preconnected commutative Lie group is surjective.TauCeti.discreteTopology_ker_lieExpAddMonoidHom: the kernel of the exponential is discrete.TauCeti.isOpenMap_lieExpAddMonoidHomandTauCeti.isOpenMap_lieExp: the exponential of a commutative Lie group is an open map.TauCeti.lieExpAddMonoidHom_surjective_of_preconnectedSpace: the exponential homomorphism of a preconnected commutative Lie group is surjective.TauCeti.lieExpQuotientKerContinuousAddEquiv: a preconnected commutative Lie group is the quotient of its Lie algebra by the kernel of the exponential, as topological groups.TauCeti.compactSpace_quotient_ker_lieExpAddMonoidHom: for a compact commutative Lie group the quotient of the Lie algebra by the kernel of the exponential is compact.TauCeti.span_ker_lieExpAddMonoidHom_eq_top,TauCeti.isZLattice_ker_lieExpAddMonoidHomandTauCeti.finrank_ker_lieExpAddMonoidHom: for a compact commutative Lie group the kernel of the exponential is a lattice of full rank in the Lie algebra.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 20 (The Exponential Map), Β§ One-Parameter Subgroups and the Exponential Map.
- T. BrΓΆcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter I, Β§ 3 (The Exponential Map), Theorem (3.6) and Lemma (3.8).
- D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 15 (Tori), Proposition 15.3.
@[simp]
theorem
TauCeti.lieExp_add
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
(X Y : LeftInvariantDerivation I G)
:
The exponential of a commutative Lie group is a homomorphism from the additive group of the Lie algebra.
noncomputable def
TauCeti.lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
:
The exponential of a commutative Lie group, as a homomorphism from the additive group of the Lie algebra to the group written additively.
Instances For
@[simp]
theorem
TauCeti.lieExpAddMonoidHom_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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
(X : LeftInvariantDerivation I G)
:
theorem
TauCeti.coe_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
:
The exponential homomorphism is the exponential, viewed as a map into Additive G.
theorem
TauCeti.mem_ker_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
{X : LeftInvariantDerivation I G}
:
Membership in the kernel of the exponential.
instance
TauCeti.discreteTopology_ker_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
:
The kernel of the exponential of a commutative Lie group is a discrete subgroup of the Lie algebra.
theorem
TauCeti.continuous_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
:
The exponential homomorphism is continuous.
theorem
TauCeti.isOpenMap_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
:
The exponential homomorphism of a commutative Lie group is an open map.
theorem
TauCeti.isOpenMap_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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
:
The exponential of a commutative Lie group is an open map.
theorem
TauCeti.range_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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
:
The exponential image of a commutative Lie group is the identity component.
theorem
TauCeti.lieExp_surjective_of_preconnectedSpace
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[PreconnectedSpace G]
:
The exponential of a preconnected commutative Lie group is surjective.
The exponential as a quotient map, and the lattice of a compact group #
theorem
TauCeti.instFiniteDimensionalRealLeftInvariantDerivation_tauCeti
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
:
The Lie algebra is finite-dimensional; a local instance for the rest of this file.
theorem
TauCeti.lieExpAddMonoidHom_surjective_of_preconnectedSpace
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[PreconnectedSpace G]
:
The exponential homomorphism of a preconnected commutative Lie group is surjective.
noncomputable def
TauCeti.lieExpQuotientKerContinuousAddEquiv
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
[PreconnectedSpace G]
:
A preconnected commutative Lie group is the quotient of its Lie algebra by the kernel of the
exponential, as topological groups: the first isomorphism theorem for the open surjective
homomorphism lieExpAddMonoidHom.
Instances For
@[simp]
theorem
TauCeti.lieExpQuotientKerContinuousAddEquiv_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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
[PreconnectedSpace G]
(X : LeftInvariantDerivation I G)
:
@[simp]
theorem
TauCeti.lieExpQuotientKerContinuousAddEquiv_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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
[PreconnectedSpace G]
(X : LeftInvariantDerivation I G)
:
instance
TauCeti.compactSpace_quotient_ker_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
[CompactSpace G]
:
The Lie algebra modulo the kernel of the exponential is compact when the group is: it is the identity component, which is closed.
theorem
TauCeti.span_ker_lieExpAddMonoidHom_eq_top
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
[CompactSpace G]
:
The kernel of the exponential of a compact commutative Lie group spans the Lie algebra.
instance
TauCeti.isZLattice_ker_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[IsTopologicalGroup G]
[CompactSpace G]
:
The kernel of the exponential of a compact commutative Lie group is a lattice in the Lie algebra.
theorem
TauCeti.finrank_ker_lieExpAddMonoidHom
{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]
[FiniteDimensional β E]
[LieGroup I (ββ€) G]
[T2Space G]
[BoundarylessManifold I G]
[IsMulCommutative G]
[CompactSpace G]
:
The rank of the kernel of the exponential is the dimension of the group.