OAI/GroupTheory/PolycyclicRecognition/Finiteness/RationalBicomplexComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Rational total comparison for the actual integral bicomplex

Exact rationalization allows the row kernel to be rationally acyclic. The integral rows themselves need not be exact.

  1. abbrev OAI.PolycyclicRecognition.rationalChainFunctor line 17
  2. instance OAI.PolycyclicRecognition.rationalModuleFunctor_preservesFiniteLimits line 20
  3. instance OAI.PolycyclicRecognition.rationalModuleFunctor_preservesFiniteColimits line 24
  4. theorem OAI.PolycyclicRecognition.rational_total_homology_isZero_of_rows line 28
  5. theorem OAI.PolycyclicRecognition.rational_bicomplex_total_of_row_epi_quasiIso line 37
  6. theorem OAI.PolycyclicRecognition.rational_chainZeroProjection_quasiIso line 61
  7. theorem OAI.PolycyclicRecognition.rational_bicomplexZeroRows_total_quasiIso line 79
  8. def OAI.PolycyclicRecognition.rational_totalRowZeroHomologyIso line 87