OAI/GroupTheory/PolycyclicRecognition/Finiteness/RepCochainMaps.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Maps and homotopies on cochains computed from representation complexes

  1. def OAI.PolycyclicRecognition.repCochainPrecomp line 19
  2. theorem OAI.PolycyclicRecognition.repCochainPrecomp_apply line 24
  3. theorem OAI.PolycyclicRecognition.repCochainPrecomp_comp line 28
  4. theorem OAI.PolycyclicRecognition.repCochainPrecomp_id line 35
  5. theorem OAI.PolycyclicRecognition.repCochainPrecomp_sub line 40
  6. def OAI.PolycyclicRecognition.repCochainHomotopy line 46
  7. def OAI.PolycyclicRecognition.repCochainHomotopyEquiv line 50
  8. def OAI.PolycyclicRecognition.repCochainPostcomp line 61
  9. theorem OAI.PolycyclicRecognition.repCochainPostcomp_apply line 71
  10. def OAI.PolycyclicRecognition.repCochainPostcompIso line 75