OAI/GroupTheory/PolycyclicRecognition/Finiteness/ControlledFillingsFromResolution.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite resolution terms give uniformly controlled fillings

Comparison with the homogeneous resolution provides the filler. Finite generation bounds the image of the filling term, and equivariance bounds the chain homotopy on each input scale.

  1. theorem OAI.PolycyclicRecognition.controlledCycleFillings_of_resolution line 19
  2. theorem OAI.PolycyclicRecognition.TypeFP.controlledCycleFillings line 79