OAI/CategoryTheory/Thomason/LabelledFibers.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Labelled Fibers.

  1. def OAI.Thomason.OmegaCategory.opFiniteFunctor line 16
  2. def OAI.Thomason.OmegaCategory.opFiniteEquivalence line 20
  3. instance OAI.Thomason.OmegaCategory.opFiniteFunctor_isEquivalence line 26
  4. def OAI.Thomason.OmegaCategory.reverseLabelFiniteObj line 29
  5. def OAI.Thomason.OmegaCategory.reverseLabelFiniteFunctor line 34
  6. def OAI.Thomason.OmegaCategory.reverseLabelFiniteTwiceIso line 46
  7. def OAI.Thomason.OmegaCategory.reverseLabelFiniteEquivalence line 55
  8. instance OAI.Thomason.OmegaCategory.reverseLabelFiniteFunctor_isEquivalence line 65
  9. def OAI.Thomason.OmegaCategory.reversedZeroFiberFiniteIso line 69
  10. def OAI.Thomason.OmegaCategory.reversedZeroFiberFiniteNatIso line 90
  11. instance OAI.Thomason.OmegaCategory.oneFiberFinite_preservesColimits line 98
  12. lemma OAI.Thomason.OmegaCategory.labelled_pushout_fibers line 114
  13. lemma OAI.Thomason.OmegaCategory.labelled_pushout_finite_fibers line 126
  14. lemma OAI.Thomason.OmegaCategory.pushout_objects line 139
  15. lemma OAI.Thomason.OmegaCategory.pushout_finite_objects line 145
  16. def OAI.Thomason.Attachments.complementMap line 168
  17. lemma OAI.Thomason.Attachments.complementMap_old line 172
  18. lemma OAI.Thomason.Attachments.complementMap_new line 175
  19. def OAI.Thomason.Attachments.complementCocone line 178
  20. def OAI.Thomason.Attachments.complementCoconeIsColimit line 185
  21. def OAI.Thomason.Attachments.pushoutComplementIso line 207
  22. lemma OAI.Thomason.posetCategorificationFiniteObjectsIso_natural line 224
  23. lemma OAI.Thomason.pushoutObjectCoordinateChange line 234
  24. lemma OAI.Thomason.poset_pushout_objects line 244
  25. def OAI.Thomason.posetPushoutObjectsComplementIso line 260
  26. lemma OAI.Thomason.poset_pushout_finite_objects line 270
  27. def OAI.Thomason.posetPushoutFiniteObjectsComplementIso line 288
  28. def OAI.Thomason.NormalizedChains.PosetTables.fullOnVertices line 315
  29. lemma OAI.Thomason.NormalizedChains.PosetTables.segmentTableMap_objects_mem line 318
  30. def OAI.Thomason.NormalizedChains.PosetTables.segmentTableMap line 323
  31. lemma OAI.Thomason.NormalizedChains.PosetTables.segmentTableMap_val line 330
  32. lemma OAI.Thomason.NormalizedChains.PosetTables.segmentTableMap_injective line 334
  33. lemma OAI.Thomason.NormalizedChains.PosetTables.segmentTableMap_surjective line 343
  34. def OAI.Thomason.NormalizedChains.PosetTables.segmentTableIso line 366
  35. lemma OAI.Thomason.NormalizedChains.PosetTables.segmentTableIso_hom line 371
  36. lemma OAI.Thomason.NormalizedChains.PosetTables.segmentTableIso_inclusion line 374
  37. def OAI.Thomason.OmegaCategory.intervalFiberObjects line 392
  38. lemma OAI.Thomason.OmegaCategory.interval_fiber_full_iff line 395
  39. def OAI.Thomason.OmegaCategory.intervalFiberFullIso line 418
  40. lemma OAI.Thomason.OmegaCategory.zero_fiber_isObjectSieve line 433
  41. lemma OAI.Thomason.OmegaCategory.one_fiber_isObjectCosieve line 446
  42. def OAI.Thomason.OmegaCategory.maxLabel line 459
  43. def OAI.Thomason.OmegaCategory.minLabel line 473
  44. lemma OAI.Thomason.OmegaCategory.intervalCell_eq_vertex_iff line 487
  45. lemma OAI.Thomason.OmegaCategory.maxLabel_zero_fiber line 498
  46. lemma OAI.Thomason.OmegaCategory.minLabel_one_fiber line 509
  47. def OAI.Thomason.OmegaCategory.truncationOverFunctor line 532
  48. def OAI.Thomason.OmegaCategory.truncationOverAdjunction line 537
  49. def OAI.Thomason.OmegaCategory.terminalConeFiniteInclusionIso line 541
  50. def OAI.Thomason.OmegaCategory.truncationZeroFiberIso line 546
  51. def OAI.Thomason.NormalizedChains.PosetTables.tableLabel line 568
  52. def OAI.Thomason.NormalizedChains.PosetTables.tableLabelFiberIso line 587
  53. lemma OAI.Thomason.NormalizedChains.PosetTables.tableLabel_level_segment line 602
  54. def OAI.Thomason.NormalizedChains.PosetTables.tableFiberSegmentIso line 614
  55. lemma OAI.Thomason.NormalizedChains.PosetTables.tableFiberSegmentIso_inclusion line 619
  56. def OAI.Thomason.NormalizedChains.PosetTables.truncationTableZeroFiberIso line 623
  57. def OAI.Thomason.OmegaCategory.initialConeFunctor line 641
  58. def OAI.Thomason.OmegaCategory.oneFiberConeAdjunction line 644
  59. def OAI.Thomason.OmegaCategory.initialConeFiniteFunctor line 648
  60. def OAI.Thomason.OmegaCategory.oneFiberFiniteConeAdjunction line 652
  61. def OAI.Thomason.OmegaCategory.initialConeFiniteInclusionIso line 658
  62. def OAI.Thomason.OmegaCategory.truncationOneFiberIso line 663
  63. def OAI.Thomason.OmegaCategory.truncationFiberIso line 671
  64. def OAI.Thomason.NormalizedChains.PosetTables.truncationTableFiberIso line 695
  65. lemma OAI.Thomason.NormalizedChains.PosetTables.tableStart_map line 715
  66. lemma OAI.Thomason.NormalizedChains.PosetTables.tableFinish_map line 725
  67. lemma OAI.Thomason.NormalizedChains.PosetTables.tableLabel_natural line 735
  68. def OAI.Thomason.NormalizedChains.PosetTables.lowerSegmentLabel line 745
  69. lemma OAI.Thomason.NormalizedChains.PosetTables.lowerSegmentLabel_zero line 757
  70. def OAI.Thomason.NormalizedChains.PosetTables.upperSegmentLabel line 763
  71. lemma OAI.Thomason.NormalizedChains.PosetTables.upperSegmentLabel_one line 775
  72. def OAI.Thomason.OmegaCategory.truncationFiberComparison line 793
  73. lemma OAI.Thomason.OmegaCategory.truncationFiberComparison_unit line 800
  74. lemma OAI.Thomason.OmegaCategory.truncationZeroFiberIso_inv_app line 807
  75. def OAI.Thomason.OmegaCategory.fiberFiniteInclusion line 853
  76. lemma OAI.Thomason.OmegaCategory.truncationFiberComparison_inclusion line 858
  77. lemma OAI.Thomason.OmegaCategory.truncationZeroFiberIso_inv_inclusion line 869
  78. lemma OAI.Thomason.NormalizedChains.PosetTables.truncationTableZeroFiberIso_inclusion line 891