OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalQuotientCompleteVanishing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional quotients propagate induced-kernel vanishing

The quotient resolution is inflated and tensored with the coefficient. Its countable free terms are actual sums of the induced kernel coefficient.

  1. abbrev OAI.PolycyclicRecognition.quotientTensorFunctor line 20
  2. theorem OAI.PolycyclicRecognition.quotientTensorFunctor_map_exact line 23
  3. instance OAI.PolycyclicRecognition.quotientTensorFunctor_preservesHomology line 30
  4. instance OAI.PolycyclicRecognition.quotientTensorFunctor_preservesMonomorphisms line 34
  5. instance OAI.PolycyclicRecognition.quotientTensorFunctor_preservesEpimorphisms line 38
  6. def OAI.PolycyclicRecognition.quotientTensorRegularIso line 42
  7. def OAI.PolycyclicRecognition.quotientTensorFreeNatIso line 48
  8. theorem OAI.PolycyclicRecognition.TypeFPInfinity.normalQuotient_complete_vanishing line 54