OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompletedCohomologyColimitKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Detecting zero complete classes in a coefficient colimit

Under FP-infinity, a complete class whose image in the coefficient colimit is zero already dies at a finite coefficient stage.

  1. theorem OAI.PolycyclicRecognition.normalizedCohomologyForward_comp line 18
  2. theorem OAI.PolycyclicRecognition.TypeFPInfinity.completedCohomology_colimit_kernel line 24