OAI/CategoryTheory/Thomason/Cones.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

Cones.

  1. abbrev OAI.Thomason.OmegaCategory.Objects line 14
  2. def OAI.Thomason.OmegaCategory.sourceObject line 16
  3. def OAI.Thomason.OmegaCategory.targetObject line 19
  4. lemma OAI.Thomason.OmegaCategory.sourceObject_source_zero line 22
  5. lemma OAI.Thomason.OmegaCategory.targetObject_source_zero line 27
  6. lemma OAI.Thomason.OmegaCategory.sourceObject_target_zero line 32
  7. lemma OAI.Thomason.OmegaCategory.targetObject_target_zero line 37
  8. lemma OAI.Thomason.OmegaCategory.sourceObject_source_succ line 42
  9. lemma OAI.Thomason.OmegaCategory.targetObject_source_succ line 47
  10. lemma OAI.Thomason.OmegaCategory.sourceObject_target_succ line 52
  11. lemma OAI.Thomason.OmegaCategory.targetObject_target_succ line 57
  12. lemma OAI.Thomason.OmegaCategory.sourceObject_comp line 62
  13. lemma OAI.Thomason.OmegaCategory.targetObject_comp line 67
  14. lemma OAI.Thomason.OmegaCategory.sourceObject_object line 72
  15. lemma OAI.Thomason.OmegaCategory.targetObject_object line 75
  16. def OAI.Thomason.OmegaCategory.Functor.objects line 78
  17. lemma OAI.Thomason.OmegaCategory.Functor.objects_source line 82
  18. lemma OAI.Thomason.OmegaCategory.Functor.objects_target line 86
  19. def OAI.Thomason.OmegaCategory.thinMap line 90
  20. def OAI.Thomason.OmegaCategory.chaoticLift line 100
  21. def OAI.Thomason.OmegaCategory.chaoticRestrict line 119
  22. def OAI.Thomason.OmegaCategory.chaoticHomEquiv line 122
  23. def OAI.Thomason.OmegaCategory.objectsFunctor line 138
  24. def OAI.Thomason.OmegaCategory.chaoticFunctor line 142
  25. def OAI.Thomason.OmegaCategory.objectsChaoticAdjunction line 146
  26. instance OAI.Thomason.OmegaCategory.objects_preservesColimits line 156
  27. structure OAI.Thomason.OmegaCategory.Subcategory line 170
  28. def OAI.Thomason.OmegaCategory.Subcategory.category line 181
  29. def OAI.Thomason.OmegaCategory.Subcategory.inclusion line 208
  30. def OAI.Thomason.OmegaCategory.Subcategory.lift line 214
  31. lemma OAI.Thomason.OmegaCategory.Subcategory.lift_inclusion line 221
  32. lemma OAI.Thomason.OmegaCategory.Subcategory.inclusion_injective line 224
  33. def OAI.Thomason.OmegaCategory.fullOn line 228
  34. lemma OAI.Thomason.OmegaCategory.comp_fixed line 246
  35. lemma OAI.Thomason.OmegaCategory.comp_eq_of_eq_fixed line 251
  36. def OAI.Thomason.OmegaCategory.Functor.fiber line 258
  37. lemma OAI.Thomason.OmegaCategory.source_object line 285
  38. lemma OAI.Thomason.OmegaCategory.target_object line 288
  39. inductive OAI.Thomason.OmegaCategory.ConeCell line 291
  40. def OAI.Thomason.OmegaCategory.ConeCell.source line 300
  41. def OAI.Thomason.OmegaCategory.ConeCell.target line 306
  42. def OAI.Thomason.OmegaCategory.ConeCell.comp line 312
  43. lemma OAI.Thomason.OmegaCategory.ConeCell.source_source line 330
  44. lemma OAI.Thomason.OmegaCategory.ConeCell.target_target line 337
  45. lemma OAI.Thomason.OmegaCategory.ConeCell.source_target line 344
  46. lemma OAI.Thomason.OmegaCategory.ConeCell.target_source line 351
  47. lemma OAI.Thomason.OmegaCategory.ConeCell.source_comp_le line 358
  48. lemma OAI.Thomason.OmegaCategory.ConeCell.target_comp_le line 370
  49. lemma OAI.Thomason.OmegaCategory.ConeCell.source_comp_gt line 382
  50. lemma OAI.Thomason.OmegaCategory.ConeCell.target_comp_gt line 393
  51. lemma OAI.Thomason.OmegaCategory.ConeCell.unit_left line 417
  52. lemma OAI.Thomason.OmegaCategory.ConeCell.unit_right line 421
  53. lemma OAI.Thomason.OmegaCategory.ConeCell.assoc line 425
  54. lemma OAI.Thomason.OmegaCategory.ConeCell.interchange line 435
  55. lemma OAI.Thomason.OmegaCategory.ConeCell.finite_dimension line 452
  56. def OAI.Thomason.OmegaCategory.terminalCone line 470
  57. lemma OAI.Thomason.OmegaCategory.terminalCone_truncated line 489
  58. def OAI.Thomason.OmegaCategory.terminalConeInclusion line 500
  59. def OAI.Thomason.OmegaCategory.intervalVertex line 516
  60. def OAI.Thomason.OmegaCategory.intervalArrow line 519
  61. lemma OAI.Thomason.OmegaCategory.interval_cases line 521
  62. lemma OAI.Thomason.OmegaCategory.interval_source_arrow line 530
  63. lemma OAI.Thomason.OmegaCategory.interval_target_arrow line 531
  64. lemma OAI.Thomason.OmegaCategory.interval_source_succ line 532
  65. lemma OAI.Thomason.OmegaCategory.interval_target_succ line 533
  66. def OAI.Thomason.OmegaCategory.coneLabel line 535
  67. def OAI.Thomason.OmegaCategory.coneMap line 546
  68. def OAI.Thomason.OmegaCategory.terminalConeFunctor line 570
  69. def OAI.Thomason.OmegaCategory.Functor.fiberMap line 588
  70. def OAI.Thomason.OmegaCategory.fiberFunctor line 597
  71. lemma OAI.Thomason.OmegaCategory.interval_arrow_ne_zero line 612
  72. lemma OAI.Thomason.OmegaCategory.interval_arrow_ne_one line 617
  73. lemma OAI.Thomason.OmegaCategory.interval_zero_ne_one line 622
  74. lemma OAI.Thomason.OmegaCategory.interval_zero_ne_arrow line 627
  75. lemma OAI.Thomason.OmegaCategory.interval_one_ne_arrow line 629
  76. lemma OAI.Thomason.OmegaCategory.interval_one_ne_zero line 631
  77. abbrev OAI.Thomason.OmegaCategory.zeroFiber line 634
  78. def OAI.Thomason.OmegaCategory.zeroSourceObject line 637
  79. lemma OAI.Thomason.OmegaCategory.zeroSourceObject_source_succ line 641
  80. lemma OAI.Thomason.OmegaCategory.zeroSourceObject_target_succ line 648
  81. lemma OAI.Thomason.OmegaCategory.zeroSourceObject_comp line 656
  82. def OAI.Thomason.OmegaCategory.coneExtendMap line 663
  83. lemma OAI.Thomason.OmegaCategory.coneExtendMap_zero line 671
  84. lemma OAI.Thomason.OmegaCategory.coneExtendMap_arrow line 678
  85. lemma OAI.Thomason.OmegaCategory.coneExtendMap_one line 685
  86. lemma OAI.Thomason.OmegaCategory.coneExtendMap_source line 691
  87. lemma OAI.Thomason.OmegaCategory.coneExtendMap_target line 714
  88. lemma OAI.Thomason.OmegaCategory.interval_map_comp_zero_left line 747
  89. lemma OAI.Thomason.OmegaCategory.interval_map_comp_zero_right line 753
  90. lemma OAI.Thomason.OmegaCategory.interval_map_comp_succ line 759
  91. lemma OAI.Thomason.OmegaCategory.coneExtendMap_comp line 765
  92. def OAI.Thomason.OmegaCategory.coneExtend line 832
  93. lemma OAI.Thomason.OmegaCategory.coneExtend_label line 839