OAI/GroupTheory/PolycyclicRecognition/Analysis/CofiberChainSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The split-in-each-degree sequence of a chain mapping cone

  1. theorem OAI.PolycyclicRecognition.chainDownSuccessorRel line 15
  2. def OAI.PolycyclicRecognition.cofiberChainProjectionComponent line 17
  3. def OAI.PolycyclicRecognition.cofiberChainProjection line 22
  4. theorem OAI.PolycyclicRecognition.cofiberChain_inclusion_projection line 41
  5. abbrev OAI.PolycyclicRecognition.cofiberChainSequence line 52
  6. def OAI.PolycyclicRecognition.cofiberChainDegreeSplitting line 56
  7. theorem OAI.PolycyclicRecognition.cofiberChainSequence_shortExact line 87