OAI/GroupTheory/Congruence/HomologyEdge.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Abstract augmented resolutions and bounded homology edge surjectivity.

  1. structure OAI.CoboundaryExpanders.HomologyEdge.ResolutionPieces line 18
  2. abbrev OAI.CoboundaryExpanders.HomologyEdge.short line 28
  3. abbrev OAI.CoboundaryExpanders.HomologyEdge.Hmap line 29
  4. lemma OAI.CoboundaryExpanders.HomologyEdge.delta_zero_of_mono line 31
  5. theorem OAI.CoboundaryExpanders.HomologyEdge.kernel_homology_isZero line 37
  6. theorem OAI.CoboundaryExpanders.HomologyEdge.epi_edge line 62
  7. lemma OAI.CoboundaryExpanders.HomologyEdge.mono_H0_inc line 83
  8. structure OAI.CoboundaryExpanders.HomologyEdge.Bounded.BoundedPieces line 108
  9. abbrev OAI.CoboundaryExpanders.HomologyEdge.Bounded.short line 118
  10. abbrev OAI.CoboundaryExpanders.HomologyEdge.Bounded.Hmap line 119
  11. lemma OAI.CoboundaryExpanders.HomologyEdge.Bounded.delta_zero_of_mono line 121
  12. theorem OAI.CoboundaryExpanders.HomologyEdge.Bounded.kernel_homology_isZero line 127
  13. theorem OAI.CoboundaryExpanders.HomologyEdge.Bounded.epi_edge line 154
  14. lemma OAI.CoboundaryExpanders.HomologyEdge.Bounded.mono_H0_inc line 175
  15. structure OAI.CoboundaryExpanders.HomologyEdge.AugmentedData line 205
  16. def OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.K line 212
  17. def OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.inc line 215
  18. instance OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.inc_mono line 216
  19. def OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.sur line 219
  20. lemma OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.sur_inc line 222
  21. lemma OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.zero line 224
  22. lemma OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.short_exact line 231
  23. def OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.pieces line 245
  24. lemma OAI.CoboundaryExpanders.HomologyEdge.AugmentedData.epi_edge line 260