OAI/Combinatorics/Coboundary/Chains.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Augmented F2 simplicial chains, boundaries, exactness, and relative attachments.

  1. abbrev OAI.CoboundaryExpanders.InfiniteChains.k line 16
  2. def OAI.CoboundaryExpanders.InfiniteChains.rawBoundary line 18
  3. lemma OAI.CoboundaryExpanders.InfiniteChains.rawBoundary_single line 21
  4. lemma OAI.CoboundaryExpanders.InfiniteChains.rawBoundary_squared line 25
  5. def OAI.CoboundaryExpanders.InfiniteChains.rawCone line 57
  6. lemma OAI.CoboundaryExpanders.InfiniteChains.rawCone_single line 61
  7. lemma OAI.CoboundaryExpanders.InfiniteChains.raw_contraction line 66
  8. structure OAI.CoboundaryExpanders.InfiniteChains.Complex line 100
  9. abbrev OAI.CoboundaryExpanders.InfiniteChains.Complex.Face line 107
  10. instance OAI.CoboundaryExpanders.InfiniteChains.Complex.(instance at line 108) line 108
  11. abbrev OAI.CoboundaryExpanders.InfiniteChains.Complex.Chains line 109
  12. def OAI.CoboundaryExpanders.InfiniteChains.Complex.erase line 111
  13. def OAI.CoboundaryExpanders.InfiniteChains.Complex.boundary line 115
  14. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.boundary_single line 118
  15. def OAI.CoboundaryExpanders.InfiniteChains.Complex.embed line 122
  16. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.embed_single line 125
  17. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.embed_injective line 131
  18. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.embed_boundary line 134
  19. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.boundary_squared line 144
  20. def OAI.CoboundaryExpanders.InfiniteChains.Complex.IsConePoint line 157
  21. def OAI.CoboundaryExpanders.InfiniteChains.Complex.cone line 159
  22. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.embed_cone line 164
  23. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.contraction line 177
  24. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.boundary_exact_of_cone line 192
  25. def OAI.CoboundaryExpanders.InfiniteChains.Complex.chainComplex line 205
  26. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.chainComplex_d line 210
  27. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.chainComplex_exactAt_of_cone line 214
  28. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.chainComplex_homology_isZero_of_cone line 222
  29. def OAI.CoboundaryExpanders.InfiniteChains.Complex.full line 227
  30. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.full_isConePoint line 232
  31. def OAI.CoboundaryExpanders.InfiniteChains.Complex.sumCoefficients line 234
  32. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.sumCoefficients_single line 238
  33. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.embed_zero line 243
  34. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.sumCoefficients_zero_injective line 256
  35. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentation_boundary_zero line 261
  36. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentation_boundary line 271
  37. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentation_exact_of_cone line 275
  38. lemma OAI.CoboundaryExpanders.InfiniteChains.Complex.augmentation_surjective_of_cone line 283
  39. abbrev OAI.CoboundaryExpanders.InfiniteChains.Attachment.Raw line 294
  40. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.supported line 296
  41. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.mem_supported line 300
  42. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.single_mem_supported line 304
  43. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.map_supported line 313
  44. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.append line 321
  45. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.append_single line 325
  46. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.project line 329
  47. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_single line 334
  48. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_append line 340
  49. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_apply line 348
  50. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.joinFaces line 367
  51. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.oldFaces line 370
  52. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.joinFaces_downward line 374
  53. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.oldFaces_downward line 381
  54. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_eq_zero_iff line 391
  55. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.boundary_supported line 412
  56. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.erase_disjSum_inl line 422
  57. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.erase_disjSum_inr line 426
  58. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.boundary_disjSum_single line 430
  59. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_boundary_single line 437
  60. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_boundary line 459
  61. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.append_supported line 468
  62. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_supported line 476
  63. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.graded line 485
  64. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.supported_mono line 489
  65. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.graded_forget line 496
  66. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.boundary_graded line 500
  67. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.append_graded line 514
  68. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.project_graded line 525
  69. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.ExactIn line 536
  70. theorem OAI.CoboundaryExpanders.InfiniteChains.Attachment.relative_filling line 540
  71. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.low_degree_old line 571
  72. def OAI.CoboundaryExpanders.InfiniteChains.Attachment.RelativeExactIn line 583
  73. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.relativeExactIn_join line 588
  74. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.finite_stage line 600
  75. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.push_filling line 613
  76. theorem OAI.CoboundaryExpanders.InfiniteChains.Attachment.exactIn_initial_of_filtration line 625
  77. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.embed_supported_equiv line 650
  78. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.embed_mem_graded line 666
  79. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.exists_embed_of_mem_graded line 672
  80. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.exactIn_iff_boundary_exact line 680
  81. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.chainComplex_exactAt_of_exactIn line 710
  82. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.split_union line 719
  83. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.boundary_piece_supported line 741
  84. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.relativeExactIn_union line 757
  85. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.relativeExactIn_empty line 786
  86. lemma OAI.CoboundaryExpanders.InfiniteChains.Attachment.relativeExactIn_finite_union line 796
  87. theorem OAI.CoboundaryExpanders.InfiniteChains.Attachment.relativeExactIn_iUnion line 815