OAI/GroupTheory/PolycyclicRecognition/Algebra/SequentialRepresentationColimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Concrete sequential colimits of representations

Only the two elementwise properties used in coefficient calculations are packaged: every element comes from a stage, and zero is detected at a later stage. They identify the cocone with the actual group-ring module colimit.

  1. structure OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone line 20
  2. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.moduleMap line 30
  3. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.moduleLift line 33
  4. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.moduleLift_of line 41
  5. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.moduleLift_bijective line 45
  6. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.moduleEquiv line 70
  7. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.lift_finitelyPresented line 73
  8. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.eventually_zero_hom line 92