OAI/GroupTheory/PolycyclicRecognition/Algebra/SubgroupInductionExact.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact induction from arbitrary subgroups

  1. theorem OAI.PolycyclicRecognition.subgroupInductionMap_mk line 15
  2. theorem OAI.PolycyclicRecognition.subgroupInductionCoordinates_naturality line 20
  3. theorem OAI.PolycyclicRecognition.subgroupInductionMap_injective line 37
  4. instance OAI.PolycyclicRecognition.subgroupInduction_preservesMonomorphisms line 50
  5. instance OAI.PolycyclicRecognition.subgroupInduction_preservesHomology line 56
  6. instance OAI.PolycyclicRecognition.subgroupInduction_preservesProjectives line 60
  7. instance OAI.PolycyclicRecognition.subgroupInduction_additive line 65
  8. def OAI.PolycyclicRecognition.subgroupInducedResolution line 75