OAI/CategoryTheory/Thomason/Globes.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

Globes.

  1. def OAI.Thomason.OmegaCategory.globePresentation line 16
  2. def OAI.Thomason.OmegaCategory.globe line 21
  3. def OAI.Thomason.OmegaCategory.globeGenerator line 23
  4. lemma OAI.Thomason.OmegaCategory.globeGenerator_bounded line 26
  5. def OAI.Thomason.OmegaCategory.globeLift line 30
  6. lemma OAI.Thomason.OmegaCategory.globeLift_generator line 34
  7. lemma OAI.Thomason.OmegaCategory.globe_functor_ext line 37
  8. lemma OAI.Thomason.OmegaCategory.globe_map_bounded line 44
  9. lemma OAI.Thomason.OmegaCategory.FilteredColimit.globe_functor_lift line 52
  10. lemma OAI.Thomason.OmegaCategory.FilteredColimit.globe_functor_equality line 69
  11. def OAI.Thomason.OmegaCategory.FilteredColimit.globeHomIsColimit line 78
  12. instance OAI.Thomason.OmegaCategory.FilteredColimit.globeHomPreservesColimit line 87
  13. instance OAI.Thomason.OmegaCategory.globe_finitelyPresentable line 95
  14. def OAI.Thomason.OmegaCategory.isoOfBijective line 113
  15. lemma OAI.Thomason.OmegaCategory.injective_of_mono line 143
  16. lemma OAI.Thomason.OmegaCategory.globes_separating line 155
  17. lemma OAI.Thomason.OmegaCategory.globes_strongGenerator line 163
  18. instance OAI.Thomason.OmegaCategory.locallyFinitelyPresentable line 177
  19. instance OAI.Thomason.OmegaCategory.locallyPresentable line 184
  20. lemma OAI.Thomason.OmegaCategory.FilteredColimit.omega_truncated line 203
  21. def OAI.Thomason.OmegaCategory.FilteredColimit.nCocone line 211
  22. def OAI.Thomason.OmegaCategory.FilteredColimit.nIsColimit line 217
  23. instance OAI.Thomason.OmegaCategory.FilteredColimit.nInclusion_preservesFilteredColimit line 223
  24. instance OAI.Thomason.OmegaCategory.nInclusion_finitelyAccessible line 232
  25. instance OAI.Thomason.OmegaCategory.nCategory_locallyFinitelyPresentable line 238
  26. instance OAI.Thomason.OmegaCategory.nCategory_locallyPresentable line 242
  27. lemma OAI.Thomason.SmallObject.commonPresentabilityCardinal line 257
  28. lemma OAI.Thomason.SmallObject.smallObjectArgument line 273
  29. lemma OAI.Thomason.SmallObject.weakFactorizationSystem line 291
  30. instance OAI.Thomason.boundaryImages_small line 310
  31. instance OAI.Thomason.hornImages_small line 315
  32. lemma OAI.Thomason.hornImages_rlp line 323
  33. lemma OAI.Thomason.boundaryImages_rlp line 343
  34. instance OAI.Thomason.boundaryImages_smallObject line 355
  35. instance OAI.Thomason.hornImages_smallObject line 360
  36. lemma OAI.Thomason.boundaryImages_weakFactorization line 365
  37. lemma OAI.Thomason.hornImages_weakFactorization line 370
  38. lemma OAI.Thomason.thomasonFibrations_weakFactorization line 375
  39. lemma OAI.Thomason.thomasonFibrationsFinite_weakFactorization line 380
  40. lemma OAI.Thomason.thomasonBoundary_weakFactorization line 386
  41. lemma OAI.Thomason.thomasonBoundaryFinite_weakFactorization line 390
  42. def OAI.Thomason.CubeExtension.radius line 408
  43. lemma OAI.Thomason.CubeExtension.abs_le_radius line 411
  44. lemma OAI.Thomason.CubeExtension.radius_nonneg line 414
  45. lemma OAI.Thomason.CubeExtension.radius_le_one line 417
  46. lemma OAI.Thomason.CubeExtension.continuous_radius line 423
  47. lemma OAI.Thomason.CubeExtension.radius_eq_one_iff line 428
  48. def OAI.Thomason.CubeExtension.denominator line 444
  49. lemma OAI.Thomason.CubeExtension.half_le_denominator line 446
  50. lemma OAI.Thomason.CubeExtension.denominator_pos line 450
  51. lemma OAI.Thomason.CubeExtension.denominator_le_one line 453
  52. lemma OAI.Thomason.CubeExtension.continuous_denominator line 456
  53. def OAI.Thomason.CubeExtension.retractTime line 460
  54. def OAI.Thomason.CubeExtension.retractSpace line 473
  55. lemma OAI.Thomason.CubeExtension.continuous_retractTime line 486
  56. lemma OAI.Thomason.CubeExtension.continuous_retractSpace line 491
  57. def OAI.Thomason.CubeExtension.roof line 499
  58. lemma OAI.Thomason.CubeExtension.retract_mem_roof line 501
  59. def OAI.Thomason.CubeExtension.retract line 533
  60. lemma OAI.Thomason.CubeExtension.denominator_eq_one_of_roof line 537
  61. lemma OAI.Thomason.CubeExtension.retract_fixed line 546
  62. def OAI.Thomason.CubeExtension.closedPaste line 574
  63. lemma OAI.Thomason.CubeExtension.closedPaste_left line 591
  64. lemma OAI.Thomason.CubeExtension.closedPaste_right line 598
  65. def OAI.Thomason.CubeExtension.glue line 608
  66. lemma OAI.Thomason.CubeExtension.glue_bottom line 630
  67. lemma OAI.Thomason.CubeExtension.glue_side line 635
  68. def OAI.Thomason.CubeExtension.extend line 641
  69. lemma OAI.Thomason.CubeExtension.extend_bottom line 647
  70. lemma OAI.Thomason.CubeExtension.extend_side line 655
  71. lemma OAI.Thomason.CubeExtension.extend_natural line 665
  72. def OAI.Thomason.CubeExtension.interpolate line 675
  73. lemma OAI.Thomason.CubeExtension.interpolate_zero line 689
  74. lemma OAI.Thomason.CubeExtension.interpolate_one line 695
  75. lemma OAI.Thomason.CubeExtension.interpolate_fixed line 701
  76. lemma OAI.Thomason.CubeExtension.extend_congr_at line 722
  77. lemma OAI.Thomason.CubeExtension.extend_eq_of_restrictions line 736
  78. def OAI.Thomason.CubeExtension.move line 757
  79. lemma OAI.Thomason.CubeExtension.move_bottom line 765
  80. lemma OAI.Thomason.CubeExtension.move_side line 769
  81. def OAI.Thomason.CubeExtension.transportLoop line 773
  82. lemma OAI.Thomason.CubeExtension.move_eq_of_restrictions line 778
  83. lemma OAI.Thomason.CubeExtension.transportLoop_homotopic_of_homotopy line 786
  84. lemma OAI.Thomason.CubeExtension.transportLoop_homotopic line 809
  85. lemma OAI.Thomason.CubeExtension.transportLoop_reverse line 838
  86. def OAI.Thomason.CubeExtension.transport line 851
  87. lemma OAI.Thomason.CubeExtension.transport_reverse line 855
  88. lemma OAI.Thomason.CubeExtension.transport_bijective line 860