OAI/CategoryTheory/Thomason/PartialPrisms.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Partial Prisms.

  1. lemma OAI.Thomason.PartialNormalized.cutAtom_boundary line 16
  2. def OAI.Thomason.PartialNormalized.finiteCut line 73
  3. theorem OAI.Thomason.DirectedComplex.PartialHom.ext line 91
  4. def OAI.Thomason.DirectedComplex.PartialHom.precomp line 98
  5. lemma OAI.Thomason.DirectedComplex.PartialHom.precomp_table line 107
  6. lemma OAI.Thomason.DirectedComplex.PartialHom.precomp_image line 113
  7. lemma OAI.Thomason.PartialNormalized.homTotal_precomp line 130
  8. lemma OAI.Thomason.PartialNormalized.homVertex_precomp line 147
  9. lemma OAI.Thomason.PartialNormalized.cutWord_precomp line 154
  10. lemma OAI.Thomason.PartialNormalized.cutTotal_precomp line 166
  11. lemma OAI.Thomason.PartialNormalized.cutHom_precomp line 181
  12. lemma OAI.Thomason.simplexInverse_natural line 202
  13. lemma OAI.Thomason.liftedPartial_natural_below line 217
  14. lemma OAI.Thomason.PartialNormalized.homWord_congr_low line 244
  15. lemma OAI.Thomason.PartialNormalized.homTotal_congr_low line 253
  16. lemma OAI.Thomason.PartialNormalized.homVertex_congr_low line 267
  17. lemma OAI.Thomason.PartialNormalized.cutWord_congr_low line 275
  18. lemma OAI.Thomason.PartialNormalized.cutTotal_congr_low line 288
  19. lemma OAI.Thomason.PartialNormalized.cutWord_congr_append_one line 303
  20. lemma OAI.Thomason.PartialNormalized.cutTable_atom_congr line 310
  21. lemma OAI.Thomason.PartialNormalized.finiteCut_congr line 352
  22. def OAI.Thomason.finiteTableCut line 399
  23. lemma OAI.Thomason.finiteTableCut_natural line 405
  24. def OAI.Thomason.DirectedComplex.PartialHom.ofHom line 438
  25. lemma OAI.Thomason.DirectedComplex.PartialHom.ofHom_table line 444
  26. lemma OAI.Thomason.DirectedComplex.PartialHom.ofHom_image line 449
  27. lemma OAI.Thomason.PartialNormalized.cutWord_const_one line 468
  28. lemma OAI.Thomason.PartialNormalized.cutTotal_const_zero line 476
  29. lemma OAI.Thomason.PartialNormalized.cutTotal_const_one line 482
  30. lemma OAI.Thomason.PartialNormalized.cutHom_const_zero line 494
  31. lemma OAI.Thomason.PartialNormalized.cutHom_const_one line 503
  32. lemma OAI.Thomason.PartialNormalized.homVertex_ofHom line 512
  33. lemma OAI.Thomason.liftedPartial_of_nu_below line 534
  34. def OAI.Thomason.finiteTableNerveVertexMap line 560
  35. def OAI.Thomason.finitePosetTableNerveMap line 574
  36. lemma OAI.Thomason.finitePosetTableNerveMap_vertex line 578
  37. lemma OAI.Thomason.finiteTableCut_const_zero line 593
  38. lemma OAI.Thomason.finiteTableCut_const_one line 602
  39. def OAI.Thomason.finiteTableNerveCutCylinder line 614
  40. def OAI.Thomason.finiteTableNerveCutHomotopy line 623
  41. lemma OAI.Thomason.finiteTableNerveVertexMap_weakEquivalence line 646
  42. lemma OAI.Thomason.finitePosetTableNerveMap_weakEquivalence line 651
  43. lemma OAI.Thomason.posetCategorificationFiniteUnit_tableMap line 658
  44. theorem OAI.Thomason.posetCategorificationFiniteUnit_weakEquivalence line 671
  45. def OAI.Thomason.OmegaCategory.categorySkeletonObject line 695
  46. lemma OAI.Thomason.OmegaCategory.categorySkeletonObject_left line 697
  47. def OAI.Thomason.OmegaCategory.categoryToSkeleton line 702
  48. lemma OAI.Thomason.OmegaCategory.categorySkeleton_hom_left line 711
  49. lemma OAI.Thomason.OmegaCategory.categorySkeleton_hom_right line 716
  50. def OAI.Thomason.OmegaCategory.skeletonToCategory line 722
  51. lemma OAI.Thomason.OmegaCategory.categoryToSkeleton_comp line 738
  52. lemma OAI.Thomason.OmegaCategory.skeletonToCategory_comp line 744
  53. def OAI.Thomason.OmegaCategory.categorySkeletonIso line 758
  54. instance OAI.Thomason.OmegaCategory.(instance at line 764) line 764
  55. instance OAI.Thomason.OmegaCategory.(instance at line 766) line 766
  56. abbrev OAI.Thomason.OneCat.Interval line 777
  57. def OAI.Thomason.OneCat.endpoint line 778
  58. abbrev OAI.Thomason.OneCat.cylinder line 780
  59. def OAI.Thomason.OneCat.projection line 781
  60. lemma OAI.Thomason.OneCat.endpoint_natural line 782
  61. lemma OAI.Thomason.OneCat.projection_natural line 784
  62. lemma OAI.Thomason.OneCat.endpoint_projection line 786
  63. lemma OAI.Thomason.OneCat.pushout_deformation line 789