OAI/GroupTheory/PolycyclicRecognition/Algebra/ExtensionSemisimpleCentralizer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Semisimple centralizers in a smooth nilpotent-kernel extension

For an abelian quotient, every quotient element has a lift whose conjugation on the nilpotent kernel centralizes the semisimple part of a prescribed lift. The correcting element lies in the actual completed kernel.

  1. theorem OAI.PolycyclicRecognition.extension_conjAct_inl line 22
  2. def OAI.PolycyclicRecognition.semisimpleActionCentralizer line 31
  3. theorem OAI.PolycyclicRecognition.extension_outer_conjugation_identity line 36
  4. theorem OAI.PolycyclicRecognition.extension_semisimple_centralizer_correction line 70
  5. theorem OAI.PolycyclicRecognition.extension_semisimple_centralizer_surjective line 96