OAI/GroupTheory/PolycyclicRecognition/Finiteness/InducedResolutionHomology.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tensoring an induced resolution

The projection formula, with the tensor factors in resolution order, identifies an induced resolution with subgroup homology for restricted coefficients.

  1. theorem OAI.PolycyclicRecognition.coinvariantsBraiding_mk line 23
  2. theorem OAI.PolycyclicRecognition.coinvariantsTensorMap_mk line 27
  3. def OAI.PolycyclicRecognition.inducedTensorRightIso line 32
  4. theorem OAI.PolycyclicRecognition.inducedTensorRightIso_mk line 39
  5. def OAI.PolycyclicRecognition.inducedTensorRightNatIso line 52
  6. def OAI.PolycyclicRecognition.inducedResolutionTensorIso line 78
  7. def OAI.PolycyclicRecognition.inducedResolutionHomologyIso line 85