OAI/Combinatorics/Coboundary/Joins.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Binary and finite joins, augmented exactness, and bounded cone constructions.

  1. def OAI.CoboundaryExpanders.InfiniteChains.Join.complex line 22
  2. def OAI.CoboundaryExpanders.InfiniteChains.Join.prepend line 30
  3. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.prepend_single line 34
  4. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.prepend_boundary line 38
  5. def OAI.CoboundaryExpanders.InfiniteChains.Join.leftAction line 48
  6. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.leftAction_single line 52
  7. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.leftAction_prepend line 58
  8. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.leftAction_homotopy line 65
  9. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.left_contraction line 77
  10. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.leftAction_graded line 85
  11. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.fill_small_left line 107
  12. def OAI.CoboundaryExpanders.InfiniteChains.Join.truncated line 125
  13. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.truncated_downward line 129
  14. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.relative_enlarge_old line 135
  15. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.relativeExactIn_self line 147
  16. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.truncated_step line 152
  17. theorem OAI.CoboundaryExpanders.InfiniteChains.Join.exactIn_join line 209
  18. def OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.cut line 249
  19. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.cut_single line 252
  20. lemma OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.cut_boundary line 256
  21. def OAI.CoboundaryExpanders.InfiniteChains.Cone.BoundedCone.normalize line 265
  22. def OAI.CoboundaryExpanders.InfiniteChains.Join.crossLinear line 288
  23. def OAI.CoboundaryExpanders.InfiniteChains.Join.cross line 291
  24. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_single_left line 294
  25. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_single_right line 298
  26. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_zero_left line 306
  27. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_zero_right line 308
  28. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_add_left line 310
  29. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_add_right line 313
  30. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_sum_left line 316
  31. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_sum_right line 319
  32. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_boundary line 322
  33. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_graded line 340
  34. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cross_size line 356
  35. def OAI.CoboundaryExpanders.InfiniteChains.Join.operator line 365
  36. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.operator_single line 371
  37. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.operator_boundary line 376
  38. def OAI.CoboundaryExpanders.InfiniteChains.Join.residual line 384
  39. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.residual_eq line 387
  40. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.residual_boundary line 390
  41. def OAI.CoboundaryExpanders.InfiniteChains.Join.joinHom line 396
  42. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.joinHom_contraction line 400
  43. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.cut_boundary_high line 424
  44. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.residual_cut_low line 433
  45. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.residual_cut_graded line 441
  46. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.residual_cut_size line 458
  47. def OAI.CoboundaryExpanders.InfiniteChains.Join.boundedCone line 475
  48. def OAI.CoboundaryExpanders.InfiniteChains.Join.fiber line 536
  49. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.mem_fiber line 538
  50. def OAI.CoboundaryExpanders.InfiniteChains.Join.finiteComplex line 547
  51. def OAI.CoboundaryExpanders.InfiniteChains.Join.splitEquiv line 557
  52. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.splitEquiv_zero line 563
  53. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.splitEquiv_succ line 565
  54. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.split_left line 567
  55. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.split_right_fiber line 578
  56. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.finiteComplex_split line 589
  57. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.finiteComplex_one line 602
  58. def OAI.CoboundaryExpanders.InfiniteChains.Join.oneEquiv line 612
  59. theorem OAI.CoboundaryExpanders.InfiniteChains.Join.exactIn_finiteComplex line 618
  60. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.exactIn_empty_left line 650
  61. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.exactIn_empty_right line 686
  62. lemma OAI.CoboundaryExpanders.InfiniteChains.Join.finiteComplex_only_empty line 727
  63. theorem OAI.CoboundaryExpanders.InfiniteChains.Join.exactIn_finiteComplex_all line 736