OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalizedFreeRepresentation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The normalized free cover of an integral representation

The basis omits zero, and a coefficient morphism sends a basis element to zero whenever its image is zero. Thus the free-cover functor preserves zero maps. The augmentation is a natural epimorphism with projective source.

  1. def OAI.PolycyclicRecognition.normalizedFreeRepresentation line 18
  2. def OAI.PolycyclicRecognition.normalizedFreeGenerator line 21
  3. theorem OAI.PolycyclicRecognition.normalizedFreeGenerator_zero line 27
  4. theorem OAI.PolycyclicRecognition.normalizedFreeGenerator_of_ne_zero line 31
  5. def OAI.PolycyclicRecognition.normalizedFreeMap line 36
  6. theorem OAI.PolycyclicRecognition.normalizedFreeMap_generator line 42
  7. def OAI.PolycyclicRecognition.normalizedFreeAugmentation line 57
  8. theorem OAI.PolycyclicRecognition.normalizedFreeAugmentation_generator line 61
  9. instance OAI.PolycyclicRecognition.normalizedFreeAugmentation_epi line 74
  10. theorem OAI.PolycyclicRecognition.normalizedFreeMap_id line 80
  11. theorem OAI.PolycyclicRecognition.normalizedFreeMap_comp line 89
  12. theorem OAI.PolycyclicRecognition.normalizedFreeMap_zero line 100
  13. def OAI.PolycyclicRecognition.normalizedFreeFunctor line 109
  14. theorem OAI.PolycyclicRecognition.normalizedFreeAugmentation_natural line 115
  15. instance OAI.PolycyclicRecognition.normalizedFreeRepresentation_projective line 127