OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalCoinvariantsInflationIso.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Degree zero in the normal coinvariant resolution

Inflated representations have trivial kernel action. Their normal coinvariants recover the original representation, including its quotient action.

  1. def OAI.PolycyclicRecognition.normalCoinvariantsInflationUnit line 18
  2. def OAI.PolycyclicRecognition.normalCoinvariantsInflationIso line 26
  3. instance OAI.PolycyclicRecognition.normalCoinvariants_leftAdjoint line 44
  4. def OAI.PolycyclicRecognition.normalQuotientResolutionZeroHomologyIso line 48