OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalCoinvariantsProjective.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Normal coinvariants preserve projective representations

The right adjoint is the actual inflation along the quotient homomorphism. This gives projective terms in the quotient complex used for the higher central-filtration comparison.

  1. def OAI.PolycyclicRecognition.normalCoinvariantsInflationCounit line 20
  2. theorem OAI.PolycyclicRecognition.normalCoinvariantsInflationCounit_mk line 38
  3. def OAI.PolycyclicRecognition.normalCoinvariantsInflationAdjunction line 42
  4. instance OAI.PolycyclicRecognition.normalCoinvariants_preservesProjective line 67
  5. instance OAI.PolycyclicRecognition.normalCoinvariantsResolutionTerm_projective line 72