OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexFiniteHomology.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finiteness from the finite diagonal of row homology

Only the row homology groups on the selected diagonal need be finite. The proof uses the actual total-homology filtration and lowers support by an actual boundary when a leading class vanishes.

  1. theorem OAI.PolycyclicRecognition.integral_range_fg_of_kernel_control line 21
  2. theorem OAI.PolycyclicRecognition.filteredTotalHomology_mono line 39
  3. theorem OAI.PolycyclicRecognition.filteredTotalHomology_zero line 47
  4. theorem OAI.PolycyclicRecognition.filteredTotalHomology_top line 59
  5. theorem OAI.PolycyclicRecognition.bicomplex_total_homology_finite_of_diagonal line 71