OAI/CategoryTheory/Thomason/FiberComparisons.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Fiber Comparisons.

  1. lemma OAI.Thomason.OmegaCategory.oneFiberConeHomEquiv_old line 17
  2. lemma OAI.Thomason.OmegaCategory.oneFiberFiniteConeHomEquiv_old line 36
  3. lemma OAI.Thomason.OmegaCategory.truncationOneFiberIso_inv_app line 57
  4. lemma OAI.Thomason.OmegaCategory.truncationFiberIso_inv_app line 97
  5. lemma OAI.Thomason.OmegaCategory.truncationFiberIso_inv_inclusion line 106
  6. lemma OAI.Thomason.NormalizedChains.PosetTables.truncationTableFiberIso_inclusion line 128
  7. def OAI.Thomason.categorificationSimplexDiagram line 153
  8. def OAI.Thomason.categorificationSimplexCocone line 157
  9. def OAI.Thomason.categorificationSimplexIsColimit line 163
  10. def OAI.Thomason.categorificationFiniteSimplexIsColimit line 168
  11. def OAI.Thomason.labelledSimplexIsColimit line 172
  12. def OAI.Thomason.labelledSimplexFiberIsColimit line 177
  13. def OAI.Thomason.labelledFiniteSimplexIsColimit line 188
  14. def OAI.Thomason.labelledFiniteSimplexFiberIsColimit line 194
  15. def OAI.Thomason.posetSimplexOrder line 220
  16. def OAI.Thomason.posetTableNerveMap line 223
  17. lemma OAI.Thomason.posetTableNerveMap_natural line 234
  18. def OAI.Thomason.posetCategorificationTableMap line 245
  19. lemma OAI.Thomason.posetCategorificationTableMap_natural line 249
  20. def OAI.Thomason.posetCategorificationLabel line 264
  21. lemma OAI.Thomason.posetCategorificationLabel_natural line 268
  22. lemma OAI.Thomason.categorification_homEquiv_app line 287
  23. lemma OAI.Thomason.posetCategorificationTableMap_leg line 304
  24. lemma OAI.Thomason.posetCategorificationTableMap_leg_lifted line 319
  25. lemma OAI.Thomason.posetCategorificationLabel_leg line 332
  26. instance OAI.Thomason.categorificationSimplexLeg_isIso line 357
  27. instance OAI.Thomason.posetCategorificationTableMap_ordinal_isIso line 368
  28. def OAI.Thomason.posetComplexFunctor line 390
  29. lemma OAI.Thomason.posetCategorificationTableMap_isIso_of_orderIso line 396
  30. theorem OAI.Thomason.posetCategorificationTableMap_finiteLinear_isIso line 409
  31. def OAI.Thomason.emptyOmegaIsInitial line 435
  32. def OAI.Thomason.emptyPosetNerveIsInitial line 446
  33. theorem OAI.Thomason.posetCategorificationTableMap_empty_isIso line 462
  34. theorem OAI.Thomason.posetCategorificationTableMap_finiteLinear_isIso_all line 469
  35. def OAI.Thomason.posetLevelInclusion line 490
  36. lemma OAI.Thomason.posetCategorification_level_mem line 493
  37. def OAI.Thomason.posetCategorificationFiberMap line 507
  38. lemma OAI.Thomason.posetCategorificationFiberMap_inclusion line 514
  39. def OAI.Thomason.posetCategorificationTableOver line 533
  40. def OAI.Thomason.posetCategorificationTableFiberMap line 537
  41. lemma OAI.Thomason.posetCategorificationFiberMap_table_fac line 542
  42. theorem OAI.Thomason.posetCategorificationFiberMap_finiteLinear_isIso line 551
  43. def OAI.Thomason.posetCategorificationFiniteFiberMap line 579
  44. lemma OAI.Thomason.posetCategorificationFiniteFiberMap_inclusion line 587
  45. theorem OAI.Thomason.posetCategorificationFiniteFiberMap_finiteLinear_isIso line 600
  46. def OAI.Thomason.posetLevelMap line 623
  47. lemma OAI.Thomason.posetLevelMap_inclusion line 628
  48. def OAI.Thomason.posetCategorificationOverMap line 632
  49. lemma OAI.Thomason.posetCategorificationFiberMap_natural line 638
  50. lemma OAI.Thomason.posetCategorificationFiniteFiberMap_natural line 661
  51. def OAI.Thomason.posetCategorificationFiberIsoFinite line 703
  52. lemma OAI.Thomason.posetCategorificationFiberIsoFinite_hom line 711
  53. lemma OAI.Thomason.posetCategorificationFiberMap_inverse_natural line 715