OAI/CategoryTheory/Thomason/Gray/GridGlobeCylinderComparison.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Higher-face compatibility of the actual mapping composition

  1. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.face_matching line 18
  2. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingFace line 26
  3. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingFace_left line 35
  4. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingFace_right line 42
  5. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe_face line 49
  6. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_face line 61
  7. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_face line 76
  8. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.face_comp line 91

    Source documentation

    The actual mapping-cell composition preserves every higher face.

    theorem face_comp (a : Bool) (r k : ℕ) (hkr : k < r) (x y : Cell D)
    (h : GlobeMappingCells.face model D true k x = GlobeMappingCells.face model D false k y)
    (h' : GlobeMappingCells.face model D true k (GlobeMappingCells.face model D a r x) =
      GlobeMappingCells.face model D false k (GlobeMappingCells.face model D a r y)) :
    GlobeMappingCells.face model D a r (comp k x y h) =
      comp k (GlobeMappingCells.face model D a r x) (GlobeMappingCells.face model D a r y) h' := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Cell, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.comp

  9. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe_retractRight line 143
  10. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe_retractLeft line 149
  11. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.paddedFace line 157
  12. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.paddedFace_cell line 161
  13. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_source_identity line 170
  14. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_target_identity line 181
  15. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_source_identity line 192
  16. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_target_identity line 200
  17. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.left_unit line 208
  18. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.right_unit line 229
  19. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.category line 272
  20. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.row line 275
  21. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.inclusion line 278
  22. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.cell line 281
  23. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.cell_dimension line 283
  24. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontal_matching line 287
  25. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.vertical_boundary line 294
  26. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.vertical_matching line 307
  27. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.hom_ext line 315
  28. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.grid_row_matching line 342
  29. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontalComposite line 379
  30. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.verticalComposite line 383
  31. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.comp_congr line 387
  32. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.face_horizontal_matching line 395
  33. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontal_composites_matching line 401
  34. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.verticalComposite_lower_face line 413
  35. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.vertical_composites_matching line 421
  36. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontalComposite_dimension line 430
  37. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.verticalComposite_dimension line 435
  38. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.verticalOuter line 441

    Source documentation

    The vertical pair of horizontal composites.

    def verticalOuter : PastingGlobe.category n n l ⟶ category n k l hkl :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.category

  39. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontalOuter line 449

    Source documentation

    The horizontal pair of vertical composites.

    def horizontalOuter : PastingGlobe.category n n k ⟶ category n k l hkl :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.category

  40. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.column line 457

    Source documentation

    The individual vertical column, including both its generating cells.

    def column (a : Bool) : PastingGlobe.category n n l ⟶ category n k l hkl :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.category

  41. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.column_left line 462
  42. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.column_right line 467
  43. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.row_composite line 472
  44. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.column_composite line 476
  45. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.verticalOuter_left line 480
  46. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.verticalOuter_right line 486
  47. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontalOuter_left line 492
  48. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontalOuter_right line 498
  49. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.interchange_diagram line 505

    Source documentation

    Strict interchange is an equality of actual finite parameter maps.

    theorem interchange_diagram :
    GrayMapping.compositionGlobe n l hln ≫ verticalOuter n k l hkl hln =
      GrayMapping.compositionGlobe n k (hkl.trans hln) ≫ horizontalOuter n k l hkl hln := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe, OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.verticalOuter, OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.horizontalOuter

  50. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.face_lower_retraction line 539
  51. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.retractTop line 549
  52. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.retractBottom line 553
  53. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.top_retractTop line 557
  54. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.bottom_retractTop line 560
  55. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.top_retractBottom line 565
  56. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.bottom_retractBottom line 570
  57. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.retractRow line 573
  58. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.row_retractRow line 576
  59. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.ImageSource line 584
  60. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.row_map_injective line 589
  61. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.cross_image_eq line 601

    Source documentation

    Equality of top and bottom images is already witnessed in the actual pushout of their functor images.

    theorem cross_image_eq (x y : F.obj (PastingGlobe.category n n k))
    (he : (F.map (row n k l hkl false)).toFun x = (F.map (row n k l hkl true)).toFun y) :
    (pushout.inl (F.map (GrayMapping.pastingFace true l n k hkl))
      (F.map (GrayMapping.pastingFace false l n k hkl))).toFun x =
    (pushout.inr (F.map (GrayMapping.pastingFace true l n k hkl))
      (F.map (GrayMapping.pastingFace false l n k hkl))).toFun y := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.row, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingFace

  62. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.rowDesc line 660
  63. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.desc_condition line 664
  64. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.desc line 696

    Source documentation

    Unique strict map with the prescribed four matching bounded cells.

    def desc : category n k l hkl ⟶ C :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.category

  65. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.desc_cell line 700
  66. def OAI.Thomason.Construction.GridGlobeBasis.top line 727
  67. theorem OAI.Thomason.Construction.GridGlobeBasis.top_dimension line 731
  68. theorem OAI.Thomason.Construction.GridGlobeBasis.top_horizontal line 736
  69. theorem OAI.Thomason.Construction.GridGlobeBasis.top_table_below line 743
  70. theorem OAI.Thomason.Construction.GridGlobeBasis.top_vertical line 752
  71. def OAI.Thomason.Construction.GridGlobeBasis.fromGrid line 774
  72. theorem OAI.Thomason.Construction.GridGlobeBasis.fromGrid_cell line 779
  73. def OAI.Thomason.Construction.GridGlobeBasis.abelianizationToBasis line 783
  74. theorem OAI.Thomason.Construction.GridGlobeBasis.unit_horizontal line 788
  75. theorem OAI.Thomason.Construction.GridGlobeBasis.unit_vertical line 798
  76. def OAI.Thomason.Construction.GridGlobeBasis.basisToAbelianization line 808
  77. theorem OAI.Thomason.Construction.GridGlobeBasis.desc_top line 815
  78. theorem OAI.Thomason.Construction.GridGlobeBasis.abelianizationToBasis_unit line 826
  79. theorem OAI.Thomason.Construction.GridGlobeBasis.basisToAbelianization_top line 833
  80. theorem OAI.Thomason.Construction.GridGlobeBasis.abelianizationToBasis_inverse line 841
  81. theorem OAI.Thomason.Construction.GridGlobeBasis.basisToAbelianization_inverse line 854
  82. def OAI.Thomason.Construction.GridGlobeBasis.abelianizationIso line 871
  83. theorem OAI.Thomason.Construction.GridGlobeBasis.abelianization_row line 894
  84. def OAI.Thomason.Construction.GridGlobeBasis.modelIso line 935
  85. theorem OAI.Thomason.Construction.GridGlobeBasis.model_row line 940