OAI/CategoryTheory/Thomason/Gray/GrayMappingEndpointEvaluation.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

The extended cylinder is composition-generated by its globe images

  1. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterLeg line 19
  2. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globeLeg line 23
  3. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterLeg_naturality line 26
  4. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.pair_image_generated line 40
  5. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.generated_by_globe_images line 94

    Source documentation

    A generating family containing every globe image generates the actual extended cylinder; binary parameters add only composites.

    theorem generated_by_globe_images {C : StrictOmegaCategory.{0}} {I : Type}
    (g : I → cylinder.obj C)
    (h : ∀ n (f : Globe.category n ⟶ C) x,
      Nonempty (CompositionExpression (cylinder.obj C) g ((globeLeg n f).toFun x)))
    (x : cylinder.obj C) : Nonempty (CompositionExpression (cylinder.obj C) g x) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globeLeg

  6. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.comparisonToRealization line 131
  7. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.evaluation_globe line 136
  8. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globeLeg_comparison line 165
  9. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globeEndpoint_image line 199
  10. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globePrism_image line 224
  11. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.atomLift line 238
  12. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.atomLift_dimension line 245
  13. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.atomLift_image line 252
  14. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model line 279
  15. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe line 282

    Source documentation

    The universal composite, with its common finite bound made explicit.

    def compositionGlobe (n k : ℕ) (hk : k < n) :
    Globe.category n ⟶ PastingGlobe.category n n k :=
…

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

  16. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe_source line 288
  17. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe_target line 297
  18. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue line 309

    Source documentation

    Glue the actual maps on the two cylinder pieces.

    def glue (hk : k < n) (f g : model.obj (Globe.category n) ⟶ D)
    (h : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ g) :
    model.obj (PastingGlobe.category n n k) ⟶ D :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category

  19. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_left line 315
  20. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_right line 322
  21. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite line 330

    Source documentation

    Composition in a fixed finite mapping level.

    def composite (hk : k < n) (f g : model.obj (Globe.category n) ⟶ D)
    (h : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ g) : model.obj (Globe.category n) ⟶ D :=
…

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

  22. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_source line 335
  23. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_target line 345
  24. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_postcompose line 355
  25. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_postcompose line 365
  26. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_cell_source line 376

    Source documentation

    The glued composite has exactly the required source in the actual union.

    theorem composite_cell_source (hk : k < n) (f g : model.obj (Globe.category n) ⟶ D)
    (h : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ g) :
    GlobeMappingCells.face model D false k (GlobeMappingCells.ι model D n (composite hk f g h)) =
      GlobeMappingCells.face model D false k (GlobeMappingCells.ι model D n f) := by
…

    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.composite

  27. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_cell_target line 383
  28. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.CellImageGenerated line 407
  29. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cellImageGenerated_mono line 411
  30. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cellImageGenerated_comp line 426
  31. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.ordered_expression line 454
  32. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cellImageGenerated_of_top line 466

    Source documentation

    At a fixed bound, the two top endpoints and the top prism suffice once all lower-dimensional face images have been generated.

    theorem cellImageGenerated_of_top {n : ℕ} (x : C) (hx : C.DimensionLE n x)
    (hsmall : ∀ p, p < n → ∀ a,
      CellImageGenerated g p (C.face a p x) (C.face_dimensionLE a p x))
    (he : ∀ a, Nonempty (CompositionExpression (cylinder.obj C) g
      ((globeLeg n (Globe.lift C x hx)).toFun (endpointTop n a))))
    (hp : Nonempty (CompositionExpression (cylinder.obj C) g
      ((globeLeg n (Globe.lift C x hx)).toFun (prismTop n)))) :
    CellImageGenerated g n x hx := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.CellImageGenerated, OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.globeLeg, OAI.Thomason.Construction.StrictOmegaCategory.Globe.lift, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpointTop, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.prismTop

  33. def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinderAtomLift line 550
  34. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cellImageGenerated_from_atoms line 553
  35. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.generated_from_atoms line 593
  36. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingLower line 620

    Source documentation

    Lower the common dimension of the two universal composable cells.

    def pastingLower {n m : ℕ} (hnm : n ≤ m) (k : ℕ) :
    PastingGlobe.category m m k ⟶ PastingGlobe.category n n k :=
…

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

  37. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingLower_left line 629
  38. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingLower_right line 635
  39. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe_lower line 641
  40. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_lower line 650

    Source documentation

    Gluing the two identity-extended maps is restriction of the original gluing.

    theorem glue_lower (hnm : n ≤ m) (hkn : k < n)
    (f g : model.obj (Globe.category n) ⟶ D)
    (h : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ g)
    (hm : model.map (Globe.faceMap true k m) ≫ (model.map (Globe.lower m n hnm) ≫ f) =
      model.map (Globe.faceMap false k m) ≫ (model.map (Globe.lower m n hnm) ≫ g)) :
    glue (hkn.trans_le hnm) (model.map (Globe.lower m n hnm) ≫ f)
      (model.map (Globe.lower m n hnm) ≫ g) hm =
      model.map (pastingLower hnm k) ≫ glue hkn f g h := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.Globe.lower, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.pastingLower

  41. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_lower line 666

    Source documentation

    Composition is unchanged by enlarging the finite bound.

    theorem composite_lower (hnm : n ≤ m) (hkn : k < n)
    (f g : model.obj (Globe.category n) ⟶ D)
    (h : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ g)
    (hm : model.map (Globe.faceMap true k m) ≫ (model.map (Globe.lower m n hnm) ≫ f) =
      model.map (Globe.faceMap false k m) ≫ (model.map (Globe.lower m n hnm) ≫ g)) :
    composite (hkn.trans_le hnm) (model.map (Globe.lower m n hnm) ≫ f)
      (model.map (Globe.lower m n hnm) ≫ g) hm =
      model.map (Globe.lower m n hnm) ≫ composite hkn f g h := by
…

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

  42. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_cell_lower line 681

    Source documentation

    The enlarged finite representative denotes the same actual mapping cell.

    theorem composite_cell_lower (hnm : n ≤ m) (hkn : k < n)
    (f g : model.obj (Globe.category n) ⟶ D)
    (h : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ g)
    (hm : model.map (Globe.faceMap true k m) ≫ (model.map (Globe.lower m n hnm) ≫ f) =
      model.map (Globe.faceMap false k m) ≫ (model.map (Globe.lower m n hnm) ≫ g)) :
    GlobeMappingCells.ι model D m
      (composite (hkn.trans_le hnm) (model.map (Globe.lower m n hnm) ≫ f)
        (model.map (Globe.lower m n hnm) ≫ g) hm) =
      GlobeMappingCells.ι model D n (composite hkn f g h) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.Globe.lower, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite

  43. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.evaluation_matching line 716
  44. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.glue_evaluation line 724
  45. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_evaluation line 736
  46. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Cell line 768
  47. structure OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative line 770
  48. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.value line 784
  49. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.raise line 787
  50. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.raise_value line 799
  51. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.value_eq line 804

    Source documentation

    Two different common finite presentations define the same composite.

    theorem value_eq (r s : Representative k x y) : r.value = s.value := by
…

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

  52. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.value_source line 821
  53. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.value_target line 826
  54. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.map line 831
  55. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.Representative.map_value line 845
  56. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.representative_exists line 856
  57. def OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.comp line 870

    Source documentation

    Actual composition on the mapping-family carrier.

    def comp (k : ℕ) (x y : Cell D)
    (h : GlobeMappingCells.face model D true k x = GlobeMappingCells.face model D false k y) :
    Cell D :=
…

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

  58. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.comp_congr line 875
  59. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.comp_eq line 883
  60. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.comp_ι line 888
  61. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.source_comp line 905
  62. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.target_comp line 911
  63. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.map_comp line 917
  64. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.evaluate_parameter line 944
  65. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.naturalEvaluation_composite line 954

    Source documentation

    Evaluation at either actual endpoint respects the finite gluing operation.

    theorem naturalEvaluation_composite {n k : ℕ} (hk : k < n)
    (f g : model.obj (Globe.category n) ⟶ D)
    (h : model.map (Globe.faceMap true k n) ≫ f = model.map (Globe.faceMap false k n) ≫ g)
    (h' : D.target k (GlobeMappingCells.naturalEvaluation η D (GlobeMappingCells.ι model D n f)) =
      D.source k (GlobeMappingCells.naturalEvaluation η D (GlobeMappingCells.ι model D n g))) :
    GlobeMappingCells.naturalEvaluation η D
        (GlobeMappingCells.ι model D n (composite hk f g h)) =
      D.comp k (GlobeMappingCells.naturalEvaluation η D (GlobeMappingCells.ι model D n f))
        (GlobeMappingCells.naturalEvaluation η D (GlobeMappingCells.ι model D n g)) h' := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.naturalEvaluation, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.model, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite

  66. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.naturalEvaluation_comp line 986

    Source documentation

    Evaluation is a strict operation-preserving map on the entire carrier.

    theorem naturalEvaluation_comp (k : ℕ) (x y : Cell D)
    (h : GlobeMappingCells.face model D true k x = GlobeMappingCells.face model D false k y)
    (h' : D.target k (GlobeMappingCells.naturalEvaluation η D x) =
      D.source k (GlobeMappingCells.naturalEvaluation η D y)) :
    GlobeMappingCells.naturalEvaluation η D (comp k x y h) =
      D.comp k (GlobeMappingCells.naturalEvaluation η D x)
        (GlobeMappingCells.naturalEvaluation η D 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.GlobeMappingCells.naturalEvaluation, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.comp