Kronecker's theorem: topological generators of commutative Lie groups

A topological generator of a topological group is an element g whose closed cyclic subgroup closedZpowers g is the whole group. For a connected commutative Lie group G with Lie algebra 𝔤 and integral lattice Λ = ker (lieExp : 𝔤 → G), the exponential of X ∈ 𝔤 is a topological generator exactly when Λ + ℤ X is dense in 𝔤 (closedZpowers_lieExp_eq_top_iff), since the exponential is an open continuous surjection whose fibres are the cosets of Λ. When G is compact, Λ spans 𝔤 and the vectors X with Λ + ℤ X dense are dense in 𝔤 (AddSubgroup.dense_setOfPred_dense_sup, Kronecker's theorem), so topological generators are dense in G.

Main results

• TauCeti.closedZpowers_lieExp_eq_top_iff: lieExp X is a topological generator of a connected commutative Lie group if and only if Λ + ℤ X is dense in the Lie algebra.
• TauCeti.dense_setOfPred_closedZpowers_eq_top and TauCeti.exists_closedZpowers_eq_top: topological generators of a compact connected commutative Lie group are dense; in particular they exist.

References

• T. Bröcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter I, § 4, Theorem (4.13) (Kronecker's theorem) and Proposition (4.14).
• D. Bump, Lie Groups, 2nd ed., Springer GTM 225 (2013), Chapter 15, Theorem 15.1 and Corollary 15.1.

theorem TauCeti.closedZpowers_lieExp_eq_top_iff {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] [IsMulCommutative G] [IsTopologicalGroup G] [PreconnectedSpace G] (X : LeftInvariantDerivation I G) : closedZpowers (lieExp X) = ⊤ ↔ Dense ↑(lieExpAddMonoidHom.ker ⊔ AddSubgroup.zmultiples X)

Kronecker's criterion: lieExp X is a topological generator of a connected commutative Lie group if and only if Λ + ℤ X is dense in the Lie algebra, Λ the kernel of the exponential.

theorem TauCeti.dense_setOfPred_closedZpowers_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] [IsMulCommutative G] [IsTopologicalGroup G] [CompactSpace G] [PreconnectedSpace G] : Dense {g : G | closedZpowers g = ⊤}

Topological generators of a compact connected commutative Lie group are dense.

theorem TauCeti.exists_closedZpowers_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] [IsMulCommutative G] [IsTopologicalGroup G] [CompactSpace G] [PreconnectedSpace G] : ∃ (g : G), closedZpowers g = ⊤

A compact connected commutative Lie group has a topological generator.