OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalBarConjugation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Comparing subgroup conjugation with ambient bar translation

The conjugation map on the subgroup bar complex equals ambient translation composed with the bar endomorphism already homotopic to the identity.

  1. theorem OAI.PolycyclicRecognition.subgroupBarConjugation_free line 19
  2. def OAI.PolycyclicRecognition.ambientConjugationNatTrans line 39
  3. def OAI.PolycyclicRecognition.ambientBarTranslation line 50
  4. theorem OAI.PolycyclicRecognition.subgroupBarConjugation_chain line 59
  5. theorem OAI.PolycyclicRecognition.quotientBar_inner_homology line 70