OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalBicomplex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Rationalization of the actual first-quadrant total complex

The finite antidiagonal makes tensoring commute with each total degree. The comparison below keeps the rational scalar action and the signed differential.

  1. abbrev OAI.PolycyclicRecognition.rationalBicomplex line 20
  2. def OAI.PolycyclicRecognition.rationalTotalDegreeEquiv line 26
  3. theorem OAI.PolycyclicRecognition.rationalTotalDegreeEquiv_tmul line 35
  4. theorem OAI.PolycyclicRecognition.rationalTotalDegreeEquiv_d line 44
  5. def OAI.PolycyclicRecognition.rationalTotalComplexIso line 76