OAI/AlgebraicTopology/Cubical/HeightChains.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicalChains.HeightFiltration.embed line 15
  2. theorem OAI.CubicalChains.HeightFiltration.embed_single line 18
  3. theorem OAI.CubicalChains.HeightFiltration.embed_front line 22
  4. theorem OAI.CubicalChains.HeightFiltration.upperTerm_embed line 30
  5. theorem OAI.CubicalChains.HeightFiltration.upper_embed line 40
  6. def OAI.CubicalChains.HeightFiltration.homotopyTerm line 47
  7. def OAI.CubicalChains.HeightFiltration.homotopy line 50
  8. theorem OAI.CubicalChains.HeightFiltration.homotopy_single line 53
  9. theorem OAI.CubicalChains.HeightFiltration.homotopy_embed line 57
  10. theorem OAI.CubicalChains.HeightFiltration.upper_homotopy line 75
  11. def OAI.CubicalChains.HeightFiltration.above line 83
  12. theorem OAI.CubicalChains.HeightFiltration.above_mono line 87
  13. theorem OAI.CubicalChains.HeightFiltration.embed_supported line 94
  14. theorem OAI.CubicalChains.HeightFiltration.homotopyTerm_above line 102
  15. theorem OAI.CubicalChains.HeightFiltration.homotopy_above line 112
  16. theorem OAI.CubicalChains.HeightFiltration.lowerTerm_above line 127
  17. theorem OAI.CubicalChains.HeightFiltration.lower_above line 135
  18. theorem OAI.CubicalChains.HeightFiltration.upper_above line 146
  19. theorem OAI.CubicalChains.HeightFiltration.boundary_above line 158
  20. theorem OAI.CubicalChains.HeightFiltration.homotopy_zero line 166
  21. def OAI.CubicalChains.HeightFiltration.push line 176
  22. theorem OAI.CubicalChains.HeightFiltration.push_apply line 179
  23. theorem OAI.CubicalChains.HeightFiltration.push_single_negative line 182
  24. theorem OAI.CubicalChains.HeightFiltration.push_single_nonnegative line 195
  25. theorem OAI.CubicalChains.HeightFiltration.push_above line 205
  26. theorem OAI.CubicalChains.HeightFiltration.boundary_squared line 229
  27. theorem OAI.CubicalChains.HeightFiltration.push_boundary line 241
  28. theorem OAI.CubicalChains.HeightFiltration.push_into_halfspace line 249
  29. def OAI.CubicalChains.HeightFiltration.total line 264

    Source documentation

    All valid cells of degree k, without a height restriction.

    def total (k : ℕ) : Submodule ℤ (Chains G A) :=
…

    Mentions: OAI.CubicalChains.Chains

  30. theorem OAI.CubicalChains.HeightFiltration.above_total line 268
  31. theorem OAI.CubicalChains.HeightFiltration.finite_lower_bound line 275
  32. theorem OAI.CubicalChains.HeightFiltration.halfspace_cycle_bounds line 286
  33. def OAI.CubicalChains.Reflection.relabel line 304
  34. theorem OAI.CubicalChains.Reflection.relabel_single line 307
  35. theorem OAI.CubicalChains.Reflection.relabel_front line 310
  36. theorem OAI.CubicalChains.Reflection.relabel_boundaryTerm line 317
  37. def OAI.CubicalChains.Reflection.letters line 324
  38. def OAI.CubicalChains.Reflection.mirror line 325
  39. theorem OAI.CubicalChains.Reflection.mirror_single line 328
  40. theorem OAI.CubicalChains.Reflection.letters_map line 333
  41. theorem OAI.CubicalChains.Reflection.letters_sign line 337
  42. theorem OAI.CubicalChains.Reflection.commute_prod line 342
  43. theorem OAI.CubicalChains.Reflection.prod_inv line 349
  44. theorem OAI.CubicalChains.Reflection.letters_origin line 358
  45. theorem OAI.CubicalChains.Reflection.mirror_single_explicit line 368
  46. theorem OAI.CubicalChains.Reflection.mirror_boundaryTerm line 374
  47. theorem OAI.CubicalChains.Reflection.mirror_twice_single line 383
  48. theorem OAI.CubicalChains.Reflection.mirror_total line 396
  49. theorem OAI.CubicalChains.Reflection.mirror_boundary line 404
  50. theorem OAI.CubicalChains.Reflection.mirror_twice line 417
  51. theorem OAI.CubicalChains.Reflection.inverse_cycle_bounds line 429
  52. theorem OAI.CubicalChains.Reflection.height_inverse_step line 452
  53. theorem OAI.CubicalChains.Reflection.height_prod line 459
  54. theorem OAI.CubicalChains.Reflection.height_inv_prod line 468
  55. def OAI.CubicalChains.Reflection.below line 474

    Source documentation

    Cubes lying entirely in the nonpositive halfspace.

    def below (k : ℕ) : Submodule ℤ (Chains G A) :=
…

    Mentions: OAI.CubicalChains.Chains

  56. theorem OAI.CubicalChains.Reflection.below_total line 478
  57. theorem OAI.CubicalChains.Reflection.mirror_above_below line 485
  58. theorem OAI.CubicalChains.Reflection.mirror_below_above line 499
  59. theorem OAI.CubicalChains.Reflection.below_boundary line 515
  60. theorem OAI.CubicalChains.Reflection.below_cycle_bounds line 533
  61. def OAI.CubicalChains.LevelExact.select line 564
  62. theorem OAI.CubicalChains.LevelExact.select_single line 567
  63. theorem OAI.CubicalChains.LevelExact.select_supported line 573
  64. theorem OAI.CubicalChains.LevelExact.select_eq_self line 584
  65. theorem OAI.CubicalChains.LevelExact.select_eq_zero line 595
  66. def OAI.CubicalChains.LevelExact.plus line 605
  67. def OAI.CubicalChains.LevelExact.minus line 606
  68. def OAI.CubicalChains.LevelExact.crossPart line 607
  69. def OAI.CubicalChains.LevelExact.crossing line 608
  70. theorem OAI.CubicalChains.LevelExact.crossing_total line 613
  71. theorem OAI.CubicalChains.LevelExact.plus_mem line 620
  72. theorem OAI.CubicalChains.LevelExact.minus_mem line 627
  73. theorem OAI.CubicalChains.LevelExact.crossPart_mem line 634
  74. theorem OAI.CubicalChains.LevelExact.decomposition line 642
  75. theorem OAI.CubicalChains.LevelExact.plus_self line 667
  76. theorem OAI.CubicalChains.LevelExact.plus_below_zero line 670
  77. theorem OAI.CubicalChains.LevelExact.crossPart_above_zero line 677
  78. theorem OAI.CubicalChains.LevelExact.crossPart_below_zero line 683
  79. theorem OAI.CubicalChains.LevelExact.crossPart_self line 692
  80. theorem OAI.CubicalChains.LevelExact.crossing_one_zero line 698
  81. theorem OAI.CubicalChains.LevelExact.halves_inter_zero line 708
  82. theorem OAI.CubicalChains.LevelExact.boundary_total line 728
  83. theorem OAI.CubicalChains.LevelExact.boundary_squared_total line 734
  84. def OAI.CubicalChains.LevelExact.levelBoundary line 741

    Source documentation

    The connecting boundary on a crossing square is the difference of its two height-zero vertices.

    def levelBoundary : Chains G A →ₗ[ℤ] Chains G A :=
…

    Mentions: OAI.CubicalChains.Chains

  85. theorem OAI.CubicalChains.LevelExact.levelBoundary_apply line 744
  86. theorem OAI.CubicalChains.LevelExact.levelBoundary_above line 748
  87. theorem OAI.CubicalChains.LevelExact.levelBoundary_below line 754
  88. theorem OAI.CubicalChains.LevelExact.levelBoundary_crossPart line 759
  89. theorem OAI.CubicalChains.LevelExact.levelBoundary_cross_boundary line 767
  90. theorem OAI.CubicalChains.LevelExact.level_cycle_bounds line 774
  91. theorem OAI.CubicalChains.LevelExact.total_four_zero line 811
  92. theorem OAI.CubicalChains.LevelExact.level_boundary_injective line 821