OAI/GroupTheory/PolycyclicRecognition/Algebra/DirectedLowerCentral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Directed unions with a uniform lower-central bound

The lower-central terms of a directed union are witnessed in its constituent subgroups. The uniform bound from integral cohomological dimension therefore allows Zorn's lemma to produce a maximal nilpotent normal subgroup.

  1. def OAI.PolycyclicRecognition.directedLowerCentral line 17
  2. theorem OAI.PolycyclicRecognition.sSup_lowerCentralSeries_le_directedLowerCentral line 33
  3. theorem OAI.PolycyclicRecognition.sSup_lowerCentralSeries_eq_bot line 50
  4. theorem OAI.PolycyclicRecognition.exists_maximal_nilpotent_normal_subgroup line 59