OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteGroupRelativeInjective.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Extending maps into projectives across integral split inclusions

For a finite group, a projective representation is injective with respect to short exact sequences that split as sequences of abelian groups. The extension uses the coefficient at the identity followed by the finite group sum.

  1. def OAI.PolycyclicRecognition.freeIdentityCoefficient line 18
  2. theorem OAI.PolycyclicRecognition.freeIdentityCoefficient_apply line 25
  3. def OAI.PolycyclicRecognition.freeAveragedLinearMap line 28
  4. theorem OAI.PolycyclicRecognition.freeAveragedLinearMap_coeff line 32
  5. def OAI.PolycyclicRecognition.freeAveragedExtension line 46
  6. theorem OAI.PolycyclicRecognition.freeAveragedExtension_eq line 59
  7. theorem OAI.PolycyclicRecognition.projective_extend_of_integral_retraction line 74