Profinite and topological groups

Groups with topology or approximated by finite quotients: profinite and pro-p groups, residual finiteness and separability, profinite rigidity, Golod–Shafarevich inequality, just-infinite groups, totally disconnected locally compact groups, group topologies, Lie groups and their dense subgroups.

• Arcwise connectedness of metric groups
• Conjugacy separability
• Finite images of minimax groups
• Free pro-p groups
• Golod–Shafarevich inequality
• Group topologies
• Nottingham group
• Profinite CN-groups
• Profinite rigidity
• Residually finite p-groups and residual nilpotence
• Separability of isolated subgroups
• Strong completeness of profinite groups
• Subgroup separability of Baumslag–Solitar groups
• Totally disconnected locally compact groups
• Upper composition factors of finitely generated groups

TheoremTwo elements generate a dense subgroup of a connected semisimple Lie group#●ready to prove

Every connected real analytic Lie group \(G\) whose Lie algebra is semisimple contains two elements \(a\) and \(b\) such that the subgroup of \(G\) generated by \(a\) and \(b\) is dense in \(G\). In particular, for connected groups the number 4 in Problem 90 of the Scottish Book (four elements generating a dense subgroup) can be lowered to 2.

theorem_wanted semisimpleLieGroup_twoGeneratorsDense :
    ∀ (n : ℕ) (G : Type*) [Group G] [TopologicalSpace G]
      [ChartedSpace (EuclideanSpace ℝ (Fin n)) G]
      [LieGroup (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ G]
      [ConnectedSpace G]
      [LieAlgebra.IsSemisimple ℝ
        (GroupLieAlgebra (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) G)],
      ∃ a b : G,
        Dense (Subgroup.closure {a, b} : Set G)

Sources

• S. Ulam and H. Auerbach, Problem 90 of the Scottish Book (every semi-simple Lie group contains four elements generating a dense subgroup; can the number 4 be lowered?); Mauldin commentary: every connected semi-simple Lie group has a free subgroup with two generators, and such a free subgroup can be chosen dense.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.