OAI/GroupTheory/PolycyclicRecognition/Finiteness/CoefficientNaturalCohomology.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coefficient naturality for cohomology from a chosen resolution

The comparison uses one fixed homotopy equivalence with the bar resolution. Consequently it commutes with every coefficient morphism.

  1. theorem OAI.PolycyclicRecognition.repCochainPrecomp_postcomp line 18
  2. theorem OAI.PolycyclicRecognition.inhomogeneousCochainsIso_coefficient line 26
  3. def OAI.PolycyclicRecognition.coefficientNaturalCohomologyIso line 45
  4. theorem OAI.PolycyclicRecognition.coefficientNaturalCohomologyIso_naturality line 54