OAI/CategoryTheory/Thomason/Definitions.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Thomason.OmegaCategory line 12

   Also declared: ComparatorChallenges/ThomasonModelStructures.lean:12 (same declaration text).

2. structure OAI.Thomason.OmegaCategory.Functor line 62

   Also declared: ComparatorChallenges/ThomasonModelStructures.lean:62 (same declaration text).

3. def OAI.Thomason.OmegaCategory.Functor.id line 79

   Also declared: ComparatorChallenges/ThomasonModelStructures.lean:79 (same declaration text).

4. def OAI.Thomason.OmegaCategory.Functor.comp line 85

   Also declared: ComparatorChallenges/ThomasonModelStructures.lean:85 (same declaration text).

5. instance OAI.Thomason.OmegaCategory.(instance at line 107) line 107
6. def OAI.Thomason.OmegaCategory.IsTruncated line 112

   Also declared: ComparatorChallenges/ThomasonModelStructures.lean:112 (same declaration text).

7. def OAI.Thomason.OmegaCategory.NCategory line 114

   Also declared: ComparatorChallenges/ThomasonModelStructures.lean:114 (same declaration text).

8. instance OAI.Thomason.OmegaCategory.(instance at line 116) line 116
9. structure OAI.Thomason.DirectedComplex line 129

   Also declared: ComparatorChallenges/ThomasonModelStructures.lean:129 (same declaration text).

10. structure OAI.Thomason.DirectedComplex.Hom line 148

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:148 (same declaration text).

11. def OAI.Thomason.DirectedComplex.Hom.id line 162

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:162 (same declaration text).

12. def OAI.Thomason.DirectedComplex.Hom.comp line 168

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:168 (same declaration text).

13. instance OAI.Thomason.DirectedComplex.(instance at line 183) line 183
14. structure OAI.Thomason.DirectedComplex.Table line 189

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:189 (same declaration text).

15. def OAI.Thomason.DirectedComplex.Table.truncate line 205

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:205 (same declaration text).

16. def OAI.Thomason.DirectedComplex.Table.comp line 235

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:235 (same declaration text).

17. def OAI.Thomason.DirectedComplex.nu line 309

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:309 (same declaration text).

18. def OAI.Thomason.DirectedComplex.Hom.table line 510

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:510 (same declaration text).

19. def OAI.Thomason.DirectedComplex.Hom.nu line 521

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:521 (same declaration text).

20. def OAI.Thomason.DirectedComplex.nuFunctor line 559

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:559 (same declaration text).

21. abbrev OAI.Thomason.NormalizedChains.Word line 579

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:579 (same declaration text).

22. abbrev OAI.Thomason.NormalizedChains.Chains line 582

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:582 (same declaration text).

23. def OAI.Thomason.NormalizedChains.bracket line 584

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:584 (same declaration text).

24. def OAI.Thomason.NormalizedChains.prepend line 588

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:588 (same declaration text).

25. def OAI.Thomason.NormalizedChains.wordBoundary line 591

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:591 (same declaration text).

26. def OAI.Thomason.NormalizedChains.boundary line 595

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:595 (same declaration text).

27. def OAI.Thomason.NormalizedChains.faces line 608

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:608 (same declaration text).

28. def OAI.Thomason.NormalizedChains.grade line 620

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:620 (same declaration text).

29. def OAI.Thomason.NormalizedChains.emptyWord line 623

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:623 (same declaration text).

30. def OAI.Thomason.NormalizedChains.emptyCoefficient line 625

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:625 (same declaration text).

31. def OAI.Thomason.NormalizedChains.Positive line 627

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:627 (same declaration text).

32. def OAI.Thomason.NormalizedChains.positiveGrade line 629

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:629 (same declaration text).

33. def OAI.Thomason.NormalizedChains.complex line 634

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:634 (same declaration text).

34. def OAI.Thomason.NormalizedChains.map line 835

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:835 (same declaration text).

35. def OAI.Thomason.NormalizedChains.complexMap line 846

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:846 (same declaration text).

36. def OAI.Thomason.NormalizedChains.simplexComplexes line 1180

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1180 (same declaration text).

37. def OAI.Thomason.orientals line 1261

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1261 (same declaration text).

38. def OAI.Thomason.OmegaCategory.ulift line 1272

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1272 (same declaration text).

39. def OAI.Thomason.OmegaCategory.uliftUp line 1308

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1308 (same declaration text).

40. def OAI.Thomason.OmegaCategory.uliftDown line 1314

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1314 (same declaration text).

41. def OAI.Thomason.OmegaCategory.uliftFunctor line 1328

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1328 (same declaration text).

42. def OAI.Thomason.raisedOrientals line 1340

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1340 (same declaration text).

43. structure OAI.Thomason.OmegaCategory.Presentation line 1351

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1351 (same declaration text).

44. structure OAI.Thomason.OmegaCategory.Presentation.Interpretation line 1364

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1364 (same declaration text).

45. inductive OAI.Thomason.OmegaCategory.CellTerm line 1377

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1377 (same declaration text).

46. def OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft line 1391

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1391 (same declaration text).

47. def OAI.Thomason.OmegaCategory.CellTerm.eval line 1395

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1395 (same declaration text).

48. def OAI.Thomason.OmegaCategory.Presentation.Equiv line 1409

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1409 (same declaration text).

49. inductive OAI.Thomason.OmegaCategory.Presentation.Valid line 1412

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1412 (same declaration text).

50. abbrev OAI.Thomason.OmegaCategory.Presentation.ValidTerm line 1418

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1418 (same declaration text).

51. instance OAI.Thomason.OmegaCategory.Presentation.termSetoid line 1420

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1420 (same declaration text).

52. abbrev OAI.Thomason.OmegaCategory.Presentation.Cells line 1431

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1431 (same declaration text).

53. def OAI.Thomason.OmegaCategory.Presentation.evaluate line 1433

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1433 (same declaration text).

54. def OAI.Thomason.OmegaCategory.CellTerm.dimension line 1444

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1444 (same declaration text).

55. def OAI.Thomason.OmegaCategory.Presentation.sourceTerm line 1458

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1458 (same declaration text).

56. def OAI.Thomason.OmegaCategory.Presentation.source line 1460

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1460 (same declaration text).

57. def OAI.Thomason.OmegaCategory.Presentation.targetTerm line 1467

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1467 (same declaration text).

58. def OAI.Thomason.OmegaCategory.Presentation.target line 1469

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1469 (same declaration text).

59. def OAI.Thomason.OmegaCategory.Presentation.compTerm line 1476

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1476 (same declaration text).

60. def OAI.Thomason.OmegaCategory.Presentation.comp line 1481

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1481 (same declaration text).

61. abbrev OAI.Thomason.OmegaCategory.Presentation.category line 1515

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1515 (same declaration text).

62. abbrev OAI.Thomason.OmegaCategory.colimitPresentation line 1655

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1655 (same declaration text).

63. def OAI.Thomason.OmegaCategory.Presentation.generator line 1670

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1670 (same declaration text).

64. def OAI.Thomason.OmegaCategory.colimitInclusion line 1681

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1681 (same declaration text).

65. def OAI.Thomason.OmegaCategory.presentedCocone line 1736

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1736 (same declaration text).

66. def OAI.Thomason.OmegaCategory.Presentation.lift line 1767

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1767 (same declaration text).

67. def OAI.Thomason.OmegaCategory.colimitInterpretation line 1808

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1808 (same declaration text).

68. def OAI.Thomason.OmegaCategory.presentedCoconeIsColimit line 1816

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1816 (same declaration text).

69. instance OAI.Thomason.OmegaCategory.hasColimits line 1865

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1865 (same declaration text).

70. instance OAI.Thomason.omegaHasSimplicialColimits line 1876

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1876 (same declaration text).

71. def OAI.Thomason.categorification line 1880

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1880 (same declaration text).

72. def OAI.Thomason.thomasonLeft line 1891

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1891 (same declaration text).

73. def OAI.Thomason.streetNerve line 1902

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1902 (same declaration text).

74. def OAI.Thomason.streetNerveMap line 1920

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1920 (same declaration text).

75. def OAI.Thomason.streetNerveFunctor line 1925

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1925 (same declaration text).

76. def OAI.Thomason.thomasonRight line 1937

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1937 (same declaration text).

77. def OAI.Thomason.streetYonedaEquiv line 1948

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1948 (same declaration text).

78. def OAI.Thomason.streetYonedaIso line 1956

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1956 (same declaration text).

79. def OAI.Thomason.categorificationAdjunction line 1962

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1962 (same declaration text).

80. def OAI.Thomason.thomasonAdjunction line 1975

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1975 (same declaration text).

81. abbrev OAI.Thomason.OmegaCategory.truncationPresentation line 1986

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1986 (same declaration text).

82. def OAI.Thomason.OmegaCategory.truncationUnit line 1991

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:1991 (same declaration text).

83. def OAI.Thomason.OmegaCategory.truncation line 2046

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2046 (same declaration text).

84. def OAI.Thomason.OmegaCategory.truncationLift line 2067

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2067 (same declaration text).

85. def OAI.Thomason.OmegaCategory.truncationFunctor line 2082

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2082 (same declaration text).

86. def OAI.Thomason.categorificationFinite line 2143

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2143 (same declaration text).

87. def OAI.Thomason.thomasonLeftFinite line 2154

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2154 (same declaration text).

88. def OAI.Thomason.streetNerveFinite line 2165

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2165 (same declaration text).

89. def OAI.Thomason.thomasonRightFinite line 2177

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2177 (same declaration text).

90. def OAI.Thomason.OmegaCategory.nCategoryInclusion line 2188

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2188 (same declaration text).

91. def OAI.Thomason.OmegaCategory.truncationHomEquiv line 2192

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2192 (same declaration text).

92. def OAI.Thomason.OmegaCategory.truncationAdjunction line 2244

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2244 (same declaration text).

93. def OAI.Thomason.categorificationFiniteAdjunction line 2305

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2305 (same declaration text).

94. def OAI.Thomason.thomasonFiniteAdjunction line 2317

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2317 (same declaration text).

95. def OAI.Thomason.WeakHomotopy.loopMap line 2330

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2330 (same declaration text).

96. def OAI.Thomason.WeakHomotopy.groupMap line 2333

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2333 (same declaration text).

97. def OAI.Thomason.WeakHomotopy.componentsMap line 2343

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2343 (same declaration text).

98. def OAI.Thomason.WeakHomotopy.Equivalence line 2347

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2347 (same declaration text).

99. def OAI.Thomason.simplicialWeakEquivalences line 2359

    Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2359 (same declaration text).

100. def OAI.Thomason.simplicialFibrations line 2362

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2362 (same declaration text).

101. structure OAI.Thomason.KanQuillenModel line 2372

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2372 (same declaration text).

102. def OAI.Thomason.LeftProperFor line 2378

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2378 (same declaration text).

103. def OAI.Thomason.RightProperFor line 2383

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2383 (same declaration text).

104. def OAI.Thomason.FibrantFor line 2388

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2388 (same declaration text).

105. def OAI.Thomason.boundaryImages line 2391

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2391 (same declaration text).

106. def OAI.Thomason.hornImages line 2394

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2394 (same declaration text).

107. structure OAI.Thomason.ExactModelEndpoint line 2397

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2397 (same declaration text).

108. def OAI.Thomason.FullMain line 2430

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2430 (same declaration text).

109. def OAI.Thomason.thomasonWeakEquivalences line 2445

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2445 (same declaration text).

110. def OAI.Thomason.thomasonWeakEquivalencesFinite line 2448

     Also declared: ComparatorChallenges/ThomasonModelStructures.lean:2448 (same declaration text).