OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalRepresentationFunctor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Rationalization and restriction of scalars for group representations

The tensor extension is exact and left adjoint to scalar restriction. Thus it preserves the projectives used in the finite rational-coefficient resolution.

  1. def OAI.PolycyclicRecognition.rationalizeRepresentation line 20
  2. def OAI.PolycyclicRecognition.rationalizeRepresentationMap line 36
  3. def OAI.PolycyclicRecognition.rationalizeRepresentationFunctor line 44
  4. instance OAI.PolycyclicRecognition.(instance at line 56) line 56
  5. def OAI.PolycyclicRecognition.integralRestrictionRepresentation line 63
  6. def OAI.PolycyclicRecognition.integralRestrictionMap line 69
  7. def OAI.PolycyclicRecognition.integralRestrictionFunctor line 75
  8. instance OAI.PolycyclicRecognition.(instance at line 81) line 81
  9. def OAI.PolycyclicRecognition.rationalRepresentationHomEquiv line 86
  10. def OAI.PolycyclicRecognition.rationalRepresentationAdjunction line 118
  11. instance OAI.PolycyclicRecognition.(instance at line 130) line 130
  12. theorem OAI.PolycyclicRecognition.rationalizeRepresentationFunctor_map_exact line 134
  13. instance OAI.PolycyclicRecognition.(instance at line 144) line 144
  14. instance OAI.PolycyclicRecognition.(instance at line 147) line 147
  15. instance OAI.PolycyclicRecognition.(instance at line 150) line 150