OAI/CategoryTheory/Thomason/Gray/GlobePastingDensity.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional cells in the globe mapping family

For a functor on strict categories, maps from the images of the globes form a reflexive globular family. Identity extensions are injective, and their filtered union has actual finite-dimensional cells and globular faces. This is the underlying cell construction for the right interval internal hom; composition is constructed separately from cylinder gluing.

  1. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.lower line 32

    Source documentation

    Extend the universal n-cell to an m-dimensional identity cell.

    def lower (m n : ℕ) (h : n ≤ m) : category m ⟶ category n :=
…

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

  2. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.lower_top line 35
  3. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.lower_self line 38
  4. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.lower_comp line 42
  5. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap_lower line 47
  6. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap_eq_lower line 52
  7. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap_lower_retraction line 59
  8. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.diagram line 73

    Source documentation

    The identity-extension diagram of maps from the actual globe images.

    def diagram : ℕ ⥤ Type where
…
  9. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier line 86
  10. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι line 88
  11. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι_lower line 91
  12. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.exists_representative line 95
  13. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι_injective line 100

    Source documentation

    Every finite-level mapping set embeds into the identity-extension union.

    theorem ι_injective (n : ℕ) : Function.Injective (ι F D n) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι

  14. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.faceCocone line 110
  15. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face line 122
  16. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face_ι line 125
  17. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face_ι_of_le line 129
  18. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.globular line 135

    Source documentation

    The globular law holds before any composition operation is imposed.

    theorem globular (a b : Bool) (r s : ℕ) (x : Carrier F D) :
    face F D a r (face F D b s x) =
      if r < s then face F D a r x else face F D b s x := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face

  19. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.finite_dimension line 145

    Source documentation

    Every mapping-family cell has a finite dimension bound.

    theorem finite_dimension (x : Carrier F D) :
    ∃ n, face F D false n x = x ∧ face F D true n x = x := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face

  20. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.faces_eq_iff line 151

    Source documentation

    Equality of r-faces is the literal equality of the restricted globe maps.

    theorem faces_eq_iff (a b : Bool) (r n m : ℕ)
    (f : F.obj (Globe.category n) ⟶ D) (g : F.obj (Globe.category m) ⟶ D) :
    face F D a r (ι F D n f) = face F D b r (ι F D m g) ↔
      F.map (Globe.faceMap a r n) ≫ f = F.map (Globe.faceMap b r m) ≫ g := by
…

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

  21. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Bounded line 159

    Source documentation

    The literal finite-dimensional condition on the mapping-family carrier.

    def Bounded (n : ℕ) (x : Carrier F D) : Prop :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier

  22. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.bounded_ι line 162
  23. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.bounded_iff_representative line 167

    Source documentation

    A bounded cell is represented at its exact bound, not just a larger stage.

    theorem bounded_iff_representative (n : ℕ) (x : Carrier F D) :
    Bounded F D n x ↔ ∃ f : F.obj (Globe.category n) ⟶ D, ι F D n f = x := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Bounded, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι

  24. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.boundedEquiv line 177

    Source documentation

    Evaluation on an n-globe exactly represents the bounded mapping cells.

    def boundedEquiv (n : ℕ) :
    (F.obj (Globe.category n) ⟶ D) ≃ {x : Carrier F D // Bounded F D n x} where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Bounded

  25. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.mapCocone line 189
  26. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map line 201

    Source documentation

    Postcompose every finite globe map by an actual strict functor.

    def map (u : D ⟶ E) : Carrier F D → Carrier F E :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier

  27. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map_ι line 204
  28. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map_face line 208
  29. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map_id line 213
  30. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map_comp line 217
  31. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.exists_representative_above line 241
  32. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.exists_representatives₂_above line 249

    Source documentation

    A pair of cells has representatives at one bound above any prescribed level.

    theorem exists_representatives₂_above (x y : Carrier F D) (N : ℕ) :
    ∃ (n : ℕ), N ≤ n ∧ ∃ f g : F.obj (Globe.category n) ⟶ D,
      ι F D n f = x ∧ ι F D n g = y := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι

  33. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.matching_representatives line 261

    Source documentation

    Matching faces remain a literal equation at every common representative level.

    theorem matching_representatives {n k : ℕ} (x y : Carrier F D)
    (h : face F D true k x = face F D false k y)
    (f g : F.obj (Globe.category n) ⟶ D)
    (hf : ι F D n f = x) (hg : ι F D n g = y) :
    F.map (Globe.faceMap true k n) ≫ f = F.map (Globe.faceMap false k n) ≫ g := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap

  34. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.exists_representatives_fin_above line 289

    Source documentation

    Choose simultaneous finite representatives, retaining any required lower bound. This supplies the three and four cells used in the strict laws.

    theorem exists_representatives_fin_above (m : ℕ) (x : Fin m → Carrier F D) (N : ℕ) :
    ∃ n, N ≤ n ∧ ∃ f : Fin m → (F.obj (Globe.category n) ⟶ D),
      ∀ i, ι F D n (f i) = x i := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι

  35. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.exists_representatives_finite_above line 306

    Source documentation

    Reindex the common bound by a finite parameter set, such as the four positions in an interchange square.

    theorem exists_representatives_finite_above {I : Type} [Finite I]
    (x : I → Carrier F D) (N : ℕ) :
    ∃ n, N ≤ n ∧ ∃ f : I → (F.obj (Globe.category n) ⟶ D),
      ∀ i, ι F D n (f i) = x i := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι

  36. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.evaluationCocone line 340
  37. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.naturalEvaluation line 354
  38. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.naturalEvaluation_ι line 356
  39. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.naturalEvaluation_face line 360
  40. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.naturalEvaluation_map line 374
  41. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.hom_top_dimension_le line 400
  42. def OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.evaluateCell line 418

    Source documentation

    Evaluate a bounded mapping representative on a cell of its source globe.

    def evaluateCell {m : ℕ} (f : F.obj (Globe.category m) ⟶ D) : Globe.Cell m → Carrier F D
  | .top => ι F D m f
  | .boundary a r => face F D a r (ι F D m f)

/-- Naturality includes every strict globe map, not only the chosen face maps. -/

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.Cell, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.face, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.map

  43. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.globe_naturality line 423

    Source documentation

    Naturality includes every strict globe map, not only the chosen face maps.

    theorem globe_naturality {n m : ℕ} (s : Globe.category n ⟶ Globe.category m)
    (f : F.obj (Globe.category m) ⟶ D) :
    ι F D n (F.map s ≫ f) = evaluateCell F D f (s.toFun Globe.Cell.top) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.ι, OAI.Thomason.Construction.StrictOmegaCategory.GlobeMappingCells.evaluateCell

  44. def OAI.Thomason.Construction.DirectedGlobeComplex.globeNerveIso line 476
  45. def OAI.Thomason.Construction.DirectedGlobeComplex.globeRealizationHomeomorph line 481
  46. theorem OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe_weak line 488

    Source documentation

    The canonical comparison satisfies actual component and homotopy-group weak equivalence, with no Kan--Quillen or Gray hypothesis.

    theorem fromGlobe_weak (n : ℕ) : h.streetWeakEquivalences (fromGlobe n) := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe

  47. theorem OAI.Thomason.Construction.DirectedGlobeComplex.globe_conjugate_weak_iff line 497

    Source documentation

    Conjugating a map by the globe identifications preserves and reflects Street weak equivalences of its actual geometric realization.

    theorem globe_conjugate_weak_iff {m n : ℕ}
    (f : (complex m).realization ⟶ (complex n).realization) :
    h.streetWeakEquivalences ((globeIso m).hom ≫ f ≫ (globeIso n).inv) ↔
      h.streetWeakEquivalences f := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.DirectedGlobeComplex.globeIso

  48. theorem OAI.Thomason.Construction.DirectedGlobeComplex.faceMap_weak_iff line 509

    Source documentation

    The signed face maps have exactly the same actual weak-equivalence status in the free strict and positive-chain presentations.

    theorem faceMap_weak_iff (a : Bool) (m n : ℕ) :
    h.streetWeakEquivalences (faceMap a m n).realization ↔
      h.streetWeakEquivalences (StrictOmegaCategory.Globe.faceMap a m n) := by
…

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

  49. def OAI.Thomason.Construction.DirectedGlobeComplex.globeUnitIso line 544

    Source documentation

    The unit comparison is an actual strict isomorphism on each globe.

    def globeUnitIso (n : ℕ) : StrictOmegaCategory.Globe.category n ≅
    (StrictOmegaCategory.Abelianization.complex (StrictOmegaCategory.Globe.category n)).realization :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex

  50. theorem OAI.Thomason.Construction.DirectedGlobeComplex.globeUnitIso_hom line 548
  51. def OAI.Thomason.Construction.DirectedGlobeComplex.globeUnitNerveIso line 562

    Source documentation

    The unit induces a literal isomorphism of the actual Street nerves.

    def globeUnitNerveIso (h : NormalizedSimplexIdentities) (n : ℕ) :
    h.streetNerve.obj (StrictOmegaCategory.Globe.category n) ≅
      h.streetNerve.obj
        (StrictOmegaCategory.Abelianization.complex (StrictOmegaCategory.Globe.category n)).realization :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex

  52. def OAI.Thomason.Construction.DirectedGlobeComplex.globeUnitRealizationHomeomorph line 568
  53. theorem OAI.Thomason.Construction.DirectedGlobeComplex.globe_unit_weak line 574
  54. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.collapse line 606

    Source documentation

    Collapse the universal m-cell to its chosen n-face, retaining all its lower faces by the universal property of the actual globe.

    def collapse (a : Bool) (n m : ℕ) : category m ⟶ category m :=
…

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

  55. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.collapse_top line 610
  56. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.collapse_eq_id line 613
  57. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.truncated_iff_collapse line 623

    Source documentation

    The existing pointwise face criterion is equivalently a test on maps out of every actual finite globe.

    theorem truncated_iff_collapse (C : StrictOmegaCategory.{0}) (n : ℕ) :
    C.IsTruncated n ↔ ∀ (m : ℕ) (f : category m ⟶ C) (a : Bool),
      collapse a n m ≫ f = f := by
…

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

  58. theorem OAI.Thomason.Construction.internalHom_truncated_iff_cylinder_globes line 639

    Source documentation

    Internal-hom truncation reduces to a concrete equality on the cylinders of finite globes. Naturality of the actual adjunction is the only transport used here.

    theorem internalHom_truncated_iff_cylinder_globes
    {F R : StrictOmegaCategory.{0} ⥤ StrictOmegaCategory.{0}} (adj : F ⊣ R)
    (Y : StrictOmegaCategory.{0}) (n : ℕ) :
    (R.obj Y).IsTruncated n ↔
      ∀ (m : ℕ) (f : F.obj (StrictOmegaCategory.Globe.category m) ⟶ Y) (a : Bool),
        F.map (StrictOmegaCategory.Globe.collapse a n m) ≫ f = f := by
…

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

  59. theorem OAI.Thomason.Construction.RightGrayInput.internalHom_truncated_iff_globe_test line 662

    Source documentation

    Preservation of finite truncations is equivalent to an explicit test on the cylinders of free globes.

    theorem internalHom_truncated_iff_globe_test
    (Y : StrictOmegaCategory.{0}) (n : ℕ) :
    (G.internalHom.obj Y).IsTruncated n ↔
      ∀ (m : ℕ) (f : G.cylinder.obj (StrictOmegaCategory.Globe.category m) ⟶ Y)
        (a : Bool), G.cylinder.map (StrictOmegaCategory.Globe.collapse a n m) ≫ f = f :=
…

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

  60. abbrev OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category line 691
  61. abbrev OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left line 694
  62. abbrev OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right line 697
  63. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.leftCell line 700
  64. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightCell line 702
  65. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.matching line 704
  66. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.hom_ext line 716

    Source documentation

    A strict map from the pasted globes is determined by its two cells.

    theorem hom_ext {n m k : ℕ} {C : StrictOmegaCategory.{0}}
    (f g : category n m k ⟶ C)
    (hl : f.toFun (leftCell n m k) = g.toFun (leftCell n m k))
    (hr : f.toFun (rightCell n m k) = g.toFun (rightCell n m k)) : f = g := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.leftCell, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.rightCell

  67. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.desc line 727

    Source documentation

    Every matching pair determines its unique strict map from the pasting.

    def desc {n m k : ℕ} (C : StrictOmegaCategory.{0})
    (x y : C) (hx : C.DimensionLE n x) (hy : C.DimensionLE m y)
    (hxy : C.target k x = C.source k y) : category n m k ⟶ C :=
…

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

  68. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.desc_left line 735
  69. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.desc_right line 748
  70. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.exists_unique_map line 761
  71. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.composite line 773
  72. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.composite_dimension line 776
  73. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.compositionMap line 785

    Source documentation

    The universal composite is itself represented by a strict globe.

    def compositionMap (n m k : ℕ) (hk : k < max n m) :
    Globe.category (max n m) ⟶ category n m k :=
…

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

  74. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.desc_composite line 790

    Source documentation

    Evaluation of the pasted universal cell is the specified composition.

    theorem desc_composite {n m k : ℕ} (C : StrictOmegaCategory.{0})
    (x y : C) (hx : C.DimensionLE n x) (hy : C.DimensionLE m y)
    (hxy : C.target k x = C.source k y) :
    (desc C x y hx hy hxy).toFun (composite n m k) = C.comp k x y hxy := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.desc, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.composite

  75. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.compositionMap_desc line 803

    Source documentation

    The composition map is compatible with every pair of bounded cells.

    theorem compositionMap_desc {n m k : ℕ} (hk : k < max n m)
    (C : StrictOmegaCategory.{0}) (x y : C)
    (hx : C.DimensionLE n x) (hy : C.DimensionLE m y)
    (hxy : C.target k x = C.source k y) :
    compositionMap n m k hk ≫ desc C x y hx hy hxy =
      Globe.lift C (C.comp k x y hxy)
        (C.dimensionLE_comp hk (C.dimensionLE_mono (Nat.le_max_left n m) hx)
          (C.dimensionLE_mono (Nat.le_max_right n m) hy) hxy) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.compositionMap, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.desc, OAI.Thomason.Construction.StrictOmegaCategory.Globe.lift

  76. inductive OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape line 834
  77. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.object line 838
  78. instance OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.(instance at line 842) line 842
  79. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion line 847
  80. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.diagram line 851
  81. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.cocone line 854
  82. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.globePoint line 860
  83. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.value line 865

    Source documentation

    Value assigned by a compatible cocone to a bounded cell.

    def value {C : StrictOmegaCategory.{0}} (s : Cocone (diagram C))
    {n : ℕ} (x : C) (hx : C.DimensionLE n x) : s.pt :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.diagram

  84. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.value_raise line 869
  85. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.value_independent line 884

    Source documentation

    A compatible family assigns the same value for every finite dimension bound.

    theorem value_independent {C : StrictOmegaCategory.{0}} (s : Cocone (diagram C))
    {n m : ℕ} (x : C) (hx : C.DimensionLE n x) (hy : C.DimensionLE m x) :
    value s x hx = value s x hy := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.diagram, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.value

  86. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.dimension line 890
  87. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.dimension_bound line 893
  88. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate line 897

    Source documentation

    The candidate map is defined on every actual cell, independently of a bound.

    def evaluate {C : StrictOmegaCategory.{0}} (s : Cocone (diagram C)) (x : C) : s.pt :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.diagram

  89. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate_eq_value line 900
  90. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate_face line 905

    Source documentation

    Face preservation is forced by the morphisms between actual free globes.

    theorem evaluate_face {C : StrictOmegaCategory.{0}} (s : Cocone (diagram C))
    (a : Bool) (m : ℕ) (x : C) :
    evaluate s (C.face a m x) = s.pt.face a m (evaluate s x) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.diagram, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate

  91. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate_map line 937

    Source documentation

    The descended cell map agrees with every leg on every cell.

    theorem evaluate_map {C : StrictOmegaCategory.{0}} (s : Cocone (diagram C))
    (i : Shape) (f : object i ⟶ C) (x : object i) :
    evaluate s (f.toFun x) =
      (s.ι.app (CostructuredArrow.mk (Y := i) f)).toFun x := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.diagram, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.object, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate

  92. theorem OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate_comp line 951

    Source documentation

    Composable pairs force the cellwise descent map to preserve composition.

    theorem evaluate_comp {C : StrictOmegaCategory.{0}} (s : Cocone (diagram C))
    (k : ℕ) (x y : C) (hxy : C.target k x = C.source k y)
    (h' : s.pt.target k (evaluate s x) = s.pt.source k (evaluate s y)) :
    evaluate s (C.comp k x y hxy) = s.pt.comp k (evaluate s x) (evaluate s y) h' := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.diagram, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.evaluate

  93. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.desc line 982
  94. def OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.isColimit line 988

    Source documentation

    Every strict category has the actual small globe-and-pasting presentation.

    def isColimit (C : StrictOmegaCategory.{0}) : IsColimit (cocone C) where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.cocone