OAI/CategoryTheory/Globular/LinearShape.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Grothendieck.Shape.linearHeight line 11
  2. theorem OAI.Grothendieck.Shape.linearHeight_lt line 13
  3. theorem OAI.Grothendieck.Shape.linear_adjacent_realization line 18
  4. theorem OAI.Grothendieck.Shape.linear_face_low line 24
  5. theorem OAI.Grothendieck.Shape.linear_face_center line 46
  6. theorem OAI.Grothendieck.Shape.linear_face_top line 68
  7. theorem OAI.Grothendieck.Shape.linear_face_top_low line 77
  8. theorem OAI.Grothendieck.Shape.isPushout_attach line 90
  9. theorem OAI.Grothendieck.GlobularTheory.composition_isPushout line 103
  10. def OAI.Grothendieck.GlobularTheory.triplePrefix line 110
  11. theorem OAI.Grothendieck.GlobularTheory.triple_isPushout line 113
  12. def OAI.Grothendieck.GlobularTheory.tripleDesc line 117
  13. theorem OAI.Grothendieck.GlobularTheory.tripleDesc_first line 125
  14. theorem OAI.Grothendieck.GlobularTheory.tripleDesc_middle line 131
  15. theorem OAI.Grothendieck.GlobularTheory.tripleDesc_last line 137
  16. theorem OAI.Grothendieck.GlobularTheory.triple_hom_ext line 142
  17. def OAI.Grothendieck.Shape.lastArrow line 157
  18. abbrev OAI.Grothendieck.Shape.appendTwo line 159
  19. def OAI.Grothendieck.Shape.appendTwoOld line 163
  20. def OAI.Grothendieck.Shape.appendTwoMiddle line 168
  21. def OAI.Grothendieck.Shape.appendTwoLast line 173
  22. def OAI.Grothendieck.Shape.appendTwoTail line 177
  23. theorem OAI.Grothendieck.Shape.appendTwoTail_first line 192
  24. theorem OAI.Grothendieck.Shape.appendTwoTail_middle line 196
  25. theorem OAI.Grothendieck.Shape.appendTwoTail_last line 200
  26. theorem OAI.Grothendieck.Shape.appendTwo_isPushout line 204
  27. theorem OAI.Grothendieck.threeChain_pushout line 248
  28. theorem OAI.Grothendieck.Shape.composition_realization_isPushout line 296
  29. theorem OAI.Grothendieck.Shape.triple_realization_isPushout line 306
  30. theorem OAI.Grothendieck.Shape.appendTwo_realization_isPushout line 311
  31. abbrev OAI.Grothendieck.Shape.appendThree line 323
  32. def OAI.Grothendieck.Shape.appendThreeOld line 326
  33. def OAI.Grothendieck.Shape.appendThreeTail line 330
  34. theorem OAI.Grothendieck.Shape.appendThree_realization_isPushout line 333
  35. theorem OAI.Grothendieck.Shape.linearBlock_gt line 343
  36. theorem OAI.Grothendieck.Shape.face_lastArrow_transport line 354
  37. theorem OAI.Grothendieck.Shape.linear_face_below line 360
  38. def OAI.Grothendieck.pushoutSpanIso line 389
  39. theorem OAI.Grothendieck.pushoutSpanIso_inl line 397
  40. theorem OAI.Grothendieck.pushoutSpanIso_inr line 407
  41. instance OAI.Grothendieck.preservesColimits_linearization line 417
  42. structure OAI.Grothendieck.Table.LinearData line 423
  43. def OAI.Grothendieck.Table.LinearData.globe line 432
  44. def OAI.Grothendieck.Table.LinearData.extend line 441
  45. theorem OAI.Grothendieck.Table.LinearData.seam_below line 475
  46. theorem OAI.Grothendieck.Table.lastArrow_isIso_globe line 496
  47. theorem OAI.Grothendieck.Table.linearBlock_lastArrow_isIso line 502
  48. def OAI.Grothendieck.Table.reindex line 509
  49. def OAI.Grothendieck.Table.reindexIso line 511
  50. theorem OAI.Grothendieck.Table.reindexIso_last line 516
  51. theorem OAI.Grothendieck.Table.lastArrow_transport line 524
  52. def OAI.Grothendieck.Table.LinearData.attachLow line 533
  53. def OAI.Grothendieck.Table.LinearData.attachHighBelow line 562
  54. theorem OAI.Grothendieck.Table.LinearData.face_top_normalized line 605
  55. def OAI.Grothendieck.Table.LinearData.attachHighCritical line 615
  56. theorem OAI.Grothendieck.Table.last_le_height line 666
  57. def OAI.Grothendieck.Table.linearData line 671