OAI/CategoryTheory/Thomason/Gray/PrismSimplexNaturality.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.model line 21
2. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.Source line 22
3. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.rowMap line 25
4. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.comparison line 29
5. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.rowMap_comparison line 38
6. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.basisComparison line 44
7. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.rowMap_basisComparison line 48
8. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.row_image_eq line 54
9. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.row_image_eq_of_basisComparison line 67
10. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.atomBasis line 86
11. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.representativeRow line 89
12. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.representativeIndex line 93
13. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.representative_spec line 97
14. def OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.atomLift line 104
15. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.atomLift_dimension line 110
16. theorem OAI.Thomason.Construction.StrictOmegaCategory.GridGlobeCylinder.atomLift_image line 115
17. def OAI.Thomason.Construction.PrismBarycentric.remainder line 151

    Source documentation

    Remove a specified amount of mass from one vertex.

    def remainder {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (j : Fin (n+1)) (a : ℝ) :
        Fin (n+1) →₀ ℝ := x.weights - Finsupp.single j a

18. theorem OAI.Thomason.Construction.PrismBarycentric.remainder_nonneg line 154
19. def OAI.Thomason.Construction.PrismBarycentric.splitWeights line 164

    Source documentation

    Duplicate vertex j, assigning mass a to its first occurrence.

    def splitWeights {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (j : Fin (n+1)) (a : ℝ) :
        Fin (n+2) →₀ ℝ :=
    …

20. def OAI.Thomason.Construction.PrismBarycentric.split line 169

    Source documentation

    The split weights form a genuine standard simplex.

    def split {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (j : Fin (n+1))
        (a : ℝ) (ha : 0 ≤ a) (hb : a ≤ x.weights j) : StdSimplex ℝ (Fin (n+2)) where
    …

21. theorem OAI.Thomason.Construction.PrismBarycentric.split_projection line 183

    Source documentation

    Collapsing the duplicated vertex recovers exactly the original point.

    theorem split_projection {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (j : Fin (n+1))
        (a : ℝ) (ha : 0 ≤ a) (hb : a ≤ x.weights j) :
        StdSimplex.map j.predAbove (split x j a ha hb) = x := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.split

22. def OAI.Thomason.Construction.PrismBarycentric.cumulative line 217

    Source documentation

    Barycentric mass before the kth vertex.

    def cumulative {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (k : ℕ) : ℝ :=
    …

23. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_zero line 221
24. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_all line 225
25. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_step line 228
26. theorem OAI.Thomason.Construction.PrismBarycentric.exists_cut line 246

    Source documentation

    Every mass threshold lies in one of the consecutive vertex intervals.

    theorem exists_cut {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (s : ℝ)
        (hs₀ : 0 ≤ s) (hs₁ : s ≤ 1) :
        ∃ j : Fin (n+1), cumulative x j.val ≤ s ∧ s ≤ cumulative x (j.val+1) := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.cumulative

27. def OAI.Thomason.Construction.PrismBarycentric.region line 271

    Source documentation

    The closed region on which the prism cut passes through vertex j.

    def region {n : ℕ} (j : Fin (n+1)) : Set (StdSimplex ℝ (Fin (n+1)) × unitInterval) :=
    …

28. theorem OAI.Thomason.Construction.PrismBarycentric.continuous_cumulative line 274
29. theorem OAI.Thomason.Construction.PrismBarycentric.region_isClosed line 283
30. theorem OAI.Thomason.Construction.PrismBarycentric.region_cover line 289
31. def OAI.Thomason.Construction.PrismBarycentric.cutMass line 311

    Source documentation

    The barycentric amount assigned to the lower copy of the cut vertex.

    def cutMass {n : ℕ} (j : Fin (n+1))
        (p : StdSimplex ℝ (Fin (n+1)) × unitInterval) : ℝ :=
    …

32. theorem OAI.Thomason.Construction.PrismBarycentric.cutMass_nonneg line 315
33. theorem OAI.Thomason.Construction.PrismBarycentric.cutMass_le line 318
34. def OAI.Thomason.Construction.PrismBarycentric.chart line 325

    Source documentation

    The chart on the jth closed region, in the corresponding (n+1)-simplex.

    def chart {n : ℕ} (j : Fin (n+1)) : C(region j, StdSimplex ℝ (Fin (n+2))) where
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region

35. theorem OAI.Thomason.Construction.PrismBarycentric.chart_projection line 348

    Source documentation

    A chart has exactly the original barycentric first projection.

    theorem chart_projection {n : ℕ} (j : Fin (n+1)) (p : region j) :
        StdSimplex.map j.predAbove (chart j p) = p.val.1 :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.chart

36. theorem OAI.Thomason.Construction.PrismBarycentric.split_zero line 369

    Source documentation

    The zero-mass cut lies in the face omitting its lower copy.

    theorem split_zero {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (j : Fin (n+1)) :
        split x j 0 le_rfl (x.weights_nonneg j) = StdSimplex.map j.castSucc.succAbove x := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.split

37. theorem OAI.Thomason.Construction.PrismBarycentric.adjacent_embeddings line 376

    Source documentation

    Away from the duplicated vertex, the two adjacent face embeddings agree.

    theorem adjacent_embeddings {n : ℕ} (j k : Fin (n+1)) (h : k ≠ j) :
        j.castSucc.succAbove k = j.succ.succAbove k := by
    …

38. theorem OAI.Thomason.Construction.PrismBarycentric.split_full line 383

    Source documentation

    Moving the entire weight to the lower copy lies in the other face.

    theorem split_full {n : ℕ} (x : StdSimplex ℝ (Fin (n+1))) (j : Fin (n+1)) :
        split x j (x.weights j) (x.weights_nonneg j) le_rfl = StdSimplex.map j.succ.succAbove x := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.split

39. abbrev OAI.Thomason.Construction.PrismBarycentric.prism line 420

    Source documentation

    The actual product of the two representable simplicial sets.

    abbrev prism (n : ℕ) : SSet.{0} := Δ[n] ⊗ Δ[1]

40. abbrev OAI.Thomason.Construction.PrismBarycentric.simplexIndex line 423

    Source documentation

    The jth maximal simplex of the standard simplicial prism.

    abbrev simplexIndex {n : ℕ} (j : Fin (n+1)) :
        CostructuredArrow SSet.stdSimplex (prism n) :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.prism

41. abbrev OAI.Thomason.Construction.PrismBarycentric.faceIndex line 428

    Source documentation

    Its codimension-one face at a cut between vertices.

    abbrev faceIndex {n : ℕ} (j : Fin (n+2)) :
        CostructuredArrow SSet.stdSimplex (prism n) :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.prism

42. def OAI.Thomason.Construction.PrismBarycentric.upperFace line 433

    Source documentation

    The face omitting the upper occurrence of the cut vertex.

    def upperFace {n : ℕ} (j : Fin (n+1)) : faceIndex j.succ ⟶ simplexIndex j :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.faceIndex, OAI.Thomason.Construction.PrismBarycentric.simplexIndex

43. def OAI.Thomason.Construction.PrismBarycentric.lowerFace line 442

    Source documentation

    The face omitting the lower occurrence of the cut vertex.

    def lowerFace {n : ℕ} (j : Fin (n+1)) : faceIndex j.castSucc ⟶ simplexIndex j :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.faceIndex, OAI.Thomason.Construction.PrismBarycentric.simplexIndex

44. def OAI.Thomason.Construction.PrismBarycentric.realizedChart line 451

    Source documentation

    Map a barycentric chart to the actual geometric realization of the prism.

    def realizedChart {n : ℕ} (j : Fin (n+1)) : C(region j, SSet.toTop.obj (prism n)) where
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.prism

45. theorem OAI.Thomason.Construction.PrismBarycentric.upperFace_value line 457

    Source documentation

    The realized upper face is its original codimension-one realization leg.

    theorem upperFace_value {n : ℕ} (j : Fin (n+1)) (x : StdSimplex ℝ (Fin (n+1))) :
        (RealizationPrism.leg (prism n) (simplexIndex j)).hom
          (ULift.up (StdSimplex.map j.succ.succAbove x)) =
          (RealizationPrism.leg (prism n) (faceIndex j.succ)).hom (ULift.up x) := by
    …

    Mentions: OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.PrismBarycentric.prism, OAI.Thomason.Construction.PrismBarycentric.simplexIndex, OAI.Thomason.Construction.PrismBarycentric.faceIndex

46. theorem OAI.Thomason.Construction.PrismBarycentric.lowerFace_value line 465

    Source documentation

    The realized lower face is its original codimension-one realization leg.

    theorem lowerFace_value {n : ℕ} (j : Fin (n+1)) (x : StdSimplex ℝ (Fin (n+1))) :
        (RealizationPrism.leg (prism n) (simplexIndex j)).hom
          (ULift.up (StdSimplex.map j.castSucc.succAbove x)) =
          (RealizationPrism.leg (prism n) (faceIndex j.castSucc)).hom (ULift.up x) := by
    …

    Mentions: OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.PrismBarycentric.prism, OAI.Thomason.Construction.PrismBarycentric.simplexIndex, OAI.Thomason.Construction.PrismBarycentric.faceIndex

47. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_monotone line 488
48. theorem OAI.Thomason.Construction.PrismBarycentric.region_between line 503

    Source documentation

    All intermediate charts contain a point belonging to the two extreme charts.

    theorem region_between {n : ℕ} {j k l : Fin (n+1)} (hjl : j ≤ l) (hlk : l ≤ k)
        {p : StdSimplex ℝ (Fin (n+1)) × unitInterval} (hj : p ∈ region j) (hk : p ∈ region k) :
        p ∈ region l :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region

49. theorem OAI.Thomason.Construction.PrismBarycentric.realizedChart_adjacent line 510

    Source documentation

    Adjacent charts have equal values on their common face.

    theorem realizedChart_adjacent {n : ℕ} (j : Fin n)
        (p : StdSimplex ℝ (Fin (n+1)) × unitInterval)
        (h₀ : p ∈ region j.castSucc) (h₁ : p ∈ region j.succ) :
        realizedChart j.castSucc ⟨p, h₀⟩ = realizedChart j.succ ⟨p, h₁⟩ := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.realizedChart

50. theorem OAI.Thomason.Construction.PrismBarycentric.realizedChart_overlap_le line 539

    Source documentation

    All charts agree, including overlaps involving zero barycentric weights.

    theorem realizedChart_overlap_le {n : ℕ} (j k : Fin (n+1)) (hjk : j ≤ k)
        (p : StdSimplex ℝ (Fin (n+1)) × unitInterval)
        (hj : p ∈ region j) (hk : p ∈ region k) :
        realizedChart j ⟨p, hj⟩ = realizedChart k ⟨p, hk⟩ := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.realizedChart

51. theorem OAI.Thomason.Construction.PrismBarycentric.realizedChart_overlap line 561
52. def OAI.Thomason.Construction.PrismBarycentric.standardPrism line 591

    Source documentation

    The actual standard prism, assembled from its maximal simplices.

    def standardPrism (n : ℕ) :
        C(StdSimplex ℝ (Fin (n+1)) × unitInterval, SSet.toTop.obj (prism n)) where
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.prism

53. theorem OAI.Thomason.Construction.PrismBarycentric.standardPrism_on_region line 607

    Source documentation

    The assembled map restricts to the originally defined chart.

    theorem standardPrism_on_region {n : ℕ} (j : Fin (n+1))
        (p : StdSimplex ℝ (Fin (n+1)) × unitInterval) (hp : p ∈ region j) :
        standardPrism n p = realizedChart j ⟨p, hp⟩ := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.standardPrism, OAI.Thomason.Construction.PrismBarycentric.realizedChart

54. theorem OAI.Thomason.Construction.PrismBarycentric.standardPrism_zero line 614

    Source documentation

    At time zero the prism is its all-zero face.

    theorem standardPrism_zero (n : ℕ) (x : StdSimplex ℝ (Fin (n+1))) :
        standardPrism n (x, 0) =
          (RealizationPrism.leg (prism n) (faceIndex (Fin.last (n+1)))).hom (ULift.up x) := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.standardPrism, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.PrismBarycentric.prism, OAI.Thomason.Construction.PrismBarycentric.faceIndex

55. theorem OAI.Thomason.Construction.PrismBarycentric.standardPrism_one line 640

    Source documentation

    At time one the prism is its all-one face.

    theorem standardPrism_one (n : ℕ) (x : StdSimplex ℝ (Fin (n+1))) :
        standardPrism n (x, 1) =
          (RealizationPrism.leg (prism n) (faceIndex (0 : Fin (n+2)))).hom (ULift.up x) := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.standardPrism, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.PrismBarycentric.prism, OAI.Thomason.Construction.PrismBarycentric.faceIndex

56. abbrev OAI.Thomason.Construction.PrismBarycentric.baseIndex line 681

    Source documentation

    The original representable simplex, indexed by its identity map.

    abbrev baseIndex (n : ℕ) : CostructuredArrow SSet.stdSimplex (Δ[n] : SSet.{0}) :=
    …

57. def OAI.Thomason.Construction.PrismBarycentric.firstProjectionMap line 685

    Source documentation

    Collapsing the duplicated vertex is exactly the first prism projection.

    def firstProjectionMap {n : ℕ} (j : Fin (n+1)) :
        (CostructuredArrow.map (fst (Δ[n] : SSet.{0}) Δ[1])).obj (simplexIndex j) ⟶ baseIndex n :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.simplexIndex, OAI.Thomason.Construction.PrismBarycentric.baseIndex

58. theorem OAI.Thomason.Construction.PrismBarycentric.realizedChart_firstProjection line 696

    Source documentation

    Every chart projects back to its original barycentric point in realization.

    theorem realizedChart_firstProjection {n : ℕ} (j : Fin (n+1)) (p : region j) :
        (SSet.toTop.map (fst (Δ[n] : SSet.{0}) Δ[1])).hom (realizedChart j p) =
          (RealizationPrism.leg (Δ[n] : SSet.{0}) (baseIndex n)).hom (ULift.up p.val.1) := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.realizedChart, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.PrismBarycentric.baseIndex

59. theorem OAI.Thomason.Construction.PrismBarycentric.standardPrism_firstProjection line 711

    Source documentation

    The assembled prism has the prescribed first projection at every point.

    theorem standardPrism_firstProjection (n : ℕ)
        (p : StdSimplex ℝ (Fin (n+1)) × unitInterval) :
        (SSet.toTop.map (fst (Δ[n] : SSet.{0}) Δ[1])).hom (standardPrism n p) =
          (RealizationPrism.leg (Δ[n] : SSet.{0}) (baseIndex n)).hom (ULift.up p.1) := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.standardPrism, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.PrismBarycentric.baseIndex

60. theorem OAI.Thomason.Construction.PrismBarycentric.zeroFace_hom line 737
61. theorem OAI.Thomason.Construction.PrismBarycentric.oneFace_hom line 748
62. def OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism line 761

    Source documentation

    The standard prism expressed in the exact topological-simplex convention used by the realization colimit (including its universe lift).

    def liftedStandardPrism (n : ℕ) :
        TopologicalInterval.cylinder.obj (SimplexCategory.toTop.{0}.obj (.mk n)) ⟶
          SSet.toTop.obj (prism n) :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.prism

63. theorem OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism_zero line 768

    Source documentation

    At zero, the continuous prism is exactly realization of the simplicial zero endpoint, preceded by the canonical representable comparison.

    theorem liftedStandardPrism_zero (n : ℕ) :
        TopologicalInterval.sectionAt (SimplexCategory.toTop.{0}.obj (.mk n)) 0 ≫
          liftedStandardPrism n = SSet.toTopSimplex.inv.app (.mk n) ≫ SSet.toTop.map SSet.ι₀ := by
    …

    Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism

64. theorem OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism_one line 782

    Source documentation

    The analogous equality at the one endpoint.

    theorem liftedStandardPrism_one (n : ℕ) :
        TopologicalInterval.sectionAt (SimplexCategory.toTop.{0}.obj (.mk n)) 1 ≫
          liftedStandardPrism n = SSet.toTopSimplex.inv.app (.mk n) ≫ SSet.toTop.map SSet.ι₁ := by
    …

    Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism

65. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_map line 814

    Source documentation

    Pushforward barycentric mass below a threshold is the mass of its preimage.

    theorem cumulative_map {m n : ℕ} (f : Fin (m+1) → Fin (n+1))
        (x : StdSimplex ℝ (Fin (m+1))) (k : ℕ) :
        cumulative (StdSimplex.map f x) k =
          ∑ i : Fin (m+1), if (f i).val < k then x.weights i else 0 := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.cumulative

66. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_map_lower line 828

    Source documentation

    No vertex at or after the cut maps strictly below its image cut.

    theorem cumulative_map_lower {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
        (x : StdSimplex ℝ (Fin (m+1))) (j : Fin (m+1)) :
        cumulative (StdSimplex.map f x) (f j).val ≤ cumulative x j.val := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.cumulative

67. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_map_upper line 847

    Source documentation

    Every vertex up to the cut maps to a vertex up to its image.

    theorem cumulative_map_upper {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
        (x : StdSimplex ℝ (Fin (m+1))) (j : Fin (m+1)) :
        cumulative x (j.val+1) ≤ cumulative (StdSimplex.map f x) ((f j).val+1) := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.cumulative

68. theorem OAI.Thomason.Construction.PrismBarycentric.region_map line 865

    Source documentation

    The image of a closed prism region belongs to the corresponding image region.

    theorem region_map {m n : ℕ} (f : Fin (m+1) →o Fin (n+1)) (j : Fin (m+1))
        (p : region j) : (StdSimplex.map f p.val.1, p.val.2) ∈ region (f j) :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region

69. def OAI.Thomason.Construction.PrismBarycentric.prismOrdinal line 884
70. theorem OAI.Thomason.Construction.PrismBarycentric.prismOrdinal_apply line 899
71. theorem OAI.Thomason.Construction.PrismBarycentric.predAbove_le_cut line 903
72. theorem OAI.Thomason.Construction.PrismBarycentric.cut_le_predAbove line 907
73. theorem OAI.Thomason.Construction.PrismBarycentric.prismOrdinal_first line 915

    Source documentation

    The first coordinate is exactly the original ordinal map.

    theorem prismOrdinal_first {m n : ℕ} (f : Fin (m+1) →o Fin (n+1)) (j : Fin (m+1))
        (k : Fin (m+2)) :
        (f j).predAbove (prismOrdinal f j k) = f (j.predAbove k) := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.prismOrdinal

74. theorem OAI.Thomason.Construction.PrismBarycentric.prismOrdinal_cut line 925

    Source documentation

    Both ends of the doubled cut stay on their prescribed sides.

    theorem prismOrdinal_cut {m n : ℕ} (f : Fin (m+1) →o Fin (n+1)) (j : Fin (m+1))
        (k : Fin (m+2)) :
        prismOrdinal f j k ≤ (f j).castSucc ↔ k ≤ j.castSucc := by
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.prismOrdinal

75. def OAI.Thomason.Construction.PrismBarycentric.simplexNaturality line 954

    Source documentation

    The lifted ordinal map is an actual map between the corresponding simplices of the simplicial prism, including degenerate ordinal maps.

    def simplexNaturality {m n : ℕ} (f : Fin (m+1) →o Fin (n+1)) (j : Fin (m+1)) :
        (CostructuredArrow.map (SSet.stdSimplex.map (SimplexCategory.Hom.mk f) ▷ Δ[1])).obj
          (simplexIndex j) ⟶ simplexIndex (f j) :=
    …

    Mentions: OAI.Thomason.Construction.PrismBarycentric.simplexIndex