OAI/CategoryTheory/Thomason/KanQuillen.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Kan Quillen.

  1. lemma OAI.Thomason.GeometricRecognition.strictFiber_isPullback line 14
  2. lemma OAI.Thomason.GeometricRecognition.sequential_colimit_lifting line 37
  3. lemma OAI.Thomason.GeometricRecognition.exStageMap_fibration line 64
  4. theorem OAI.Thomason.GeometricRecognition.exInfinity_fibration line 70
  5. lemma OAI.Thomason.GeometricRecognition.weak_kan_fibration_rlp line 89
  6. theorem OAI.Thomason.GeometricRecognition.weak_fibration_rlp line 94
  7. theorem OAI.Thomason.GeometricRecognition.boundary_right_class line 110
  8. lemma OAI.Thomason.KanQuillen.anodyne_class line 128
  9. lemma OAI.Thomason.KanQuillen.first_wfs line 141
  10. lemma OAI.Thomason.KanQuillen.second_wfs line 145
  11. def OAI.Thomason.KanQuillen.geometricModel line 149
  12. def OAI.Thomason.DependentPosets.incl line 171
  13. def OAI.Thomason.DependentPosets.componentIso line 175
  14. lemma OAI.Thomason.DependentPosets.label_const line 185
  15. def OAI.Thomason.DependentPosets.restricted line 189
  16. def OAI.Thomason.DependentPosets.branch line 194
  17. lemma OAI.Thomason.DependentPosets.incl_branch line 198
  18. def OAI.Thomason.DependentPosets.isColimit line 205
  19. def OAI.Thomason.DependentPosets.iso line 227
  20. lemma OAI.Thomason.DependentPosets.iso_hom_ι line 230
  21. def OAI.Thomason.DependentPosets.old line 235
  22. lemma OAI.Thomason.DependentPosets.old_lower line 236
  23. def OAI.Thomason.DependentPosets.oldIso line 242
  24. def OAI.Thomason.DependentPosets.oldNerveIso line 259
  25. lemma OAI.Thomason.DependentPosets.oldNerveIso_ι line 264
  26. lemma OAI.Thomason.DependentPosets.old_naturality line 273
  27. lemma OAI.Thomason.DependentPosets.mem_upward_old line 285
  28. def OAI.Thomason.DependentPosets.oldUp line 295
  29. def OAI.Thomason.DependentPosets.oldRetraction line 298
  30. lemma OAI.Thomason.DependentPosets.oldRetraction_retract line 307
  31. lemma OAI.Thomason.DependentPosets.oldRetraction_adjunction line 315
  32. structure OAI.Thomason.TransferAcyclicity.PosetAttachment line 343
  33. abbrev OAI.Thomason.TransferAcyclicity.PosetAttachment.arrow line 356
  34. def OAI.Thomason.TransferAcyclicity.Admissible line 358
  35. instance OAI.Thomason.TransferAcyclicity.(instance at line 361) line 361
  36. lemma OAI.Thomason.TransferAcyclicity.horn_admissible line 366
  37. def OAI.Thomason.TransferAcyclicity.sumData line 392
  38. def OAI.Thomason.TransferAcyclicity.posetCoprodIso line 412
  39. def OAI.Thomason.TransferAcyclicity.oldCoprodIso line 417
  40. lemma OAI.Thomason.TransferAcyclicity.posetCoprodIso_ι line 421
  41. lemma OAI.Thomason.TransferAcyclicity.oldCoprodIso_ι line 428
  42. lemma OAI.Thomason.TransferAcyclicity.coprod_inc line 440
  43. instance OAI.Thomason.TransferAcyclicity.admissible_coproducts line 466
  44. instance OAI.Thomason.TransferAcyclicity.(instance at line 489) line 489
  45. lemma OAI.Thomason.TransferAcyclicity.poset_attachment_local line 491
  46. lemma OAI.Thomason.TransferAcyclicity.admissible_pushout line 522
  47. lemma OAI.Thomason.TransferAcyclicity.coproduct_horn_pushout line 539
  48. def OAI.Thomason.TransferAcyclicity.OneStatement line 559
  49. lemma OAI.Thomason.TransferAcyclicity.sequential_horn_weak line 573
  50. theorem OAI.Thomason.TransferAcyclicity.one line 625
  51. def OAI.Thomason.FirstTransferredWFS.OneStatement line 642
  52. lemma OAI.Thomason.FirstTransferredWFS.leftClass_one line 657
  53. theorem OAI.Thomason.FirstTransferredWFS.one line 676
  54. lemma OAI.Thomason.boundaryImages_right_class line 690
  55. lemma OAI.Thomason.transferred_second_wfs line 697
  56. def OAI.Thomason.modelOne line 706
  57. lemma OAI.Thomason.modelOne_weak line 722
  58. lemma OAI.Thomason.modelOne_fib line 724
  59. lemma OAI.Thomason.modelOne_cof line 726
  60. def OAI.Thomason.ModelStructuresOneStatement line 729
  61. theorem OAI.Thomason.modelStructuresOne line 736
  62. lemma OAI.Thomason.GeometricRecognition.weak_local line 750
  63. lemma OAI.Thomason.GeometricRecognition.weak_kan_heq line 759
  64. theorem OAI.Thomason.GeometricRecognition.left_proper line 771
  65. theorem OAI.Thomason.GeometricRecognition.right_proper line 777
  66. def OAI.Thomason.QuillenCriterion.OneStatement line 796
  67. lemma OAI.Thomason.QuillenCriterion.sdEx_unit_weak line 811
  68. lemma OAI.Thomason.QuillenCriterion.sdExSquared_unit_weak line 819
  69. lemma OAI.Thomason.QuillenCriterion.unit_one_weak line 828
  70. theorem OAI.Thomason.QuillenCriterion.one line 837