OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalCentralLayers.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Rational actions on the upper central layers

Ambient conjugation preserves the characteristic upper central series. On each central layer it therefore gives a rational linear action. Trivial rational action implies trivial action on the layer itself, since the successive quotients are torsion-free.

  1. abbrev OAI.PolycyclicRecognition.CentralLayer line 22
  2. def OAI.PolycyclicRecognition.upperCentralLayerAut line 24
  3. def OAI.PolycyclicRecognition.rationalUpperCentralAction line 29
  4. theorem OAI.PolycyclicRecognition.upperCentralLayerAut_eq_one_of_rational line 34
  5. theorem OAI.PolycyclicRecognition.commutator_centralLayer_le_of_rational_kernel line 43
  6. theorem OAI.PolycyclicRecognition.subgroup_le_rationalUpperCentralAction_ker line 68