OAI/GroupTheory/PolycyclicRecognition/Algebra/SeparateDerivedClosure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Derived subgroups in the polynomial group topology

Separate continuity of commutators passes derived-series bounds to closure. It also makes the subgroup generated by the commutators of connected subgroups connected. These are the two closure facts required in the solvable matrix-group argument.

  1. theorem OAI.PolycyclicRecognition.commutator_separateClosure_le line 25
  2. theorem OAI.PolycyclicRecognition.isSolvable_separateClosure line 32
  3. theorem OAI.PolycyclicRecognition.isPreconnected_commutator line 54