OAI/CategoryTheory/Thomason/CoherentGluing.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Coherent Gluing.

  1. lemma OAI.Thomason.KanLocal.heq_id line 17
  2. lemma OAI.Thomason.KanLocal.heq_of_isIso line 20
  3. lemma OAI.Thomason.KanLocal.heq_comp line 26
  4. lemma OAI.Thomason.KanLocal.heq_homotopic line 39
  5. lemma OAI.Thomason.KanLocal.heq_of_rlp line 45
  6. lemma OAI.Thomason.KanLocal.pre_rlp_of_anodyne line 68
  7. def OAI.Thomason.KanLocal.Local line 80
  8. lemma OAI.Thomason.KanLocal.local_anodyne line 83
  9. lemma OAI.Thomason.KanLocal.local_iso line 86
  10. lemma OAI.Thomason.KanLocal.local_comp line 91
  11. def OAI.Thomason.KanLocal.preHomotopyMap line 96
  12. lemma OAI.Thomason.KanLocal.preHomotopyMap_zero line 100
  13. lemma OAI.Thomason.KanLocal.preHomotopyMap_one line 109
  14. def OAI.Thomason.KanLocal.preHomotopy line 118
  15. lemma OAI.Thomason.KanLocal.homotopic_pre_map line 128
  16. lemma OAI.Thomason.KanLocal.local_homotopic line 136
  17. lemma OAI.Thomason.KanLocal.local_heq line 139
  18. def OAI.Thomason.KanLocal.uncurryHomotopy line 146
  19. def OAI.Thomason.KanLocal.curryHomotopy line 156
  20. lemma OAI.Thomason.KanLocal.homotopic_uncurry line 168
  21. lemma OAI.Thomason.KanLocal.homotopic_curry line 176
  22. lemma OAI.Thomason.KanLocal.homotopic_uncurry' line 184
  23. lemma OAI.Thomason.KanLocal.homotopic_curry' line 188
  24. lemma OAI.Thomason.KanLocal.uncurry'_pre line 192
  25. lemma OAI.Thomason.KanLocal.curry'_pre line 198
  26. lemma OAI.Thomason.KanLocal.precomp_surjective line 203
  27. lemma OAI.Thomason.KanLocal.precomp_injective line 210
  28. lemma OAI.Thomason.KanLocal.local_weak line 221
  29. lemma OAI.Thomason.KanLocal.heq_of_precomp line 253
  30. lemma OAI.Thomason.KanLocal.heq_of_postcomp line 262
  31. lemma OAI.Thomason.KanLocal.homotopy_of_anodyne_eq_relative line 271
  32. lemma OAI.Thomason.KanLocal.anodyne_deformation line 303
  33. lemma OAI.Thomason.KanLocal.heq_anodyne line 312
  34. lemma OAI.Thomason.KanLocal.pullback_anodyne_heq line 319
  35. lemma OAI.Thomason.KanLocal.pullback_heq line 356
  36. lemma OAI.Thomason.KanLocal.local_pushout line 387
  37. lemma OAI.Thomason.KanLocal.local_pushout_map line 400
  38. lemma OAI.Thomason.OneCat.cylinderMap_pre line 421
  39. lemma OAI.Thomason.OneCat.cylinderMap_post line 430
  40. lemma OAI.Thomason.OneCat.cylinderMap_projection line 439
  41. lemma OAI.Thomason.OneCat.pushout_deformation_coherent line 447
  42. lemma OAI.Thomason.OneCat.nerve_pushout_coherent line 481
  43. def OAI.Thomason.CoherentGluing.Coherent line 559
  44. lemma OAI.Thomason.CoherentGluing.coherent_of_postIso line 563
  45. def OAI.Thomason.OneCat.orderMapCylinder line 592
  46. def OAI.Thomason.OneCat.posetMapCylinder line 602
  47. lemma OAI.Thomason.OneCat.posetMapCylinder_zero line 607
  48. lemma OAI.Thomason.OneCat.posetMapCylinder_one line 611
  49. lemma OAI.Thomason.OneCat.posetMapCylinder_stationary line 615
  50. lemma OAI.Thomason.OneCat.posetMapRetraction line 624
  51. lemma OAI.Thomason.OneCat.nerve_categorification_attach line 639
  52. lemma OAI.Thomason.OneCat.finite_poset_comparison_coherent line 647
  53. abbrev OAI.Thomason.AttachmentComparison.posetObj line 715
  54. abbrev OAI.Thomason.AttachmentComparison.posetMap line 718
  55. abbrev OAI.Thomason.AttachmentComparison.sb line 721
  56. abbrev OAI.Thomason.AttachmentComparison.inc line 724
  57. lemma OAI.Thomason.AttachmentComparison.sb_inc line 728
  58. lemma OAI.Thomason.AttachmentComparison.attachment_nerve_cover line 733
  59. lemma OAI.Thomason.AttachmentComparison.poset_nerve_cover line 781