OAI/GroupTheory/PolycyclicRecognition/Geometry/InnerCentralizerLieSubalgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Lie algebra of the inner centralizer

Vectors centralizing S modulo the center form a Lie subalgebra. Their brackets are actually fixed by S, which makes the fixed projection a Lie homomorphism.

  1. theorem OAI.PolycyclicRecognition.bracket_fixed_of_central_differences line 17
  2. def OAI.PolycyclicRecognition.innerCentralizerLieSubalgebra line 30
  3. theorem OAI.PolycyclicRecognition.fixed_projection_bracket line 39
  4. def OAI.PolycyclicRecognition.innerCentralizerFixedProjection line 65
  5. def OAI.PolycyclicRecognition.innerCentralizerCentralProjection line 72
  6. theorem OAI.PolycyclicRecognition.innerCentralizerCentralProjection_central line 91
  7. theorem OAI.PolycyclicRecognition.innerCentralizer_projection_decomposition line 96