OAI/GroupTheory/PolycyclicRecognition/Algebra/InnerCentralizerProduct.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A direct product decomposition of the semisimple inner centralizer

The moving factor is central and the other factor is fixed pointwise. Both projections preserve the actual polynomial group law.

  1. def OAI.PolycyclicRecognition.semisimpleFixedSubalgebra line 18
  2. def OAI.PolycyclicRecognition.semisimpleMovingCenter line 27
  3. theorem OAI.PolycyclicRecognition.fixed_mem_innerCentralizer line 36
  4. theorem OAI.PolycyclicRecognition.movingCenter_mem_innerCentralizer line 42
  5. def OAI.PolycyclicRecognition.innerCentralizerFixedGroupProjection line 55
  6. def OAI.PolycyclicRecognition.innerCentralizerMovingGroupProjection line 61
  7. def OAI.PolycyclicRecognition.innerCentralizerProductHom line 69
  8. theorem OAI.PolycyclicRecognition.innerCentralizerProductHom_bijective line 76
  9. def OAI.PolycyclicRecognition.innerCentralizerProductEquiv line 102
  10. def OAI.PolycyclicRecognition.innerCentralizerMovingInclusion line 109
  11. theorem OAI.PolycyclicRecognition.innerCentralizerMovingProjection_section line 114
  12. theorem OAI.PolycyclicRecognition.innerCentralizerMovingProjection_eq_one_iff line 123