OAI/CategoryTheory/Thomason/SieveAttachments.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Sieve Attachments.

  1. def OAI.Thomason.OneCat.liftInterval line 14
  2. def OAI.Thomason.OneCat.cylinderMap line 18
  3. lemma OAI.Thomason.OneCat.cylinderMap_zero line 28
  4. lemma OAI.Thomason.OneCat.cylinderMap_one line 35
  5. def OAI.Thomason.OneCat.homotopy line 43
  6. lemma OAI.Thomason.OneCat.retract_le line 69
  7. def OAI.Thomason.OneCat.orderCylinder line 71
  8. def OAI.Thomason.OneCat.posetCylinder line 81
  9. lemma OAI.Thomason.OneCat.posetCylinder_zero line 86
  10. lemma OAI.Thomason.OneCat.posetCylinder_one line 90
  11. lemma OAI.Thomason.OneCat.posetCylinder_stationary line 94
  12. lemma OAI.Thomason.OneCat.posetRetraction line 104
  13. def OAI.Thomason.OneCat.nerveOfCategoryIso line 119
  14. instance OAI.Thomason.OneCat.oneUnitCatIso line 122
  15. def OAI.Thomason.OneCat.categorificationCatIso line 127
  16. lemma OAI.Thomason.OneCat.categorificationCatIso_nerve line 132
  17. lemma OAI.Thomason.OneCat.categorificationCatIso_natural line 138
  18. lemma OAI.Thomason.OneCat.poset_pushout_nerve_weak line 163
  19. theorem OAI.Thomason.couniversalOne line 193
  20. theorem OAI.Thomason.labelled_poset_attachment line 235
  21. def OAI.Thomason.posetCategorificationFiniteLabel line 272
  22. theorem OAI.Thomason.labelled_poset_finite_attachment line 277
  23. def OAI.Thomason.OmegaCategory.constantLabel line 324
  24. lemma OAI.Thomason.OmegaCategory.comp_constantLabel line 330
  25. def OAI.Thomason.OmegaCategory.constantFiberIso line 333
  26. lemma OAI.Thomason.OmegaCategory.fiberInclusion_label line 340
  27. theorem OAI.Thomason.OmegaCategory.endpoint_attachment line 347
  28. def OAI.Thomason.posetPieceFiberIso line 390
  29. lemma OAI.Thomason.posetPieceFiberIso_inclusion line 397
  30. theorem OAI.Thomason.poset_sieve_attachment line 405
  31. def OAI.Thomason.OmegaCategory.constantFiniteFiberIso line 440
  32. theorem OAI.Thomason.OmegaCategory.endpoint_finite_attachment line 448
  33. def OAI.Thomason.posetPieceFiniteFiberIso line 495
  34. lemma OAI.Thomason.posetPieceFiniteFiberIso_inclusion line 505
  35. theorem OAI.Thomason.poset_finite_sieve_attachment line 514
  36. lemma OAI.Thomason.OmegaCategory.Subcategory.inclusion_mono line 551
  37. def OAI.Thomason.Attachments.subposetMap line 570
  38. def OAI.Thomason.Attachments.IsPosetAttachmentPiece line 573
  39. def OAI.Thomason.Attachments.IsPosetNewPiece line 584
  40. lemma OAI.Thomason.Attachments.posetLabel_constant line 593
  41. def OAI.Thomason.Attachments.constantAttachmentLabel line 607
  42. lemma OAI.Thomason.Attachments.constantAttachmentLabel_old line 612
  43. lemma OAI.Thomason.Attachments.constantAttachmentLabel_new line 614
  44. lemma OAI.Thomason.Attachments.subposetMap_comp line 617
  45. lemma OAI.Thomason.Attachments.constant_attachment_old_piece line 624
  46. lemma OAI.Thomason.Attachments.constant_attachment_new_piece line 669
  47. lemma OAI.Thomason.Attachments.tableLabel_objects line 711
  48. lemma OAI.Thomason.Attachments.posetLabel_objects line 721
  49. lemma OAI.Thomason.Attachments.interval_vertex_mem_old line 728
  50. lemma OAI.Thomason.Attachments.interval_vertex_mem_new line 733
  51. lemma OAI.Thomason.Attachments.labelled_objects_cover line 743
  52. lemma OAI.Thomason.Attachments.maxLabel_objects_fiber line 764
  53. lemma OAI.Thomason.Attachments.minLabel_objects_fiber line 773
  54. lemma OAI.Thomason.Attachments.comp_maxLabel line 782
  55. lemma OAI.Thomason.Attachments.comp_minLabel line 784
  56. theorem OAI.Thomason.Attachments.sieve_attachment_covers line 798