OAI/CategoryTheory/Thomason/BoundaryQuotients.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Boundary Quotients.

  1. def OAI.Thomason.OmegaCategory.boundarySetoid line 14
  2. abbrev OAI.Thomason.OmegaCategory.BoundaryQuotient.Cell line 21
  3. def OAI.Thomason.OmegaCategory.BoundaryQuotient.map line 22
  4. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.map_eq_iff line 23
  5. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.surjective line 25
  6. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.source_respects line 27
  7. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.target_respects line 37
  8. def OAI.Thomason.OmegaCategory.BoundaryQuotient.source line 47
  9. def OAI.Thomason.OmegaCategory.BoundaryQuotient.target line 48
  10. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.source_map line 49
  11. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.target_map line 50
  12. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.source_high line 52
  13. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.target_high line 56
  14. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.injective_on_lower line 61
  15. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.composable_low line 65
  16. def OAI.Thomason.OmegaCategory.BoundaryQuotient.comp line 72
  17. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.comp_map line 77
  18. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.comp_map_low line 109
  19. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.comp_high line 115
  20. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.high_composable line 119
  21. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.source_source line 123
  22. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.target_target line 127
  23. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.source_target line 131
  24. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.target_source line 135
  25. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.source_comp_le line 140
  26. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.target_comp_le line 148
  27. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.source_comp_gt line 157
  28. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.target_comp_gt line 167
  29. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.unit_left line 178
  30. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.unit_right line 185
  31. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.assoc line 193
  32. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.interchange line 206
  33. def OAI.Thomason.OmegaCategory.BoundaryQuotient.category line 223
  34. lemma OAI.Thomason.OmegaCategory.BoundaryQuotient.truncated line 242
  35. def OAI.Thomason.OmegaCategory.BoundaryQuotient.projection line 245
  36. lemma OAI.Thomason.OmegaCategory.truncationUnit_injective_below line 253
  37. lemma OAI.Thomason.OmegaCategory.truncationUnit_surjective line 263
  38. lemma OAI.Thomason.OmegaCategory.truncationUnit_surjective_nCells line 305
  39. lemma OAI.Thomason.OmegaCategory.truncationUnit_onCells_surjective line 323
  40. def OAI.Thomason.OmegaCategory.truncationCellLift line 332
  41. lemma OAI.Thomason.OmegaCategory.truncationCellLift_unit line 336
  42. lemma OAI.Thomason.OmegaCategory.truncationCellLift_map line 341
  43. lemma OAI.Thomason.OmegaCategory.truncationUnit_onCells_injective line 346
  44. lemma OAI.Thomason.OmegaCategory.truncationCellLift_of_unit line 352
  45. lemma OAI.Thomason.OmegaCategory.truncationCellLift_source_fixed line 356
  46. lemma OAI.Thomason.OmegaCategory.truncationCellLift_composable line 365
  47. lemma OAI.Thomason.OmegaCategory.truncationCellLift_comp line 375
  48. def OAI.Thomason.OmegaCategory.truncationLambdaRawRetraction line 386
  49. lemma OAI.Thomason.OmegaCategory.truncationLambdaRawRetraction_single line 390
  50. lemma OAI.Thomason.OmegaCategory.truncationLambdaRawRetraction_relations line 396
  51. def OAI.Thomason.OmegaCategory.truncationLambdaRetraction line 408
  52. lemma OAI.Thomason.OmegaCategory.truncationLambdaRetraction_gen line 413
  53. lemma OAI.Thomason.OmegaCategory.truncationLambdaRetraction_leftInverse line 419
  54. lemma OAI.Thomason.OmegaCategory.truncationUnit_lambdaMap_injective line 429
  55. def OAI.Thomason.liftedBasis line 449
  56. lemma OAI.Thomason.liftedBasis_cons line 462
  57. lemma OAI.Thomason.liftedBasis_unit line 471
  58. def OAI.Thomason.liftedChainMap line 486
  59. lemma OAI.Thomason.liftedChainMap_bracket line 490
  60. lemma OAI.Thomason.liftedChainMap_unit line 496
  61. lemma OAI.Thomason.liftedChainMap_d line 513
  62. lemma OAI.Thomason.liftedChainMap_aug line 532
  63. lemma OAI.Thomason.liftedBasis_positive line 545
  64. lemma OAI.Thomason.liftedChainMap_positive line 556
  65. def OAI.Thomason.liftedChainHom line 569
  66. lemma OAI.Thomason.atomCounitInverse_row line 576
  67. def OAI.Thomason.boundedOrientalLift line 585
  68. lemma OAI.Thomason.boundedOrientalLift_atom line 589
  69. lemma OAI.Thomason.boundedOrientalLift_unit line 661
  70. lemma OAI.Thomason.truncation_oriental_surjective line 671
  71. structure OAI.Thomason.DirectedComplex.PartialHom line 688
  72. def OAI.Thomason.DirectedComplex.PartialHom.table line 699
  73. lemma OAI.Thomason.DirectedComplex.PartialHom.table_bounded line 727
  74. lemma OAI.Thomason.DirectedComplex.PartialHom.table_source line 733
  75. lemma OAI.Thomason.DirectedComplex.PartialHom.table_target_lt line 739
  76. lemma OAI.Thomason.DirectedComplex.PartialHom.table_composable line 745
  77. lemma OAI.Thomason.DirectedComplex.PartialHom.table_comp_lt line 750
  78. lemma OAI.Thomason.DirectedComplex.PartialHom.table_source_n line 757