Classification of continuous one-parameter subgroups

This file proves that every continuous homomorphism from the real line to a finite-dimensional Lie group is generated by a unique tangent vector, equivalently by a unique left-invariant derivation. The proof uses a private dyadic-local-logarithm argument: logarithms at dyadic times converge to zero, eventually scale exactly under time halving, and therefore determine one global generator.

Main results

• existsUnique_eq_mulInvariantOneParameterSubgroup: tangent-vector existence and uniqueness.
• oneParameterSubgroupEquiv: the classification equivalence between left-invariant derivations and continuous one-parameter subgroups.
• existsUnique_eq_oneParameterSubgroup: the derivation-based existence-and-uniqueness statement.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "One-parameter subgroups".

theorem exists_eq_mulInvariantOneParameterSubgroup {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] (φ : Multiplicative ℝ →ₜ* G) : ∃ (v : GroupLieAlgebra I G), φ = mulInvariantOneParameterSubgroup v

Every continuous one-parameter subgroup is generated by some tangent vector.

theorem mulInvariantOneParameterSubgroup_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] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : Function.Injective mulInvariantOneParameterSubgroup

Distinct tangent vectors generate distinct continuous one-parameter subgroups.

theorem existsUnique_eq_mulInvariantOneParameterSubgroup {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] (φ : Multiplicative ℝ →ₜ* G) : ∃! v : GroupLieAlgebra I G, φ = mulInvariantOneParameterSubgroup v

Every continuous one-parameter subgroup is generated by a unique tangent vector.

theorem oneParameterSubgroup_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] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] [T2Space G] [BoundarylessManifold I G] : Function.Injective oneParameterSubgroup

Distinct left-invariant derivations generate distinct one-parameter subgroups.

theorem oneParameterSubgroup_surjective {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] : Function.Surjective oneParameterSubgroup

Every continuous one-parameter subgroup is generated by a left-invariant derivation.

noncomputable def oneParameterSubgroupEquiv {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] : LeftInvariantDerivation I G ≃ (Multiplicative ℝ →ₜ* G)

Continuous one-parameter subgroups of a finite-dimensional Lie group are equivalent to its left-invariant derivations.

@[simp]

theorem oneParameterSubgroupEquiv_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] (X : LeftInvariantDerivation I G) : oneParameterSubgroupEquiv X = oneParameterSubgroup X

The classification equivalence evaluates to the one-parameter subgroup generated by a left-invariant derivation.

theorem existsUnique_eq_oneParameterSubgroup {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] (φ : Multiplicative ℝ →ₜ* G) : ∃! X : LeftInvariantDerivation I G, φ = oneParameterSubgroup X

Every continuous one-parameter subgroup is generated by a unique left-invariant derivation.