OAI/CategoryTheory/Thomason/PosetalColimits.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Posetal Colimits.

  1. lemma OAI.Thomason.KanLocal.local_colimit_nat line 17
  2. abbrev OAI.Thomason.SubdividedUnit.C line 78
  3. abbrev OAI.Thomason.SubdividedUnit.N line 79
  4. abbrev OAI.Thomason.SubdividedUnit.η line 80
  5. lemma OAI.Thomason.SubdividedUnit.nerve_attachment_mono line 82
  6. lemma OAI.Thomason.SubdividedUnit.unit_local_attachment line 97
  7. structure OAI.Thomason.PosetCoproduct.Piece line 163
  8. instance OAI.Thomason.PosetCoproduct.(instance at line 167) line 167
  9. def OAI.Thomason.PosetCoproduct.incl line 174
  10. def OAI.Thomason.PosetCoproduct.value line 177
  11. lemma OAI.Thomason.PosetCoproduct.label_const line 181
  12. lemma OAI.Thomason.PosetCoproduct.incl_value line 185
  13. def OAI.Thomason.PosetCoproduct.isColimit line 192
  14. def OAI.Thomason.PosetCoproduct.iso line 214
  15. lemma OAI.Thomason.PosetCoproduct.iso_hom_ι line 217
  16. def OAI.Thomason.PosetCoproduct.old line 223
  17. lemma OAI.Thomason.PosetCoproduct.old_lower line 224
  18. def OAI.Thomason.PosetCoproduct.oldIso line 227
  19. def OAI.Thomason.PosetCoproduct.oldNerveIso line 234
  20. lemma OAI.Thomason.PosetCoproduct.oldNerveIso_ι line 239
  21. lemma OAI.Thomason.PosetCoproduct.old_naturality line 245
  22. def OAI.Thomason.PosetCoproduct.oldUp line 257
  23. def OAI.Thomason.PosetCoproduct.oldRetraction line 262
  24. lemma OAI.Thomason.PosetCoproduct.oldRetraction_retract line 266
  25. lemma OAI.Thomason.PosetCoproduct.oldRetraction_adjunction line 274
  26. def OAI.Thomason.HornAttachments.oldSet line 293
  27. lemma OAI.Thomason.HornAttachments.oldSet_lower line 296
  28. def OAI.Thomason.HornAttachments.upwardToMeeting line 299
  29. def OAI.Thomason.HornAttachments.flagRetraction line 306
  30. lemma OAI.Thomason.HornAttachments.flagRetraction_retract line 310
  31. lemma OAI.Thomason.HornAttachments.flagRetraction_adjunction line 314
  32. def OAI.Thomason.HornAttachments.simplexFaces line 319
  33. def OAI.Thomason.HornAttachments.oldFlagsIso line 324
  34. lemma OAI.Thomason.HornAttachments.oldFlagsIso_naturality line 330
  35. abbrev OAI.Thomason.SubdividedUnit.D line 348
  36. def OAI.Thomason.SubdividedUnit.mappedCoprodIso line 350
  37. lemma OAI.Thomason.SubdividedUnit.mappedCoprodIso_ι line 354
  38. abbrev OAI.Thomason.SubdividedUnit.Faces line 364
  39. abbrev OAI.Thomason.SubdividedUnit.Flags line 365
  40. abbrev OAI.Thomason.SubdividedUnit.BoundaryFlags line 366
  41. def OAI.Thomason.SubdividedUnit.simplexCoprodIso line 369
  42. def OAI.Thomason.SubdividedUnit.boundaryCoprodIso line 373
  43. lemma OAI.Thomason.SubdividedUnit.simplexCoprodIso_ι line 379
  44. lemma OAI.Thomason.SubdividedUnit.boundaryCoprodIso_ι line 386
  45. lemma OAI.Thomason.SubdividedUnit.mappedCoprodIso_naturality line 394
  46. lemma OAI.Thomason.SubdividedUnit.boundaryCoprodIso_naturality line 409
  47. lemma OAI.Thomason.SubdividedUnit.unit_local_of_iso line 436
  48. lemma OAI.Thomason.SubdividedUnit.unit_local_initial line 446
  49. lemma OAI.Thomason.SubdividedUnit.boundary_unit_successor line 455
  50. lemma OAI.Thomason.SubdividedUnit.unit_local_skeleton line 487
  51. lemma OAI.Thomason.SubdividedUnit.skeleton_monos line 503
  52. theorem OAI.Thomason.SubdividedUnit.unit_local_one line 513
  53. theorem OAI.Thomason.SubdividedUnit.one line 544
  54. def OAI.Thomason.GeometricRecognition.Posetal.Property line 556
  55. def OAI.Thomason.GeometricRecognition.Posetal.IsPosetal line 559
  56. lemma OAI.Thomason.GeometricRecognition.Posetal.property_poset line 561
  57. lemma OAI.Thomason.GeometricRecognition.Posetal.property_iso line 567
  58. lemma OAI.Thomason.GeometricRecognition.Posetal.isPosetal_of_property line 578
  59. lemma OAI.Thomason.GeometricRecognition.Posetal.property_of_isPosetal line 587
  60. def OAI.Thomason.GeometricRecognition.Posetal.EdgeThin line 591
  61. def OAI.Thomason.GeometricRecognition.Posetal.EdgeAntisym line 594
  62. lemma OAI.Thomason.GeometricRecognition.Posetal.nerve_edgeThin line 597
  63. lemma OAI.Thomason.GeometricRecognition.Posetal.nerve_edgeAntisym line 606
  64. lemma OAI.Thomason.GeometricRecognition.Posetal.property_of_nerve_edges line 613
  65. lemma OAI.Thomason.GeometricRecognition.Posetal.edgeThin_of_mono line 624
  66. lemma OAI.Thomason.GeometricRecognition.Posetal.edgeAntisym_of_mono line 631
  67. lemma OAI.Thomason.GeometricRecognition.Posetal.eq_eventually line 644
  68. lemma OAI.Thomason.GeometricRecognition.Posetal.edgeThin_colimit line 650
  69. lemma OAI.Thomason.GeometricRecognition.Posetal.edgeAntisym_colimit line 684