OAI/GroupTheory/PolycyclicRecognition/Finiteness/CofiberCochainSequence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The short exact sequence of cochains of a mapping cone

  1. def OAI.PolycyclicRecognition.cofiberCochainInclusionComponent line 21
  2. def OAI.PolycyclicRecognition.cofiberCochainInclusion line 29
  3. def OAI.PolycyclicRecognition.cofiberCochainProjection line 55
  4. theorem OAI.PolycyclicRecognition.cofiberCochainInclusion_projection line 59
  5. def OAI.PolycyclicRecognition.cofiberCochainSequence line 74
  6. theorem OAI.PolycyclicRecognition.cofiberCochainProjection_surjective line 78
  7. theorem OAI.PolycyclicRecognition.cofiberCochainInclusion_injective line 86
  8. theorem OAI.PolycyclicRecognition.cofiberCochainSequence_exact_degree line 103
  9. theorem OAI.PolycyclicRecognition.cofiberCochainSequence_shortExact line 134
  10. def OAI.PolycyclicRecognition.cofiberCochainSectionComponent line 142
  11. theorem OAI.PolycyclicRecognition.cofiberCochainSection_projection line 146
  12. theorem OAI.PolycyclicRecognition.cofiberCochainSection_d line 155