OAI/GroupTheory/PolycyclicRecognition/Algebra/ControlledCycleFillings.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Coarse invariance of uniformly controlled cycle fillings

Only finite chains occur here. A fixed input scale must admit a fixed filling scale for every cycle. This quantitative condition is stronger than ordinary acyclicity of the standard resolution and is the condition needed in the remaining finiteness argument.

  1. def OAI.PolycyclicRecognition.HasControlledCycleFillings line 19
  2. theorem OAI.PolycyclicRecognition.tupleChainMap_id line 28
  3. theorem OAI.PolycyclicRecognition.tupleChainMap_comp line 37
  4. theorem OAI.PolycyclicRecognition.tupleChainMap_cycle line 48
  5. theorem OAI.PolycyclicRecognition.tupleChainPrism_cycle line 58
  6. theorem OAI.PolycyclicRecognition.HasControlledCycleFillings.of_coarse line 75
  7. theorem OAI.PolycyclicRecognition.controlledCycleFillings_coarse_iff line 107