OAI/CategoryTheory/Thomason/Gray/TripleGlobeRetractions.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Unrestricted interchange for the actual mapping-cell operation

The actual grid-cylinder pushout glues four boundary-compatible maps. Evaluation of the strict grid diagram proves interchange, first at a common finite level and then on the filtered-union carrier.

  1. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.gridGlue line 29
  2. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.gridGlue_row line 41
  3. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.gridGlue_evaluation line 53
  4. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_interchange line 68

    Source documentation

    Interchange at every common finite mapping level.

    theorem composite_interchange (hkl : k < l) (hln : l < n)
    (f : Bool → Bool → (model.obj (Globe.category n) ⟶ D))
    (hh : ∀ b, model.map (Globe.faceMap true k n) ≫ f b false =
      model.map (Globe.faceMap false k n) ≫ f b true)
    (hv : ∀ a, model.map (Globe.faceMap true l n) ≫ f false a =
      model.map (Globe.faceMap false l n) ≫ f true a)
    (hV : model.map (Globe.faceMap true l n) ≫
        composite (hkl.trans hln) (f false false) (f false true) (hh false) =
      model.map (Globe.faceMap false l n) ≫
        composite (hkl.trans hln) (f true false) (f true true) (hh true))
    (hH : model.map (Globe.faceMap true k n) ≫
        composite hln (f false false) (f true false) (hv false) =
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite

  5. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.interchange_ι line 115

    Source documentation

    Interchange on the images of four finite representatives.

    theorem interchange_ι (hkl : k < l) (hln : l < n)
    (f : Bool → Bool → (model.obj (Globe.category n) ⟶ D))
    (hh : ∀ b, GlobeMappingCells.face model D true k (GlobeMappingCells.ι model D n (f b false)) =
      GlobeMappingCells.face model D false k (GlobeMappingCells.ι model D n (f b true)))
    (hv : ∀ a, GlobeMappingCells.face model D true l (GlobeMappingCells.ι model D n (f false a)) =
      GlobeMappingCells.face model D false l (GlobeMappingCells.ι model D n (f true a)))
    (hV : GlobeMappingCells.face model D true l
        (comp k (GlobeMappingCells.ι model D n (f false false))
          (GlobeMappingCells.ι model D n (f false true)) (hh false)) =
      GlobeMappingCells.face model D false l
        (comp k (GlobeMappingCells.ι model D n (f true false))
          (GlobeMappingCells.ι model D n (f true true)) (hh true)))
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.comp

  6. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.interchange_family line 175

    Source documentation

    Interchange for any four matching cells of the actual mapping carrier.

    theorem interchange_family (k l : ℕ) (hkl : k < l) (x : Bool → Bool → Cell D)
    (hh : ∀ b, GlobeMappingCells.face model D true k (x b false) =
      GlobeMappingCells.face model D false k (x b true))
    (hv : ∀ a, GlobeMappingCells.face model D true l (x false a) =
      GlobeMappingCells.face model D false l (x true a))
    (hV : GlobeMappingCells.face model D true l (comp k (x false false) (x false true) (hh false)) =
      GlobeMappingCells.face model D false l (comp k (x true false) (x true true) (hh true)))
    (hH : GlobeMappingCells.face model D true k (comp l (x false false) (x true false) (hv false)) =
      GlobeMappingCells.face model D false k (comp l (x false true) (x true true) (hv true))) :
    comp l (comp k (x false false) (x false true) (hh false))
        (comp k (x true false) (x true true) (hh true)) hV =
      comp k (comp l (x false false) (x true false) (hv false))
…

    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

  7. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.interchange line 216

    Source documentation

    The strict interchange law in the usual four-cell notation.

    theorem interchange (k l : ℕ) (hkl : k < l) (a b c d : Cell D)
    (hab : GlobeMappingCells.face model D true k a = GlobeMappingCells.face model D false k b)
    (hcd : GlobeMappingCells.face model D true k c = GlobeMappingCells.face model D false k d)
    (hac : GlobeMappingCells.face model D true l a = GlobeMappingCells.face model D false l c)
    (hbd : GlobeMappingCells.face model D true l b = GlobeMappingCells.face model D false l d)
    (hl : GlobeMappingCells.face model D true l (comp k a b hab) =
      GlobeMappingCells.face model D false l (comp k c d hcd))
    (hr : GlobeMappingCells.face model D true k (comp l a c hac) =
      GlobeMappingCells.face model D false k (comp l b d hbd)) :
    comp l (comp k a b hab) (comp k c d hcd) hl =
      comp k (comp l a c hac) (comp l b d hbd) hr := 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

  8. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.curry_rep_lower line 263
  9. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry line 272
  10. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry_eq line 277

    Source documentation

    Every dimension bound computes the same curried cell.

    theorem cellCurry_eq (u : model.obj C ⟶ D) (x : C) {n : ℕ} (hx : C.DimensionLE n x) :
    cellCurry u x = GlobeMappingCells.ι model D n (model.map (Globe.lift C x hx) ≫ u) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model, OAI.Thomason.Construction.StrictOmegaCategory.Globe.lift

  11. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry_globe line 287

    Source documentation

    Restriction to any bounded cell is exactly its globe representative.

    theorem cellCurry_globe (u : model.obj C ⟶ D) {n : ℕ} (s : Globe.category n ⟶ C) :
    cellCurry u (s.toFun Globe.Cell.top) = GlobeMappingCells.ι model D n (model.map s ≫ u) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model

  12. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry_face line 295
  13. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry_comp line 305

    Source documentation

    Cellwise currying respects each defined composition.

    theorem cellCurry_comp (u : model.obj C ⟶ D) (k : ℕ) (x y : C)
    (h : C.target k x = C.source k y)
    (h' : GlobeMappingCells.face model D true k (cellCurry u x) =
      GlobeMappingCells.face model D false k (cellCurry u y)) :
    cellCurry u (C.comp k x y h) = comp k (cellCurry u x) (cellCurry u y) h' := by
…

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

  14. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry_precomp line 344

    Source documentation

    Currying commutes with an arbitrary strict map of source categories.

    theorem cellCurry_precomp {B : StrictOmegaCategory.{0}} (s : B ⟶ C)
    (u : model.obj C ⟶ D) (x : B) :
    cellCurry (model.map s ≫ u) x = cellCurry u (s.toFun x) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry

  15. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry_postcomp line 355

    Source documentation

    Currying commutes with postcomposition in the target.

    theorem cellCurry_postcomp (u : model.obj C ⟶ D) (v : D ⟶ E) (x : C) :
    cellCurry (u ≫ v) x = GlobeMappingCells.map model v (cellCurry u x) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.cellCurry, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model

  16. def OAI.Thomason.Construction.TripleGlobeBasis.top line 375
  17. theorem OAI.Thomason.Construction.TripleGlobeBasis.top_dimension line 378
  18. theorem OAI.Thomason.Construction.TripleGlobeBasis.top_matching line 382
  19. def OAI.Thomason.Construction.TripleGlobeBasis.fromTriple line 402
  20. theorem OAI.Thomason.Construction.TripleGlobeBasis.fromTriple_cell line 406
  21. def OAI.Thomason.Construction.TripleGlobeBasis.abelianizationToBasis line 410
  22. theorem OAI.Thomason.Construction.TripleGlobeBasis.unit_matching line 415
  23. def OAI.Thomason.Construction.TripleGlobeBasis.basisToAbelianization line 425
  24. theorem OAI.Thomason.Construction.TripleGlobeBasis.desc_top line 431
  25. theorem OAI.Thomason.Construction.TripleGlobeBasis.abelianizationToBasis_unit line 440
  26. theorem OAI.Thomason.Construction.TripleGlobeBasis.basisToAbelianization_top line 447
  27. theorem OAI.Thomason.Construction.TripleGlobeBasis.abelianizationToBasis_inverse line 455
  28. theorem OAI.Thomason.Construction.TripleGlobeBasis.basisToAbelianization_inverse line 468
  29. def OAI.Thomason.Construction.TripleGlobeBasis.abelianizationIso line 478
  30. theorem OAI.Thomason.Construction.TripleGlobeBasis.embed_lower line 501
  31. theorem OAI.Thomason.Construction.TripleGlobeBasis.inclusion_basisAtom line 510
  32. def OAI.Thomason.Construction.TripleGlobeBasis.pairCopy line 528
  33. def OAI.Thomason.Construction.TripleGlobeBasis.pairEmbed line 530
  34. def OAI.Thomason.Construction.TripleGlobeBasis.pairInclusion line 534
  35. theorem OAI.Thomason.Construction.TripleGlobeBasis.inclusion_pairInclusion line 538
  36. theorem OAI.Thomason.Construction.TripleGlobeBasis.pairInclusion_atom line 548
  37. def OAI.Thomason.Construction.TripleGlobeBasis.globeCylinderIndex line 557
  38. def OAI.Thomason.Construction.TripleGlobeBasis.pairCylinderIndex line 563
  39. theorem OAI.Thomason.Construction.TripleGlobeBasis.globeCylinder_atom line 569
  40. theorem OAI.Thomason.Construction.TripleGlobeBasis.pairCylinder_atom line 590
  41. theorem OAI.Thomason.Construction.TripleGlobeBasis.abelianization_globe line 626
  42. theorem OAI.Thomason.Construction.TripleGlobeBasis.abelianization_pair line 651
  43. def OAI.Thomason.Construction.TripleGlobeBasis.modelIso line 691
  44. def OAI.Thomason.Construction.TripleGlobeBasis.globeModelIso line 696
  45. theorem OAI.Thomason.Construction.TripleGlobeBasis.model_globe line 700
  46. theorem OAI.Thomason.Construction.TripleGlobeBasis.model_pair line 709
  47. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.collapsePair line 739
  48. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.bridge_collapsePair line 743
  49. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.retractPair line 749
  50. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.retractLast line 753
  51. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.pair_retractPair line 757
  52. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.last_retractPair line 760
  53. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.pair_retractLast line 764
  54. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.last_retractLast line 768
  55. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.ImageSource line 773
  56. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.imageCell line 776
  57. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.targetCell line 781
  58. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.cross_image_eq line 787
  59. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.imageCell_eq line 824

    Source documentation

    Equal target piece cells are already equal in the source pushout.

    theorem imageCell_eq (n k : ℕ) (hkn : k ≤ n)
    (x y : F.obj (PastingGlobe.category n n k) ⊕ F.obj (Globe.category n))
    (he : targetCell F n k x = targetCell F n k y) :
    imageCell F n k x = imageCell F n k y := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.targetCell, OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.imageCell