OAI/CategoryTheory/Thomason/RecursiveCylinders.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Recursive Cylinders.

  1. def OAI.Thomason.GrayTwo.projectionIndex line 15
  2. lemma OAI.Thomason.GrayTwo.pastedObj_projection line 21
  3. lemma OAI.Thomason.GrayTwo.endpoint_top line 80
  4. lemma OAI.Thomason.GrayTwo.tensorFace_vertical line 87
  5. lemma OAI.Thomason.GrayTwo.pushout_glue line 96
  6. def OAI.Thomason.GrayTwo.cooperation line 104
  7. lemma OAI.Thomason.GrayTwo.cooperation_cell line 107
  8. lemma OAI.Thomason.GrayTwo.cooperation_endpoint line 112
  9. lemma OAI.Thomason.GrayTwo.projection_cell line 138
  10. lemma OAI.Thomason.GrayTwo.map_projection_cell line 159
  11. lemma OAI.Thomason.GrayTwo.cutProjection_left_cell line 166
  12. lemma OAI.Thomason.GrayTwo.cutProjection_right_cell line 174
  13. lemma OAI.Thomason.GrayTwo.cooperation_projection line 182
  14. theorem OAI.Thomason.GrayTwo.firstMixedCooperation line 214
  15. lemma OAI.Thomason.GrayTwo.Diagram.ext line 229
  16. lemma OAI.Thomason.GrayTwo.Diagram.ext_generators line 236
  17. lemma OAI.Thomason.GrayTwo.Diagram.map_paste line 246
  18. lemma OAI.Thomason.GrayTwo.paste_glue_left line 267
  19. lemma OAI.Thomason.GrayTwo.paste_glue_right line 269
  20. lemma OAI.Thomason.GrayTwo.paste_assoc line 271
  21. def OAI.Thomason.GrayTwo.constantObj line 317
  22. lemma OAI.Thomason.GrayTwo.constantObj_bounded line 324
  23. lemma OAI.Thomason.GrayTwo.constantObj_faces line 328
  24. def OAI.Thomason.GrayTwo.constant line 342
  25. lemma OAI.Thomason.GrayTwo.constant_obj line 351
  26. lemma OAI.Thomason.GrayTwo.obj4_bounded line 358
  27. lemma OAI.Thomason.GrayTwo.obj17_bounded line 359
  28. lemma OAI.Thomason.GrayTwo.constant_left_glue line 361
  29. lemma OAI.Thomason.GrayTwo.constant_right_glue line 362
  30. lemma OAI.Thomason.GrayTwo.paste_left_unit line 371
  31. lemma OAI.Thomason.GrayTwo.paste_right_unit line 377
  32. def OAI.Thomason.GlobeComplex.shiftDown line 394
  33. lemma OAI.Thomason.GlobeComplex.shiftDown_coordinate line 412
  34. lemma OAI.Thomason.GlobeComplex.shiftUp_coordinate line 415
  35. lemma OAI.Thomason.GlobeComplex.mass_shiftDown line 418
  36. lemma OAI.Thomason.GlobeComplex.mass_shiftUp line 421
  37. lemma OAI.Thomason.GlobeComplex.positive_shiftDown line 424
  38. lemma OAI.Thomason.GlobeComplex.positive_shiftUp line 427
  39. lemma OAI.Thomason.GlobeComplex.shiftDown_d line 431
  40. lemma OAI.Thomason.GlobeComplex.shiftUp_d line 439
  41. def OAI.Thomason.GlobeComplex.vertexWeights line 445
  42. lemma OAI.Thomason.GlobeComplex.vertexWeights_coordinate line 448
  43. lemma OAI.Thomason.GlobeComplex.vertexWeights_zero line 451
  44. lemma OAI.Thomason.GlobeComplex.vertexWeights_positive line 456
  45. lemma OAI.Thomason.GlobeComplex.d_shiftUp_zero line 461
  46. lemma OAI.Thomason.GlobeComplex.vertexWeights_add line 468
  47. lemma OAI.Thomason.GlobeComplex.mass_d line 474
  48. abbrev OAI.Thomason.GrayRecursive.K line 490
  49. def OAI.Thomason.GrayRecursive.diagonalRow line 492
  50. def OAI.Thomason.GrayRecursive.IsDiagonal line 496
  51. def OAI.Thomason.GrayRecursive.downRow line 499
  52. lemma OAI.Thomason.GrayRecursive.downRow_d line 510
  53. lemma OAI.Thomason.GrayRecursive.downRow_positive line 544
  54. lemma OAI.Thomason.GrayRecursive.diagonal_row_one line 551
  55. def OAI.Thomason.GrayRecursive.down line 575
  56. lemma OAI.Thomason.GrayRecursive.down_row line 589
  57. def OAI.Thomason.GrayRecursive.upRow line 603
  58. lemma OAI.Thomason.GrayRecursive.upRow_d_zero line 626
  59. lemma OAI.Thomason.GrayRecursive.upRow_d_succ line 646
  60. lemma OAI.Thomason.GrayRecursive.upRow_d line 669
  61. lemma OAI.Thomason.GrayRecursive.downRow_upRow line 675
  62. lemma OAI.Thomason.GrayRecursive.upRow_downRow_succ line 678
  63. lemma OAI.Thomason.GrayRecursive.upRow_downRow_zero line 682
  64. lemma OAI.Thomason.GrayRecursive.upRow_positive line 686
  65. lemma OAI.Thomason.GrayRecursive.upRow_zero_d line 692
  66. def OAI.Thomason.GrayRecursive.up line 711
  67. lemma OAI.Thomason.GrayRecursive.up_zero line 737
  68. lemma OAI.Thomason.GrayRecursive.up_succ line 740
  69. lemma OAI.Thomason.GrayRecursive.up_diagonal line 743
  70. lemma OAI.Thomason.GrayRecursive.down_up line 745
  71. lemma OAI.Thomason.GrayRecursive.up_down line 749
  72. def OAI.Thomason.GrayRecursive.diagonalEquiv line 759
  73. def OAI.Thomason.OmegaCategory.homCategory line 775
  74. def OAI.Thomason.OmegaCategory.Functor.homMap line 835
  75. lemma OAI.Thomason.OmegaCategory.homCategory_truncated line 847