OAI/CategoryTheory/Thomason/Generators.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Generators.

  1. instance OAI.Thomason.thomasonBoundary_smallCardinal line 19
  2. instance OAI.Thomason.thomasonHorn_smallCardinal line 27
  3. instance OAI.Thomason.thomasonBoundaryFinite_smallCardinal line 36
  4. instance OAI.Thomason.thomasonHornFinite_smallCardinal line 45
  5. lemma OAI.Thomason.boundaryImages_right_fib_and_weak line 55
  6. lemma OAI.Thomason.thomasonBoundary_right_fib_and_weak line 63
  7. lemma OAI.Thomason.thomasonBoundaryFinite_right_fib_and_weak line 67
  8. lemma OAI.Thomason.thomasonCofibrations_le_boundaryGenerated line 72
  9. lemma OAI.Thomason.thomasonCofibrationsFinite_le_boundaryGenerated line 76
  10. lemma OAI.Thomason.hornGenerated_le_thomasonCofibrations line 80
  11. lemma OAI.Thomason.hornGeneratedFinite_le_thomasonCofibrations line 85
  12. def OAI.Thomason.thomasonBoundaryFactorization line 90
  13. def OAI.Thomason.thomasonBoundaryFiniteFactorization line 97
  14. def OAI.Thomason.NormalizedChains.injectiveWordMap line 117
  15. lemma OAI.Thomason.NormalizedChains.map_injectiveOrderHom line 124
  16. lemma OAI.Thomason.NormalizedChains.map_injectiveOrderHom_apply line 138
  17. lemma OAI.Thomason.NormalizedChains.map_injectiveOrderHom_injective line 143
  18. lemma OAI.Thomason.NormalizedChains.map_supportedOn line 149
  19. lemma OAI.Thomason.NormalizedChains.supportedOn_of_injective_map line 162
  20. def OAI.Thomason.NormalizedChains.upperCutLinearExtension line 171
  21. lemma OAI.Thomason.NormalizedChains.upperCutLinearExtension_injective line 189
  22. lemma OAI.Thomason.NormalizedChains.positive_supportedOn_of_boundary_upper_partial line 194
  23. lemma OAI.Thomason.NormalizedChains.positive_supportedOn_of_boundary_partial line 231
  24. lemma OAI.Thomason.NormalizedChains.table_supportedOn_upper_partial line 240
  25. lemma OAI.Thomason.NormalizedChains.table_supportedOn_lower_partial line 255
  26. lemma OAI.Thomason.NormalizedChains.table_segment_unique_lift_partial line 270
  27. lemma OAI.Thomason.NormalizedChains.table_source_le_target_partial line 282
  28. lemma OAI.Thomason.NormalizedChains.map_table_injectiveOrderHom line 301
  29. lemma OAI.Thomason.NormalizedChains.positive_cycle_zero_partial line 309
  30. lemma OAI.Thomason.NormalizedChains.table_endomorphism_identity_partial line 317
  31. lemma OAI.Thomason.NormalizedChains.PosetTables.coneTable_one_source line 339
  32. lemma OAI.Thomason.NormalizedChains.PosetTables.coneTable_one_target line 360
  33. def OAI.Thomason.NormalizedChains.PosetTables.tableStart line 393
  34. def OAI.Thomason.NormalizedChains.PosetTables.tableFinish line 396
  35. lemma OAI.Thomason.NormalizedChains.PosetTables.tableStart_row line 399
  36. lemma OAI.Thomason.NormalizedChains.PosetTables.tableFinish_row line 405
  37. lemma OAI.Thomason.NormalizedChains.PosetTables.tableStart_le_finish line 411
  38. lemma OAI.Thomason.NormalizedChains.PosetTables.map_table_eq_edge line 414
  39. lemma OAI.Thomason.NormalizedChains.PosetTables.ordered_arrow_ext line 440
  40. def OAI.Thomason.NormalizedChains.PosetTables.tableEndpoints line 443
  41. lemma OAI.Thomason.NormalizedChains.PosetTables.tableStart_edge line 462
  42. lemma OAI.Thomason.NormalizedChains.PosetTables.tableFinish_edge line 466
  43. lemma OAI.Thomason.NormalizedChains.PosetTables.edgeTable_diagonal line 470
  44. def OAI.Thomason.NormalizedChains.PosetTables.posetOneFunctor line 496
  45. def OAI.Thomason.NormalizedChains.PosetTables.posetDiagramFunctor line 525
  46. lemma OAI.Thomason.NormalizedChains.PosetTables.posetDiagramFunctor_posetOneFunctor line 530
  47. lemma OAI.Thomason.NormalizedChains.PosetTables.tableStart_vertex line 537
  48. lemma OAI.Thomason.NormalizedChains.PosetTables.tableFinish_vertex line 541
  49. lemma OAI.Thomason.NormalizedChains.PosetTables.tableEndpoints_vertex line 545
  50. lemma OAI.Thomason.NormalizedChains.PosetTables.tableEndpoints_edge line 550
  51. lemma OAI.Thomason.NormalizedChains.PosetTables.posetOneFunctor_posetDiagramFunctor_obj line 556
  52. lemma OAI.Thomason.NormalizedChains.PosetTables.posetOneFunctor_posetDiagramFunctor line 567
  53. def OAI.Thomason.NormalizedChains.PosetTables.posetOneEquiv line 581
  54. lemma OAI.Thomason.NormalizedChains.PosetTables.complexMap_vertex line 603
  55. lemma OAI.Thomason.NormalizedChains.PosetTables.complexMap_edge line 614
  56. lemma OAI.Thomason.NormalizedChains.PosetTables.posetOneFunctor_naturality_obj line 631
  57. lemma OAI.Thomason.NormalizedChains.PosetTables.posetOneFunctor_naturality line 638
  58. lemma OAI.Thomason.tableObjects_map line 660
  59. def OAI.Thomason.chaoticNerveLift line 671
  60. def OAI.Thomason.chaoticNerveRestrict line 685
  61. lemma OAI.Thomason.chaoticNerveRestrict_lift line 689
  62. lemma OAI.Thomason.chaoticNerveLift_restrict line 695
  63. def OAI.Thomason.verticesChaoticHomEquiv line 718
  64. def OAI.Thomason.verticesChaoticAdjunction line 725
  65. def OAI.Thomason.categorificationObjectsIso line 739
  66. def OAI.Thomason.OmegaCategory.objectsFiniteFunctor line 757
  67. def OAI.Thomason.OmegaCategory.chaoticFiniteFunctor line 760
  68. def OAI.Thomason.OmegaCategory.objectsFiniteChaoticAdjunction line 764
  69. lemma OAI.Thomason.OmegaCategory.objectsFinite_preservesColimits line 771
  70. def OAI.Thomason.categorificationFiniteObjectsIso line 787
  71. def OAI.Thomason.posetCategorificationObjectsIso line 794
  72. def OAI.Thomason.posetCategorificationFiniteObjectsIso line 798
  73. lemma OAI.Thomason.posetCategorificationObjectsIso_natural line 803
  74. def OAI.Thomason.OmegaCategory.finiteInterval line 825
  75. def OAI.Thomason.OmegaCategory.fiberFiniteFunctor line 828
  76. def OAI.Thomason.OmegaCategory.terminalConeFiniteObj line 834
  77. def OAI.Thomason.OmegaCategory.terminalConeFiniteFunctor line 839
  78. def OAI.Thomason.OmegaCategory.zeroFiberFiniteConeAdjunction line 859
  79. instance OAI.Thomason.OmegaCategory.zeroFiberFinite_preservesColimits line 885