OAI/CategoryTheory/Thomason/DirectedPrisms.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Directed Prisms.

  1. structure OAI.Thomason.DirectedComplex.PositiveAntihomotopy line 16
  2. def OAI.Thomason.DirectedComplex.PositiveAntihomotopy.cylinderMap line 28
  3. def OAI.Thomason.DirectedComplex.PositiveAntihomotopy.cylinderHom line 38
  4. lemma OAI.Thomason.DirectedComplex.PositiveAntihomotopy.cylinderHom_endpoint_false line 65
  5. lemma OAI.Thomason.DirectedComplex.PositiveAntihomotopy.cylinderHom_endpoint_true line 71
  6. lemma OAI.Thomason.NormalizedChains.degreeSign_of_grade line 90
  7. lemma OAI.Thomason.NormalizedChains.prism_of_grade_zero line 107
  8. def OAI.Thomason.NormalizedChains.gradedPrism line 117
  9. def OAI.Thomason.RelativePrismData.antihomotopy line 137
  10. def OAI.Thomason.RelativePrismData.cylinderChainMap line 154
  11. lemma OAI.Thomason.RelativePrismData.cylinderChainMap_endpoint_false line 157
  12. lemma OAI.Thomason.RelativePrismData.cylinderChainMap_endpoint_true line 161
  13. def OAI.Thomason.RelativePrismData.tableCylinder line 165
  14. def OAI.Thomason.DirectedComplex.Hom.cylinderMap line 180
  15. def OAI.Thomason.DirectedComplex.Hom.cylinder line 190
  16. lemma OAI.Thomason.DirectedComplex.Hom.cylinder_id line 204
  17. lemma OAI.Thomason.DirectedComplex.Hom.cylinder_comp line 208
  18. lemma OAI.Thomason.DirectedComplex.Hom.cylinder_endpoint line 213
  19. lemma OAI.Thomason.DirectedComplex.Hom.cylinder_projection line 220
  20. lemma OAI.Thomason.NormalizedChains.map_prism line 239
  21. lemma OAI.Thomason.NormalizedChains.prism_stationary_map line 277
  22. lemma OAI.Thomason.RelativePrismData.cylinderChainMap_stationary line 313
  23. lemma OAI.Thomason.RelativePrismData.tableCylinder_stationary line 348
  24. def OAI.Thomason.DirectedComplex.PositiveAntihomotopy.precomp line 367
  25. def OAI.Thomason.DirectedComplex.PositiveAntihomotopy.postcomp line 376
  26. lemma OAI.Thomason.DirectedComplex.PositiveAntihomotopy.precomp_cylinderHom line 387
  27. lemma OAI.Thomason.DirectedComplex.PositiveAntihomotopy.postcomp_cylinderHom line 393
  28. def OAI.Thomason.RelativePrismData.simplexImage line 412
  29. lemma OAI.Thomason.RelativePrismData.simplexImage_finite line 415
  30. lemma OAI.Thomason.RelativePrismData.simplexImage_shape line 419
  31. lemma OAI.Thomason.RelativePrismData.simplexImage_bounded line 433
  32. lemma OAI.Thomason.RelativePrismData.simplexImage_total line 440
  33. abbrev OAI.Thomason.RelativePrismData.simplexImageLinearOrder line 452
  34. def OAI.Thomason.RelativePrismData.simplexImageLeft line 460
  35. def OAI.Thomason.RelativePrismData.simplexImageRight line 464
  36. def OAI.Thomason.RelativePrismData.simplexImageMap line 468
  37. def OAI.Thomason.NormalizedChains.wordEmbedding line 489
  38. lemma OAI.Thomason.NormalizedChains.map_orderEmbedding line 495
  39. lemma OAI.Thomason.NormalizedChains.map_orderEmbedding_injective line 508
  40. lemma OAI.Thomason.NormalizedChains.complexMap_orderEmbedding_injective line 514
  41. def OAI.Thomason.DirectedComplex.PositiveAntihomotopy.lift line 532
  42. def OAI.Thomason.RelativePrismData.simplexImageInclusion line 564
  43. def OAI.Thomason.RelativePrismData.simplexAntihomotopy line 567
  44. def OAI.Thomason.RelativePrismData.simplexCylinderChainMap line 595
  45. lemma OAI.Thomason.RelativePrismData.simplexCylinderChainMap_inclusion line 599
  46. lemma OAI.Thomason.RelativePrismData.simplexCylinderChainMap_naturality line 619
  47. structure OAI.Thomason.OmegaCategory.ThinCell line 657
  48. def OAI.Thomason.OmegaCategory.ThinCell.vertex line 667
  49. def OAI.Thomason.OmegaCategory.ThinCell.source line 669
  50. def OAI.Thomason.OmegaCategory.ThinCell.target line 673
  51. def OAI.Thomason.OmegaCategory.ThinCell.comp line 677
  52. lemma OAI.Thomason.OmegaCategory.ThinCell.source_zero line 683
  53. lemma OAI.Thomason.OmegaCategory.ThinCell.source_succ line 684
  54. lemma OAI.Thomason.OmegaCategory.ThinCell.target_zero line 685
  55. lemma OAI.Thomason.OmegaCategory.ThinCell.target_succ line 686
  56. lemma OAI.Thomason.OmegaCategory.ThinCell.vertex_left line 687
  57. lemma OAI.Thomason.OmegaCategory.ThinCell.vertex_right line 688
  58. lemma OAI.Thomason.OmegaCategory.ThinCell.comp_zero_left line 689
  59. lemma OAI.Thomason.OmegaCategory.ThinCell.comp_zero_right line 690
  60. lemma OAI.Thomason.OmegaCategory.ThinCell.comp_succ line 691
  61. def OAI.Thomason.OmegaCategory.thin line 695
  62. def OAI.Thomason.OmegaCategory.interval line 749
  63. def OAI.Thomason.OmegaCategory.chaotic line 752
  64. lemma OAI.Thomason.OmegaCategory.thin_truncated line 755