OAI/GroupTheory/PolycyclicRecognition/Algebra/SequentialHomLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Hom from a finitely presented module commutes with sequential limits

The comparison is an isomorphism of abelian groups, expressed as a linear equivalence over the integers. This includes noncommutative group rings.

  1. def OAI.PolycyclicRecognition.sequentialHomTransition line 19
  2. instance OAI.PolycyclicRecognition.sequentialHomTransition_directed line 25
  3. def OAI.PolycyclicRecognition.sequentialHomCocone line 39
  4. def OAI.PolycyclicRecognition.sequentialHomComparison line 45
  5. theorem OAI.PolycyclicRecognition.sequentialHomComparison_of line 56
  6. theorem OAI.PolycyclicRecognition.sequentialHomComparison_injective line 62
  7. theorem OAI.PolycyclicRecognition.sequentialHomComparison_surjective line 77
  8. def OAI.PolycyclicRecognition.sequentialHomLimitEquiv line 84