OAI/CategoryTheory/Thomason/Linearization.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Linearization.

  1. def OAI.Thomason.OmegaCategory.op line 14
  2. lemma OAI.Thomason.OmegaCategory.op_op line 40
  3. def OAI.Thomason.OmegaCategory.Functor.op line 42
  4. lemma OAI.Thomason.OmegaCategory.Functor.op_op line 49
  5. lemma OAI.Thomason.OmegaCategory.Functor.op_id line 52
  6. lemma OAI.Thomason.OmegaCategory.Functor.op_comp line 54
  7. lemma OAI.Thomason.OmegaCategory.op_truncated line 58
  8. def OAI.Thomason.OmegaCategory.opFunctor line 61
  9. def OAI.Thomason.OmegaCategory.opEquivalence line 65
  10. def OAI.Thomason.OmegaCategory.intervalReflect line 71
  11. lemma OAI.Thomason.OmegaCategory.intervalReflect_vertex line 84
  12. lemma OAI.Thomason.OmegaCategory.intervalReflect_arrow line 87
  13. lemma OAI.Thomason.OmegaCategory.intervalReflect_involutive line 89
  14. lemma OAI.Thomason.OmegaCategory.intervalReflect_injective line 95
  15. def OAI.Thomason.OmegaCategory.reverseLabel line 98
  16. lemma OAI.Thomason.OmegaCategory.reverseLabel_reverseLabel line 101
  17. def OAI.Thomason.OmegaCategory.reverseLabelFunctor line 109
  18. def OAI.Thomason.OmegaCategory.reverseLabelTwiceIso line 131
  19. def OAI.Thomason.OmegaCategory.reverseLabelEquivalence line 139
  20. instance OAI.Thomason.OmegaCategory.reverseLabelFunctor_isEquivalence line 148
  21. instance OAI.Thomason.OmegaCategory.opFunctor_isEquivalence line 151
  22. def OAI.Thomason.OmegaCategory.reversedZeroFiberIso line 154
  23. def OAI.Thomason.OmegaCategory.reversedZeroFiberNatIso line 175
  24. instance OAI.Thomason.OmegaCategory.oneFiber_preservesColimits line 183
  25. def OAI.Thomason.NormalizedChains.edgeTable line 201
  26. lemma OAI.Thomason.NormalizedChains.edgeTable_source line 240
  27. lemma OAI.Thomason.NormalizedChains.edgeTable_target line 247
  28. lemma OAI.Thomason.NormalizedChains.edgeTable_sourceObject line 254
  29. lemma OAI.Thomason.NormalizedChains.edgeTable_targetObject line 258
  30. def OAI.Thomason.OmegaCategory.IsObjectSieve line 272
  31. def OAI.Thomason.OmegaCategory.IsObjectCosieve line 275
  32. lemma OAI.Thomason.OmegaCategory.isObjectSieve_iff_oneCells line 278
  33. lemma OAI.Thomason.OmegaCategory.isObjectCosieve_iff_oneCells line 287
  34. lemma OAI.Thomason.OmegaCategory.simplex_objects_mem_sieve line 298
  35. lemma OAI.Thomason.OmegaCategory.simplex_objects_mem_cosieve line 319
  36. def OAI.Thomason.OmegaCategory.Functor.liftFullOn line 340
  37. lemma OAI.Thomason.OmegaCategory.Functor.liftFullOn_inclusion line 346
  38. lemma OAI.Thomason.OmegaCategory.simplex_sieve_cover line 350
  39. lemma OAI.Thomason.OmegaCategory.simplex_cosieve_cover line 361
  40. def OAI.Thomason.OmegaCategory.fullOnMap line 384
  41. lemma OAI.Thomason.OmegaCategory.fullOnMap_inclusion line 391
  42. def OAI.Thomason.OmegaCategory.fullNerve line 395
  43. def OAI.Thomason.OmegaCategory.fullNerveIso line 399
  44. lemma OAI.Thomason.OmegaCategory.fullNerveIso_hom_ι line 426
  45. instance OAI.Thomason.OmegaCategory.fullInclusion_nerve_mono line 430
  46. instance OAI.Thomason.OmegaCategory.fullOnMap_nerve_mono line 435
  47. lemma OAI.Thomason.OmegaCategory.fullNerve_inf line 440
  48. lemma OAI.Thomason.OmegaCategory.fullNerve_sieve_sup line 445
  49. lemma OAI.Thomason.OmegaCategory.fullNerve_cosieve_sup line 456
  50. lemma OAI.Thomason.OmegaCategory.fullNerve_isPushout line 467
  51. lemma OAI.Thomason.OmegaCategory.sieve_cover_nerve_isPushout line 478
  52. lemma OAI.Thomason.OmegaCategory.cosieve_cover_nerve_isPushout line 486
  53. def OAI.Thomason.OmegaCategory.sourceCell line 504
  54. def OAI.Thomason.OmegaCategory.targetCell line 507
  55. lemma OAI.Thomason.OmegaCategory.sourceCell_source_lt line 510
  56. lemma OAI.Thomason.OmegaCategory.targetCell_target_lt line 515
  57. lemma OAI.Thomason.OmegaCategory.sourceCell_target_lt line 520
  58. lemma OAI.Thomason.OmegaCategory.targetCell_source_lt line 525
  59. def OAI.Thomason.OmegaCategory.gradedComp line 530
  60. lemma OAI.Thomason.OmegaCategory.sourceCell_comp_lt line 536
  61. lemma OAI.Thomason.OmegaCategory.targetCell_comp_lt line 542
  62. abbrev OAI.Thomason.OmegaCategory.LambdaRaw line 548
  63. def OAI.Thomason.OmegaCategory.lambdaRelations line 550
  64. abbrev OAI.Thomason.OmegaCategory.LambdaChain line 557
  65. def OAI.Thomason.OmegaCategory.lambdaGen line 559
  66. lemma OAI.Thomason.OmegaCategory.lambdaGen_degenerate line 562
  67. lemma OAI.Thomason.OmegaCategory.lambdaGen_comp line 567
  68. lemma OAI.Thomason.OmegaCategory.lambda_linear_ext line 577
  69. def OAI.Thomason.OmegaCategory.lambdaRawD line 589
  70. lemma OAI.Thomason.OmegaCategory.lambdaRawD_single line 593
  71. lemma OAI.Thomason.OmegaCategory.lambdaRawD_relations line 598
  72. def OAI.Thomason.OmegaCategory.lambdaD line 625
  73. lemma OAI.Thomason.OmegaCategory.lambdaD_gen line 628
  74. lemma OAI.Thomason.OmegaCategory.lambdaD_square line 633
  75. def OAI.Thomason.OmegaCategory.lambdaRawAug line 663
  76. lemma OAI.Thomason.OmegaCategory.lambdaRawAug_relations line 666
  77. def OAI.Thomason.OmegaCategory.lambdaAug line 672
  78. lemma OAI.Thomason.OmegaCategory.lambdaAug_gen line 675
  79. lemma OAI.Thomason.OmegaCategory.lambdaAug_d line 680
  80. def OAI.Thomason.OmegaCategory.lambdaPositive line 686
  81. lemma OAI.Thomason.OmegaCategory.lambdaGen_positive line 689
  82. def OAI.Thomason.OmegaCategory.linearization line 693
  83. lemma OAI.Thomason.OmegaCategory.lambdaGen_source_above line 702
  84. lemma OAI.Thomason.OmegaCategory.lambdaGen_target_above line 709
  85. def OAI.Thomason.OmegaCategory.lambdaUnitTable line 717
  86. lemma OAI.Thomason.OmegaCategory.lambdaUnitTable_row line 742
  87. lemma OAI.Thomason.OmegaCategory.lambdaUnitTable_source line 746
  88. lemma OAI.Thomason.OmegaCategory.lambdaUnitTable_target line 770
  89. lemma OAI.Thomason.OmegaCategory.lambdaUnitTable_comp line 796
  90. def OAI.Thomason.OmegaCategory.lambdaUnit line 831