OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexTotalExactFunctor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exactness of first-quadrant totalization

Finite antidiagonal coordinates transfer degreewise exactness to the actual total-complex functor.

  1. abbrev OAI.PolycyclicRecognition.integralFirstQuadrantTotal line 18
  2. instance OAI.PolycyclicRecognition.integralFirstQuadrantTotal_additive line 22
  3. theorem OAI.PolycyclicRecognition.bicomplex_total_preserves_exact line 42
  4. instance OAI.PolycyclicRecognition.integralFirstQuadrantTotal_preservesHomology line 68