OAI/CategoryTheory/Thomason/Gray/ConstructedRightGray.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Associativity of the actual mapping-cell composition

The constructed three-globe cylinder pushout extends any matching triple. Evaluation of its strict associativity diagram then proves associativity at a finite mapping level, and common finite representatives give the unrestricted carrier law.

  1. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.tripleGlue_condition line 31
  2. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.tripleGlue line 41
  3. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.tripleGlue_pair line 48
  4. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.tripleGlue_first line 55
  5. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.tripleGlue_middle line 63
  6. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.tripleGlue_last line 71
  7. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_assoc line 79

    Source documentation

    Associativity at any common finite mapping level.

    theorem composite_assoc (hk : k < n) (f g h : model.obj (Globe.category n) ⟶ D)
    (hfg : model.map (Globe.faceMap true k n) ≫ f = model.map (Globe.faceMap false k n) ≫ g)
    (hgh : model.map (Globe.faceMap true k n) ≫ g = model.map (Globe.faceMap false k n) ≫ h)
    (hl : model.map (Globe.faceMap true k n) ≫ composite hk f g hfg =
      model.map (Globe.faceMap false k n) ≫ h)
    (hr : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ composite hk g h hgh) :
    composite hk (composite hk f g hfg) h hl = composite hk f (composite hk g h hgh) hr := by
…

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

  8. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.assoc_ι line 108

    Source documentation

    Associativity on the images of three finite representatives.

    theorem assoc_ι (hk : k < n) (f g h : model.obj (Globe.category n) ⟶ D)
    (hfg : model.map (Globe.faceMap true k n) ≫ f = model.map (Globe.faceMap false k n) ≫ g)
    (hgh : model.map (Globe.faceMap true k n) ≫ g = model.map (Globe.faceMap false k n) ≫ h)
    (hxy : GlobeMappingCells.face model D true k (GlobeMappingCells.ι model D n f) =
      GlobeMappingCells.face model D false k (GlobeMappingCells.ι model D n g))
    (hyz : GlobeMappingCells.face model D true k (GlobeMappingCells.ι model D n g) =
      GlobeMappingCells.face model D false k (GlobeMappingCells.ι model D n h))
    (hl : GlobeMappingCells.face model D true k
        (comp k (GlobeMappingCells.ι model D n f) (GlobeMappingCells.ι model D n g) hxy) =
      GlobeMappingCells.face model D false k (GlobeMappingCells.ι model D n h))
    (hr : GlobeMappingCells.face model D true k (GlobeMappingCells.ι model D n f) =
      GlobeMappingCells.face model D false k
…

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

  9. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.assoc line 145

    Source documentation

    The actual carrier operation satisfies strict associativity.

    theorem assoc (k : ℕ) (x y z : Cell D)
    (hxy : GlobeMappingCells.face model D true k x = GlobeMappingCells.face model D false k y)
    (hyz : GlobeMappingCells.face model D true k y = GlobeMappingCells.face model D false k z)
    (hl : GlobeMappingCells.face model D true k (comp k x y hxy) =
      GlobeMappingCells.face model D false k z)
    (hr : GlobeMappingCells.face model D true k x =
      GlobeMappingCells.face model D false k (comp k y z hyz)) :
    comp k (comp k x y hxy) z hl = comp k x (comp k y z hyz) 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

  10. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomObj line 197

    Source documentation

    The strict mapping category of the actual interval model.

    def internalHomObj (D : StrictOmegaCategory.{0}) : StrictOmegaCategory.{0} where
…
  11. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomMap line 212

    Source documentation

    Postcomposition as a strict functor on the actual mapping categories.

    def internalHomMap {D E : StrictOmegaCategory.{0}} (u : D ⟶ E) :
    internalHomObj D ⟶ internalHomObj E where
…

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

  12. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHom line 221

    Source documentation

    The global right interval internal-hom functor.

    def internalHom : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0} where
…
  13. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.evaluation line 235

    Source documentation

    Natural maps into the cylinder give strict evaluations; in particular this constructs both interval endpoint evaluations.

    def evaluation (η : 𝟭 StrictOmegaCategory.{0} ⟶ model) (D : StrictOmegaCategory.{0}) :
    internalHomObj D ⟶ D where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomObj

  14. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.evaluationNatTrans line 242

    Source documentation

    Evaluation is natural under postcomposition.

    def evaluationNatTrans (η : 𝟭 StrictOmegaCategory.{0} ⟶ model) :
    internalHom ⟶ 𝟭 StrictOmegaCategory.{0} where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHom

  15. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.globeHomEquiv line 271

    Source documentation

    Representability on every free globe.

    def globeHomEquiv (n : ℕ) (D : StrictOmegaCategory.{0}) :
    (model.obj (Globe.category n) ⟶ D) ≃ (Globe.category n ⟶ internalHomObj D) :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomObj

  16. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.globeHomEquiv_top line 275
  17. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.globeHomEquiv_symm_top line 279
  18. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.globeHomEquiv_precomp line 286

    Source documentation

    Contravariant naturality includes arbitrary strict globe maps.

    theorem globeHomEquiv_precomp {n m : ℕ} (D : StrictOmegaCategory.{0})
    (s : Globe.category n ⟶ Globe.category m) (f : model.obj (Globe.category m) ⟶ D) :
    globeHomEquiv n D (model.map s ≫ f) = s ≫ globeHomEquiv m D f := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.globeHomEquiv

  19. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.globeHomEquiv_postcomp line 295

    Source documentation

    Covariant naturality is the actual strict postcomposition map.

    theorem globeHomEquiv_postcomp {n : ℕ} {D E : StrictOmegaCategory.{0}}
    (f : model.obj (Globe.category n) ⟶ D) (u : D ⟶ E) :
    globeHomEquiv n E (f ≫ u) = globeHomEquiv n D f ≫ internalHomMap u := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.globeHomEquiv, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomMap

  20. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry line 324

    Source documentation

    A concrete chain-model map gives a strict map into the actual internal hom.

    def modelCurry (u : model.obj C ⟶ D) : C ⟶ internalHomObj D where
…

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

  21. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry_precomp line 329
  22. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry_postcomp line 335
  23. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry_globe_eq line 341
  24. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry_restrict line 350
  25. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry_globe_bijective line 354
  26. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry_pasting_bijective line 366

    Source documentation

    Binary gluing upgrades the globe bijection to each composition parameter.

    theorem modelCurry_pasting_bijective {n k : ℕ} (hk : k < n) (D : StrictOmegaCategory.{0}) :
    Function.Bijective (modelCurry (C := PastingGlobe.category n n k) (D := D)) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.modelCurry, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category

  27. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.parameterCurryEquiv line 405

    Source documentation

    The natural Hom bijection on every globe-and-pasting parameter.

    def parameterCurryEquiv (i : GlobePasting.Shape) (D : StrictOmegaCategory.{0}) :
    (model.obj (GlobePasting.object i) ⟶ D) ≃
      (GlobePasting.object i ⟶ internalHomObj D) :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.object, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHomObj

  28. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.parameterCurry_precomp line 413
  29. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.parameterCurry_postcomp line 419
  30. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.curryCocone line 446
  31. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.curryHom line 465
  32. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.curryHom_fac line 468
  33. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.uncurryCocone line 474
  34. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.uncurryHom line 492
  35. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.uncurryHom_fac line 495
  36. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.uncurry_curry line 501
  37. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.curry_uncurry line 509
  38. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.homEquiv line 519

    Source documentation

    The literal Hom bijection for the extended cylinder.

    def homEquiv : (GrayChainExtension.cylinder.obj C ⟶ D) ≃ (C ⟶ internalHomObj D) where
…

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

  39. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.curryHom_postcomp line 527
  40. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.uncurryHom_precomp line 541
  41. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.adjunction line 561

    Source documentation

    The actual global right interval internal-hom adjunction.

    def adjunction : GrayChainExtension.cylinder ⊣ internalHom :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.internalHom

  42. def OAI.Thomason.Construction.NormalizedSimplexIdentities.extendedSimplexModelIso line 589
  43. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.extendedSimplexModelIso_hom line 595

    Source documentation

    The ordered-cell isomorphism is the canonical global comparison.

    theorem extendedSimplexModelIso_hom (m : SimplexCategory) :
    (h.extendedSimplexModelIso m).hom = GrayChainExtension.comparison.app (h.object m.len) := by
…
  44. def OAI.Thomason.Construction.NormalizedSimplexIdentities.extendedSimplexModelNatIso line 609

    Source documentation

    Naturality is inherited from the actual global comparison.

    def extendedSimplexModelNatIso :
    h.cosimplicial ⋙ GrayChainExtension.cylinder ≅
      h.cosimplicial ⋙ GrayChainExtension.model :=
…
  45. def OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedRightSimplexComparison line 622

    Source documentation

    The explicit right chain simplex cylinder identifies with the global extended interval tensor, naturally in every simplex operator.

    def constructedRightSimplexComparison :
    h.cylinderCosimplicial ≅ h.cosimplicial ⋙ GrayChainExtension.cylinder :=
…
  46. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedRightSimplexComparison_comp line 626
  47. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedRightSimplexComparison_endpoint line 638
  48. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedRightSimplexComparison_projection line 650
  49. def OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedRightGrayInput line 656

    Source documentation

    The right interval adjunction with its natural ordered simplex comparison.

    def constructedRightGrayInput : RightGrayInput h where
…

    Mentions: OAI.Thomason.Construction.RightGrayInput

  50. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedRightGrayTruncation line 668

    Source documentation

    The same constructed internal hom preserves each finite truncation.

    theorem constructedRightGrayTruncation : GrayTruncationInput h.constructedRightGrayInput :=
…

    Mentions: OAI.Thomason.Construction.GrayTruncationInput