OAI/CategoryTheory/Thomason/CylinderProfiles.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Cylinder Profiles.

  1. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_endpoint line 17
  2. def OAI.Thomason.GrayRecursive.IntervalHom.tensorParameter line 29
  3. def OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel line 32
  4. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorParameter_generator line 35
  5. lemma OAI.Thomason.GrayRecursive.IntervalHom.intervalLabel_cylinder_map line 45
  6. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_generator line 50
  7. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_endpoint line 55
  8. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_values line 60
  9. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_monotone line 64
  10. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_source line 67
  11. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_target line 76
  12. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_comp line 85
  13. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorLabel_comp_stationary line 95
  14. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_zero_faces_are_endpoints line 127
  15. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorEndpoint_injective line 181
  16. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorEndpoint_eq_iff line 189
  17. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_object_endpoint line 201
  18. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_object_reconstruct line 215
  19. lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_stationary line 229
  20. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_stationary_reconstruct line 246
  21. structure OAI.Thomason.DirectedComplex.PositiveAcyclic line 299
  22. def OAI.Thomason.DirectedComplex.CylinderTables.side line 308
  23. def OAI.Thomason.DirectedComplex.CylinderTables.cross line 312
  24. def OAI.Thomason.DirectedComplex.CylinderTables.project line 315
  25. def OAI.Thomason.DirectedComplex.CylinderTables.label line 317
  26. lemma OAI.Thomason.DirectedComplex.CylinderTables.project_row line 319
  27. lemma OAI.Thomason.DirectedComplex.CylinderTables.side_positive line 322
  28. lemma OAI.Thomason.DirectedComplex.CylinderTables.cross_positive line 328
  29. lemma OAI.Thomason.DirectedComplex.CylinderTables.cross_boundary line 331
  30. lemma OAI.Thomason.DirectedComplex.CylinderTables.left_boundary line 335
  31. lemma OAI.Thomason.DirectedComplex.CylinderTables.right_boundary line 342
  32. lemma OAI.Thomason.DirectedComplex.CylinderTables.augmentation_sides line 349
  33. lemma OAI.Thomason.DirectedComplex.CylinderTables.augmentation_cross line 353
  34. lemma OAI.Thomason.DirectedComplex.CylinderTables.label_truncate line 358
  35. lemma OAI.Thomason.DirectedComplex.CylinderTables.label_comp line 364
  36. lemma OAI.Thomason.DirectedComplex.CylinderTables.label_endpoint line 372
  37. lemma OAI.Thomason.DirectedComplex.CylinderTables.label_cylinder_map line 378
  38. lemma OAI.Thomason.DirectedComplex.CylinderTables.label_values line 384
  39. lemma OAI.Thomason.DirectedComplex.CylinderTables.label_monotone line 392
  40. lemma OAI.Thomason.DirectedComplex.CylinderTables.cross_zero_of_stationary line 397
  41. lemma OAI.Thomason.DirectedComplex.CylinderTables.side_zero_of_empty line 406
  42. lemma OAI.Thomason.DirectedComplex.CylinderTables.stationary_reconstruct line 418
  43. lemma OAI.Thomason.DirectedComplex.CylinderTables.endpoint_or_crossing line 447
  44. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_augmentation line 462
  45. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_starts_ends line 466
  46. theorem OAI.Thomason.NormalizedChains.complexPositiveAcyclic line 489
  47. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_label line 510
  48. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_project line 541
  49. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_endpoint_apply line 545
  50. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_endpoint_fiber line 549
  51. lemma OAI.Thomason.GrayRecursive.IntervalHom.tensor_endpoint_or_crossing line 567
  52. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_injective_of_crossing line 581
  53. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_surjective_of_crossing line 597
  54. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_objects_bijective line 607
  55. lemma OAI.Thomason.DirectedComplex.CylinderTables.side_of_row_zero line 643
  56. lemma OAI.Thomason.DirectedComplex.CylinderTables.cross_of_row_zero line 649
  57. def OAI.Thomason.DirectedComplex.CylinderTables.crossingProfile line 652
  58. def OAI.Thomason.DirectedComplex.CylinderTables.leftProfileRow line 662
  59. def OAI.Thomason.DirectedComplex.CylinderTables.rightProfileRow line 665
  60. lemma OAI.Thomason.DirectedComplex.CylinderTables.left_d line 668
  61. lemma OAI.Thomason.DirectedComplex.CylinderTables.right_d line 672
  62. lemma OAI.Thomason.DirectedComplex.CylinderTables.leftProfileRow_boundary line 676
  63. lemma OAI.Thomason.DirectedComplex.CylinderTables.rightProfileRow_boundary line 684
  64. def OAI.Thomason.DirectedComplex.CylinderTables.leftProfile line 692
  65. def OAI.Thomason.DirectedComplex.CylinderTables.rightProfile line 714
  66. lemma OAI.Thomason.DirectedComplex.CylinderTables.side_cylinder_map line 734
  67. lemma OAI.Thomason.DirectedComplex.CylinderTables.cross_cylinder_map line 739
  68. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossingProfile_natural line 742
  69. lemma OAI.Thomason.DirectedComplex.CylinderTables.leftProfile_natural line 747
  70. lemma OAI.Thomason.DirectedComplex.CylinderTables.rightProfile_natural line 756
  71. lemma OAI.Thomason.DirectedComplex.CylinderTables.project_profiles line 765
  72. lemma OAI.Thomason.DirectedComplex.CylinderTables.crossing_profiles_ext line 774