OAI/GroupTheory/PolycyclicRecognition/Finiteness/FiniteKernelsFromFillings.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Controlled fillings make the next resolution kernel finite

The kernel is the sum of two finite images: controlled fillers mapped back from homogeneous chains, and the comparison homotopy applied to the finite resolution term. This proves finite generation without assuming noetherianity of the group ring.

  1. theorem OAI.PolycyclicRecognition.resolution_comp_range_le_kernel line 21
  2. theorem OAI.PolycyclicRecognition.finite_resolution_kernel_of_controlledFillings line 32