OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexDiagonal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite coordinates for the first-quadrant total complex

Each total degree is the finite antidiagonal of the actual bicomplex. These coordinates allow finite elimination, without assuming convergence of a spectral sequence.

  1. abbrev OAI.PolycyclicRecognition.NatBicomplex line 21
  2. abbrev OAI.PolycyclicRecognition.bicomplexDiagonal line 24
  3. def OAI.PolycyclicRecognition.bicomplexToDiagonal line 29
  4. def OAI.PolycyclicRecognition.bicomplexFromDiagonal line 37
  5. theorem OAI.PolycyclicRecognition.bicomplexToDiagonal_ι line 43
  6. theorem OAI.PolycyclicRecognition.bicomplexFromDiagonal_single line 57
  7. theorem OAI.PolycyclicRecognition.bicomplexToFromDiagonal line 71
  8. theorem OAI.PolycyclicRecognition.bicomplexFromToDiagonal line 78
  9. def OAI.PolycyclicRecognition.bicomplexDiagonalEquiv line 96