OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalInductionExact.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact induction along the normal subgroup in a cyclic extension

  1. theorem OAI.PolycyclicRecognition.normalInductionMap_mk line 20
  2. theorem OAI.PolycyclicRecognition.inductionCoordinates_naturality line 25
  3. theorem OAI.PolycyclicRecognition.normalInductionMap_injective line 42
  4. instance OAI.PolycyclicRecognition.normalInduction_preservesMonomorphisms line 55
  5. instance OAI.PolycyclicRecognition.normalInduction_preservesHomology line 61
  6. instance OAI.PolycyclicRecognition.normalInduction_preservesProjectives line 65
  7. instance OAI.PolycyclicRecognition.normalInduction_additive line 70
  8. def OAI.PolycyclicRecognition.normalInducedResolution line 80