Subsimplices as functors

30 Nov 2020

Given a n-semisimplicial type (A_0, \dotsc, A_n), we may form the Σ-type \mathrm{simplices}(n) \coloneqq \Sigma(x^0_0, \dotsc, x^0_n \colon A_0) (x^1_0 \colon A_1\,x^0_0\,x^0_1) \dotsb.\ A_n (\dots), of n-simplices with k-faces labelled by the A_k.

Example: \mathrm{simplices}(2) = \Sigma(x, y, z \colon A_0) (f \colon A_1\,x\,y) (g \colon A_1\,x\,z) (h \colon A_1\,y\,z). \ A_2\,x\,y\,z\,f\,g\,h is the type of triangles with vertices, edges and face dependently labelled by elements of A_0, A_1, A_2.

The appropriate projections then form maps \mathrm{simplices}(n) \rightarrow \mathrm{simplices}(m) for m \leq n (i.e. into lower-dimensional simplices) selecting the faces of \mathrm{simplices}(n).

Example: (\pi_x, \pi_y, \pi_f),\ (\pi_x, \pi_z, \pi_g),\ (\pi_y, \pi_z, \pi_h) \colon \mathrm{simplices}(2) \rightarrow \mathrm{simplices}(1) pick the edges of a triangle, while \pi_z \colon \mathrm{simplices}(2) \rightarrow \mathrm{simplices}(0) picks the third vertex.

Recall that we define the “semisimplex” category \mathbb{\Delta}_+ as the subcategory of the (skeletal) simplex category without degeneracy maps. For any dimension n, \mathrm{simplices} is a presheaf over \mathbb{\Delta}_+, where \mathrm{simplices}(f) for arrows f are the projections mentioned in the previous paragraph. This is just saying that \mathrm{simplices} is indeed a semisimplical object in the category of types.

An element T \colon \mathrm{simplices}(n) then gives rise to a natural transformation T^n \colon よ[n] \Rightarrow \mathrm{simplices}, where よ[n] is the representable functor and the components T^n_m send a sequence s \in \mathrm{hom}([m], [n]) to the tuple encoding the face of T corresponding to s.

Example: Let T \coloneqq (a,b,c,f,g,h,F) \colon \mathrm{simplices}(2). Then naturality of T^n says, for instance, that the following diagram (prettier)

    hom([1], [2]) ───> shape(1) = Σ(x, y: A₀). A₁ x y
          |               |
    - ∘ 1 |               | π₂
          v               v
    hom([0], [2]) ───> shape(0) = A₀

commutes, sending

01 |─> (a, b, f)    02 |─> (a, c, g)    12 |─> (b, c, h)
 ─         ─         ─         ─         ─         ─
 |         |         |         |         |         |
 v         v         v         v         v         v
 1 |─────> b         2 |─────> c         2 |─────> c

(To be continued.)

Updated 1 Dec 2020.