OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexTotalComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Total comparison through an acyclic row kernel

The quotient in a short exact sequence of first-quadrant bicomplexes induces a quasi-isomorphism of total complexes when the kernel rows are exact.

  1. theorem OAI.PolycyclicRecognition.integral_shortExact_quasiIso_g line 16
  2. theorem OAI.PolycyclicRecognition.bicomplex_total_quotient_quasiIso line 36
  3. theorem OAI.PolycyclicRecognition.bicomplex_total_of_row_epi_quasiIso line 47