OAI/GroupTheory/BooneHigman/MappingTori.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Sequential limits, injective induced maps, and finite presentation of mapping tori.

  1. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.transition line 15
  2. instance OAI.FiniteAlgebraicEnvelopes.SequentialLimit.(instance at line 17) line 17
  3. abbrev OAI.FiniteAlgebraicEnvelopes.SequentialLimit.Limit line 28
  4. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.of line 30
  5. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.of_transition line 35
  6. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.of_succ line 38
  7. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.lift line 46
  8. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.lift_of line 52
  9. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.hom_ext line 55
  10. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.shiftHom line 60
  11. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.forwardHom line 66
  12. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.shift_of line 75
  13. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.forward_of line 76
  14. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.shift line 78
  15. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.shift_apply_of line 91
  16. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.shift_symm_of line 92
  17. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.compatible_of_succ line 94
  18. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.action line 108
  19. abbrev OAI.FiniteAlgebraicEnvelopes.SequentialLimit.Torus line 111
  20. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.base line 113
  21. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.stable line 114
  22. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.action_one line 116
  23. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.action_neg_one line 119
  24. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.relation line 124
  25. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.stageMap line 135
  26. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.stageMap_apply line 138
  27. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.stageMap_succ line 141
  28. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.limitMap line 145
  29. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.limitMap_of line 148
  30. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.limitMap_shift line 150
  31. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.limitMap_shift_inv line 158
  32. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.limitMap_shift_zpow line 165
  33. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.torusLift line 180
  34. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.torusLift_base line 186
  35. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.torusLift_stable line 189
  36. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.inl_of line 194
  37. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.torus_hom_ext line 207
  38. abbrev OAI.FiniteAlgebraicEnvelopes.MappingTorus.Free line 229
  39. def OAI.FiniteAlgebraicEnvelopes.MappingTorus.letter line 230
  40. def OAI.FiniteAlgebraicEnvelopes.MappingTorus.relator line 231
  41. def OAI.FiniteAlgebraicEnvelopes.MappingTorus.relations line 234
  42. instance OAI.FiniteAlgebraicEnvelopes.MappingTorus.(instance at line 235) line 235
  43. abbrev OAI.FiniteAlgebraicEnvelopes.MappingTorus.Presentation line 236
  44. def OAI.FiniteAlgebraicEnvelopes.MappingTorus.base line 237
  45. def OAI.FiniteAlgebraicEnvelopes.MappingTorus.stable line 238
  46. theorem OAI.FiniteAlgebraicEnvelopes.MappingTorus.relation line 240
  47. def OAI.FiniteAlgebraicEnvelopes.MappingTorus.lift line 252
  48. theorem OAI.FiniteAlgebraicEnvelopes.MappingTorus.lift_base line 259
  49. theorem OAI.FiniteAlgebraicEnvelopes.MappingTorus.lift_stable line 262
  50. theorem OAI.FiniteAlgebraicEnvelopes.MappingTorus.hom_ext line 266
  51. def OAI.FiniteAlgebraicEnvelopes.MappingTorus.equivalence line 280
  52. theorem OAI.FiniteAlgebraicEnvelopes.MappingTorus.finite_relations line 298
  53. theorem OAI.FiniteAlgebraicEnvelopes.MappingTorus.finitelyPresented line 328
  54. theorem OAI.FiniteAlgebraicEnvelopes.MappingTorus.torus_finitelyPresented line 334
  55. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.transition_natural line 346
  56. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.map line 358
  57. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.map_of line 365
  58. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.map_shift line 367
  59. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.map_surjective line 370
  60. theorem OAI.FiniteAlgebraicEnvelopes.SequentialLimit.map_injective line 378

    Source documentation

    Killing the coefficient kernel in one step makes the induced map injective. No injectivity assumption on either transition is needed.

    theorem map_injective (hk : ∀ x, q x = 1 → f x = 1) : Function.Injective (map f g q hq) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.SequentialLimit.map

  61. def OAI.FiniteAlgebraicEnvelopes.SequentialLimit.equivalence line 392