OAI/CategoryTheory/Thomason/SubdivisionWeak.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

Subdivision Weak.

  1. def OAI.Thomason.Subdivision.conicalFlagExtension line 18
  2. lemma OAI.Thomason.Subdivision.conicalFlagExtension_old line 55
  3. lemma OAI.Thomason.Subdivision.hornFaces_downward line 63
  4. def OAI.Thomason.Subdivision.hornFlagOldVertices line 69
  5. lemma OAI.Thomason.Subdivision.hornFlagOldVertices_old line 80
  6. def OAI.Thomason.Subdivision.hornFlagExtension line 90
  7. lemma OAI.Thomason.Subdivision.hornFlagExtension_old line 95
  8. lemma OAI.Thomason.Subdivision.sd_lastVertex_nerve line 118
  9. def OAI.Thomason.Subdivision.orderedSdExtension line 125
  10. lemma OAI.Thomason.Subdivision.orderedSdExtension_restriction line 130
  11. def OAI.Thomason.Subdivision.hornFlagExtensionAllowed line 171
  12. lemma OAI.Thomason.Subdivision.hornFlagExtensionAllowed_old line 176
  13. def OAI.Thomason.Subdivision.sdHornExtension line 185
  14. lemma OAI.Thomason.Subdivision.sdHornExtension_restriction line 191
  15. lemma OAI.Thomason.Subdivision.exComparison_double_mate line 218
  16. def OAI.Thomason.Subdivision.exHornExtension line 228
  17. lemma OAI.Thomason.Subdivision.exHornExtension_restriction line 234
  18. abbrev OAI.Thomason.Subdivision.exStage line 252
  19. def OAI.Thomason.Subdivision.exSequence line 255
  20. def OAI.Thomason.Subdivision.exInfinity line 258
  21. def OAI.Thomason.Subdivision.exInfinityInclusion line 260
  22. lemma OAI.Thomason.Subdivision.exInfinityInclusion_step line 264
  23. def OAI.Thomason.Subdivision.exInfinityComparison line 272
  24. lemma OAI.Thomason.Subdivision.exInfinityComparison_anodyne line 275
  25. lemma OAI.Thomason.Subdivision.exInfinityComparison_weak line 292
  26. lemma OAI.Thomason.Subdivision.exInfinity_horn_filling line 296
  27. lemma OAI.Thomason.Subdivision.exInfinity_kan line 314
  28. def OAI.Thomason.Subdivision.exStageMap line 334
  29. lemma OAI.Thomason.Subdivision.exStageMap_id line 339
  30. lemma OAI.Thomason.Subdivision.exStageMap_comp line 345
  31. def OAI.Thomason.Subdivision.exSequenceMap line 351
  32. def OAI.Thomason.Subdivision.exSequenceFunctor line 358
  33. def OAI.Thomason.Subdivision.exInfinityFunctor line 364
  34. lemma OAI.Thomason.Subdivision.exInfinityInclusion_naturality line 367
  35. def OAI.Thomason.Subdivision.exInfinityUnit line 372
  36. lemma OAI.Thomason.Subdivision.exInfinity_map_weak_iff line 376
  37. instance OAI.Thomason.Subdivision.exStage_preservesLimits line 401
  38. instance OAI.Thomason.Subdivision.exSequence_preservesLimits line 412
  39. instance OAI.Thomason.Subdivision.sequentialSSetColim_preservesFiniteLimits line 415
  40. instance OAI.Thomason.Subdivision.exInfinity_preservesFiniteLimits line 422
  41. instance OAI.Thomason.Subdivision.finiteNonemptyChains line 438
  42. instance OAI.Thomason.Subdivision.finiteOrderNerve line 443
  43. def OAI.Thomason.Subdivision.exEvaluationIso line 446
  44. instance OAI.Thomason.Subdivision.ex_preservesFilteredColimits line 451
  45. instance OAI.Thomason.Subdivision.exStage_preservesFilteredColimits line 472
  46. instance OAI.Thomason.Subdivision.exSequence_preservesFilteredColimits line 483
  47. instance OAI.Thomason.Subdivision.exInfinity_preservesFilteredColimits line 487
  48. instance OAI.Thomason.Subdivision.exInfinity_preservesMonomorphisms line 491
  49. instance OAI.Thomason.street_preservesFilteredColimits line 506
  50. instance OAI.Thomason.finiteInclusion_preservesFilteredColimits line 509
  51. instance OAI.Thomason.streetFinite_preservesFilteredColimits line 513
  52. instance OAI.Thomason.thomasonRight_preservesFilteredColimits line 518
  53. instance OAI.Thomason.thomasonFiniteRight_preservesFiltered line 523
  54. instance OAI.Thomason.thomasonRight_finitelyAccessible line 528
  55. instance OAI.Thomason.thomasonRightFinite_finitelyAccessible line 531
  56. instance OAI.Thomason.thomasonLeft_finitelyPresentable line 537
  57. instance OAI.Thomason.thomasonLeftFinite_finitelyPresentable line 541
  58. def OAI.Thomason.topPrism line 557
  59. def OAI.Thomason.posetPointMap line 565
  60. def OAI.Thomason.posetTopMap line 568
  61. lemma OAI.Thomason.posetPoint_top line 571
  62. lemma OAI.Thomason.posetTop_point line 574
  63. def OAI.Thomason.tableTopContraction line 577
  64. lemma OAI.Thomason.tablePoint_weakEquivalence line 588
  65. lemma OAI.Thomason.tableMap_weakEquivalence_of_top line 598
  66. lemma OAI.Thomason.NormalizedChains.word_length_le_one_of_subsingleton line 620
  67. lemma OAI.Thomason.NormalizedChains.grade_pos_zero_of_subsingleton line 632
  68. instance OAI.Thomason.NormalizedChains.table_subsingleton line 643
  69. def OAI.Thomason.tablePointTerminal line 670
  70. def OAI.Thomason.tablePointNerveTerminal line 680
  71. def OAI.Thomason.tablePointNerveIso line 685
  72. lemma OAI.Thomason.tableNerve_terminal_weakEquivalence line 689
  73. def OAI.Thomason.NormalizedChains.orderULiftUp line 713
  74. def OAI.Thomason.NormalizedChains.orderULiftDown line 717
  75. lemma OAI.Thomason.NormalizedChains.orderULiftUp_down line 721
  76. lemma OAI.Thomason.NormalizedChains.orderULiftDown_up line 722
  77. def OAI.Thomason.NormalizedChains.complexULiftIso line 727
  78. def OAI.Thomason.categorificationSimplexIso line 765
  79. lemma OAI.Thomason.raisedOriental_terminal_weakEquivalence line 770
  80. lemma OAI.Thomason.categorificationSimplex_terminal_weakEquivalence line 783
  81. def OAI.Thomason.nerveTopSimplex line 810
  82. def OAI.Thomason.nerveTopVertex line 824
  83. def OAI.Thomason.nerveTopCylinder line 832
  84. def OAI.Thomason.nerveTopHomotopy line 841
  85. lemma OAI.Thomason.nerveTop_terminal_weakEquivalence line 869
  86. lemma OAI.Thomason.standardSimplex_terminal_weakEquivalence line 874
  87. lemma OAI.Thomason.categorificationUnit_simplex_weakEquivalence line 883