OAI/CategoryTheory/Thomason/SubdivisionFaces.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Subdivision Faces.

  1. def OAI.Thomason.NormalizedChains.tableStart line 18
  2. def OAI.Thomason.NormalizedChains.tableFinish line 21
  3. lemma OAI.Thomason.NormalizedChains.tableStart_row line 24
  4. lemma OAI.Thomason.NormalizedChains.tableFinish_row line 30
  5. lemma OAI.Thomason.NormalizedChains.tableStart_le_finish line 36
  6. lemma OAI.Thomason.NormalizedChains.map_table_eq_edge line 39
  7. lemma OAI.Thomason.NormalizedChains.ordered_arrow_ext line 65
  8. def OAI.Thomason.NormalizedChains.tableEndpoints line 68
  9. lemma OAI.Thomason.NormalizedChains.tableStart_edge line 87
  10. lemma OAI.Thomason.NormalizedChains.tableFinish_edge line 91
  11. lemma OAI.Thomason.NormalizedChains.edgeTable_diagonal line 95
  12. def OAI.Thomason.NormalizedChains.orientalOneFunctor line 121
  13. def OAI.Thomason.NormalizedChains.ordinalDiagramFunctor line 150
  14. lemma OAI.Thomason.NormalizedChains.ordinalDiagramFunctor_orientalOneFunctor line 155
  15. lemma OAI.Thomason.NormalizedChains.tableStart_vertex line 162
  16. lemma OAI.Thomason.NormalizedChains.tableFinish_vertex line 166
  17. lemma OAI.Thomason.NormalizedChains.tableEndpoints_vertex line 170
  18. lemma OAI.Thomason.NormalizedChains.tableEndpoints_edge line 175
  19. lemma OAI.Thomason.NormalizedChains.orientalOneFunctor_ordinalDiagramFunctor_obj line 181
  20. lemma OAI.Thomason.NormalizedChains.orientalOneFunctor_ordinalDiagramFunctor line 192
  21. def OAI.Thomason.NormalizedChains.orientalOneEquiv line 206
  22. lemma OAI.Thomason.NormalizedChains.complexMap_vertex line 228
  23. lemma OAI.Thomason.NormalizedChains.complexMap_edge line 239
  24. lemma OAI.Thomason.NormalizedChains.orientalOneFunctor_naturality_obj line 256
  25. lemma OAI.Thomason.NormalizedChains.orientalOneFunctor_naturality line 263
  26. def OAI.Thomason.oneNerveIso line 285
  27. def OAI.Thomason.OmegaCategory.oneCell line 308
  28. lemma OAI.Thomason.OmegaCategory.oneSkeletonIso_inv_map line 312
  29. def OAI.Thomason.OmegaCategory.liftOneFunctor line 318
  30. lemma OAI.Thomason.OmegaCategory.liftOneFunctor_map line 323
  31. lemma OAI.Thomason.OmegaCategory.liftOneFunctor_oneMap line 329
  32. lemma OAI.Thomason.OmegaCategory.mappedCast_val line 334
  33. lemma OAI.Thomason.OmegaCategory.oneMap_liftOneFunctor_obj line 340
  34. lemma OAI.Thomason.OmegaCategory.oneMap_liftOneFunctor line 359
  35. def OAI.Thomason.OmegaCategory.oneSkeletonCatFunctor line 388
  36. def OAI.Thomason.OmegaCategory.oneSkeletonFullyFaithful line 394
  37. instance OAI.Thomason.OmegaCategory.(instance at line 401) line 401
  38. instance OAI.Thomason.OmegaCategory.(instance at line 402) line 402
  39. lemma OAI.Thomason.oneNerveIso_natural line 416
  40. def OAI.Thomason.oneNerveFunctorIso line 423
  41. instance OAI.Thomason.streetNerveFiniteOne_full line 429
  42. instance OAI.Thomason.streetNerveFiniteOne_faithful line 432
  43. instance OAI.Thomason.categorificationFiniteOne_counit_iso line 435
  44. def OAI.Thomason.categorificationFiniteOne_nerve_iso line 439
  45. abbrev OAI.Thomason.Subdivision.OrdinalVertices line 455
  46. abbrev OAI.Thomason.Subdivision.OrdinalChains line 460
  47. def OAI.Thomason.Subdivision.ordinalVertex line 461
  48. lemma OAI.Thomason.Subdivision.le_initialFlag line 463
  49. def OAI.Thomason.Subdivision.partialLastVertex line 471
  50. lemma OAI.Thomason.Subdivision.partialLastVertex_apply line 485
  51. lemma OAI.Thomason.Subdivision.chainLast_partialLastVertex line 489
  52. lemma OAI.Thomason.Subdivision.partialLastVertex_initialFlag line 496
  53. lemma OAI.Thomason.Subdivision.partialLastVertex_comp_of_le line 501
  54. lemma OAI.Thomason.Subdivision.partialLastVertex_comm line 512
  55. lemma OAI.Thomason.Subdivision.partialLastVertex_idem line 523
  56. lemma OAI.Thomason.Subdivision.partialLastVertex_top line 527
  57. lemma OAI.Thomason.Subdivision.partialLastVertex_zero line 533
  58. lemma OAI.Thomason.Subdivision.exComparison_apply line 562
  59. def OAI.Thomason.Subdivision.partialLastMap line 574
  60. lemma OAI.Thomason.Subdivision.partialLastMap_comp_of_le line 578
  61. lemma OAI.Thomason.Subdivision.partialLastMap_comm line 585
  62. lemma OAI.Thomason.Subdivision.partialLastMap_zero line 593
  63. def OAI.Thomason.Subdivision.ExLevel line 611
  64. lemma OAI.Thomason.Subdivision.ExLevel.mono line 615
  65. lemma OAI.Thomason.Subdivision.exLevel_top line 623
  66. lemma OAI.Thomason.Subdivision.exLevel_zero_iff line 630
  67. def OAI.Thomason.Subdivision.singletonChain line 660
  68. lemma OAI.Thomason.Subdivision.mem_singletonChain line 670
  69. def OAI.Thomason.Subdivision.chainUnionMap line 673
  70. lemma OAI.Thomason.Subdivision.mem_chainUnionMap line 688
  71. lemma OAI.Thomason.Subdivision.chainUnionMap_singleton line 694
  72. lemma OAI.Thomason.Subdivision.chainUnionMap_map line 701
  73. def OAI.Thomason.Subdivision.extraVertexFace line 716
  74. def OAI.Thomason.Subdivision.extraVertex line 722
  75. lemma OAI.Thomason.Subdivision.predAbove_succ_succAbove line 726
  76. lemma OAI.Thomason.Subdivision.extraVertexFace_gap line 731
  77. def OAI.Thomason.Subdivision.faceVertices line 738
  78. lemma OAI.Thomason.Subdivision.faceVertices_apply line 742
  79. lemma OAI.Thomason.Subdivision.extraVertex_face line 745
  80. def OAI.Thomason.Subdivision.extraVertexMap line 755
  81. lemma OAI.Thomason.Subdivision.extraVertexMap_face line 759
  82. def OAI.Thomason.Subdivision.exPairSimplex line 772
  83. lemma OAI.Thomason.Subdivision.exPairSimplex_face line 776