Complements on standard simplices

A map of simplicial sets q : Δ[m] ⟶ Δ[n] is determined by its vertex map, the m-simplex yonedaEquiv q of Δ[n], and it acts on the simplices of Δ[m] by composing with it. Standard simplices are nerves of finite linear orders, hence quasicategories. These facts let one handle maps from horns and simplices to Δ[n], for instance to Δ[1] when splitting a simplex into an initial and a final segment.

An injective m-simplex of Δ[n] is the increasing enumeration of its set of vertices, and the faces of the increasing enumeration of a set J enumerate the sets J with one element removed.

Main results

• SSet.stdSimplex.hom_app_apply: the vertices of the image of a simplex under a map of standard simplices.

• SSet.stdSimplex.const_app_apply: the constant map at a vertex of Δ[n] sends every simplex to the constant simplex at that vertex.

• SSet.stdSimplex.δ_objMk_orderEmbOfFin: the faces of the increasing enumeration of a set of vertices.

• SSet.stdSimplex.objMk_orderEmbOfFin_image: an injective simplex is the increasing enumeration of its set of vertices.

• SSet.stdSimplex.subcomplex_hom_app_apply: the vertices of the image of a simplex under a map from a subcomplex of a standard simplex to a standard simplex.

• SSet.stdSimplex.hom_app_obj₀Equiv_symm: a map g of standard simplices sends the vertex j to the vertex yonedaEquiv g j.

• SSet.stdSimplex.edge_edge_apply_zero, SSet.stdSimplex.edge_edge_apply_one: the endpoints of an edge of Δ[n] are its vertices 0 and 1.

• SSet.stdSimplex.nonempty_edge_iff: Δ[n] has an edge from a to b exactly when a ≤ b, and it is then unique (SSet.stdSimplex.subsingleton_edge).

• SSet.stdSimplex.quasicategory: standard simplices are quasicategories.

• SSet.stdSimplex.isConnected: standard simplices are connected.

• SSet.stdSimplex.contraction: the homotopy from the constant map at the initial vertex of Δ[n] to its identity.

• SSet.horn_one_ι_eq_const: each horn Λ[1, i] of Δ[1] is the vertex i.

• SSet.fstStdSimplexZeroIso: the projection K ⊗ Δ[0] ⟶ K is an isomorphism.

• SSet.boundary.isConnected: the boundary ∂Δ[n + 2] is connected.

theorem SSet.stdSimplex.hom_app_apply {m n d : ℕ} (q : stdSimplex.obj { len := m } ⟶ stdSimplex.obj { len := n }) (x : (stdSimplex.obj { len := m }).obj (Opposite.op { len := d })) (j : Fin (d + 1)) : ((CategoryTheory.ConcreteCategory.hom (q.app (Opposite.op { len := d }))) x) j = (yonedaEquiv q) (x j)

A map of standard simplices q : Δ[m] ⟶ Δ[n] sends a simplex x of Δ[m] to the simplex whose j-th vertex is the image of the j-th vertex of x under the vertex map of q.

theorem SSet.stdSimplex.const_app_apply {X : SSet} {n d : ℕ} (e : Fin (n + 1)) (x : X.obj (Opposite.op { len := d })) (j : Fin (d + 1)) : ((CategoryTheory.ConcreteCategory.hom ((SSet.const (const n e (Opposite.op { len := 0 }))).app (Opposite.op { len := d }))) x) j = e

The constant map at the vertex e of Δ[n] sends every simplex to a simplex all of whose vertices are e.

@[simp]

theorem SSet.stdSimplex.coe_asOrderHom {n d : ℕ} (x : (stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) : ⇑(asOrderHom x) = ⇑x

The vertex map asOrderHom x of a simplex x of Δ[n] evaluates like x itself: both are the vertex function of the morphism objEquiv x : ⦋d⦌ ⟶ ⦋n⦌ of the simplex category.

theorem SSet.stdSimplex.δ_objMk_orderEmbOfFin {n m : ℕ} (J : Finset (Fin (n + 1))) (h : J.card = m + 2) (i : Fin (m + 2)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (stdSimplex.obj { len := n }) i)) (objMk (J.orderEmbOfFin h).toOrderHom) = objMk ((J.erase ((J.orderEmbOfFin h) i)).orderEmbOfFin ⋯).toOrderHom

The i-th face of the simplex of Δ[n] enumerating a set J of vertices in increasing order enumerates J with its i-th smallest element removed.

theorem SSet.stdSimplex.objMk_orderEmbOfFin_image {n m : ℕ} (x : (stdSimplex.obj { len := n }).obj (Opposite.op { len := m })) (h : (Finset.image (⇑x) Finset.univ).card = m + 1) : objMk ((Finset.image (⇑x) Finset.univ).orderEmbOfFin h).toOrderHom = x

A simplex x of Δ[n] whose vertices are pairwise distinct, that is whose set of vertices has m + 1 elements, enumerates its set of vertices in increasing order.

@[simp]

theorem SSet.stdSimplex.yonedaEquiv_id_apply (n : ℕ) (j : Fin (n + 1)) : (yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := n }))) j = j

The top simplex of Δ[n], corresponding to its identity map, has j as its j-th vertex.

@[simp]

theorem SSet.stdSimplex.const_apply (n : ℕ) (k : Fin (n + 1)) (d : ℕ) (t : Fin (d + 1)) : (const n k (Opposite.op { len := d })) t = k

The constant simplex at the vertex k of Δ[n] has all its vertices equal to k.

@[simp]

theorem SSet.stdSimplex.obj_map_apply {n d d' : ℕ} (f : Opposite.op { len := d } ⟶ Opposite.op { len := d' }) (x : (stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (j : Fin (d' + 1)) : ((CategoryTheory.ConcreteCategory.hom ((stdSimplex.obj { len := n }).map f)) x) j = x ((SimplexCategory.Hom.toOrderHom f.unop) j)

The vertices of the image of a simplex x of Δ[n] under a simplicial operator f are the vertices of x indexed through f.

@[simp]

theorem SSet.stdSimplex.edge_apply_zero (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : (edge n a b hab) 0 = a

The edge of Δ[n] from a to b starts at a.

@[simp]

theorem SSet.stdSimplex.edge_apply_one (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : (edge n a b hab) 1 = b

The edge of Δ[n] from a to b ends at b.

theorem SSet.stdSimplex.subcomplex_hom_app_apply {d n a : ℕ} {S : (stdSimplex.obj { len := d }).Subcomplex} (g : S.toSSet ⟶ stdSimplex.obj { len := n }) (x : (stdSimplex.obj { len := d }).obj (Opposite.op { len := a })) (hx : x ∈ S.obj (Opposite.op { len := a })) (t : Fin (a + 1)) (ht : obj₀Equiv.symm (x t) ∈ S.obj (Opposite.op { len := 0 })) : ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := a }))) ⟨x, hx⟩) t = ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) ⟨obj₀Equiv.symm (x t), ht⟩) 0

A map g from a subcomplex S of Δ[d] to Δ[n] acts on vertices: the t-th vertex of the image of a simplex x of S is the image of the t-th vertex of x.

theorem SSet.stdSimplex.yonedaEquiv_eq_app_id {X : SSet} {n : ℕ} (f : stdSimplex.obj { len := n } ⟶ X) : yonedaEquiv f = (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) (yonedaEquiv (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := n })))

The simplex of X corresponding to a map f : Δ[n] ⟶ X is the image under f of the top simplex of Δ[n].

theorem SSet.stdSimplex.hom_app_obj₀Equiv_symm {d d' : ℕ} (g : stdSimplex.obj { len := d' } ⟶ stdSimplex.obj { len := d }) (j : Fin (d' + 1)) : (CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 0 }))) (obj₀Equiv.symm j) = obj₀Equiv.symm ((yonedaEquiv g) j)

A map of standard simplices g : Δ[d'] ⟶ Δ[d] sends the vertex j of Δ[d'] to the vertex yonedaEquiv g j of Δ[d].

theorem SSet.stdSimplex.edge_edge_apply_zero {n : ℕ} {y x : (stdSimplex.obj { len := n }).obj (Opposite.op { len := 0 })} (e : Edge y x) : e.edge 0 = y 0

The vertex 0 of an edge of Δ[n] from y to x is the vertex y, the face δ 1 of the edge.

theorem SSet.stdSimplex.edge_edge_apply_one {n : ℕ} {y x : (stdSimplex.obj { len := n }).obj (Opposite.op { len := 0 })} (e : Edge y x) : e.edge 1 = x 0

The vertex 1 of an edge of Δ[n] from y to x is the vertex x, the face δ 0 of the edge.

instance SSet.stdSimplex.subsingleton_edge {n : ℕ} (y x : (stdSimplex.obj { len := n }).obj (Opposite.op { len := 0 })) : Subsingleton (Edge y x)

A standard simplex has at most one edge between any two vertices: an edge of Δ[n] is determined by its endpoints.

theorem SSet.stdSimplex.nonempty_edge_iff {n : ℕ} (a b : Fin (n + 1)) : Nonempty (Edge (obj₀Equiv.symm a) (obj₀Equiv.symm b)) ↔ a ≤ b

The standard simplex Δ[n] has an edge from the vertex a to the vertex b exactly when a ≤ b.

instance SSet.stdSimplex.quasicategory (n : ℕ) : (stdSimplex.obj { len := n }).Quasicategory

Standard simplices are quasicategories, being isomorphic to nerves of linear orders.

instance SSet.stdSimplex.isConnected (n : ℕ) : (stdSimplex.obj { len := n }).IsConnected

Standard simplices are connected: the edge from 0 to k joins every vertex k to the initial vertex.

noncomputable def SSet.stdSimplex.contraction (n : ℕ) : Homotopy (SSet.const (obj₀Equiv.symm 0)) (CategoryTheory.CategoryStruct.id (stdSimplex.obj { len := n }))

The contraction of the standard simplex Δ[n] onto its initial vertex: the homotopy from the constant map at 0 to the identity which is 0 over the vertex 0 of Δ[1] and the identity over the vertex 1.

theorem SSet.horn_one_ι_eq_const (i : Fin 2) : (horn 1 i).ι = const (stdSimplex.obj₀Equiv.symm i)

The horn Λ[1, i] is the vertex i of Δ[1]: every simplex of it is constant at i.

def SSet.fstStdSimplexZeroIso (K : SSet) : CategoryTheory.MonoidalCategoryStruct.tensorObj K (stdSimplex.obj { len := 0 }) ≅ K

The projection K ⊗ Δ[0] ⟶ K is an isomorphism, Δ[0] being terminal.

@[simp]

theorem SSet.fstStdSimplexZeroIso_hom (K : SSet) : K.fstStdSimplexZeroIso.hom = CategoryTheory.SemiCartesianMonoidalCategory.fst K (stdSimplex.obj { len := 0 })

@[simp]

theorem SSet.fstStdSimplexZeroIso_inv (K : SSet) : K.fstStdSimplexZeroIso.inv = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id K) (stdSimplex.isTerminalObj₀.from K)

instance SSet.instIsIsoFstObjSimplexCategoryStdSimplexMkOfNatNat_tauCeti (K : SSet) : CategoryTheory.IsIso (CategoryTheory.SemiCartesianMonoidalCategory.fst K (stdSimplex.obj { len := 0 }))

The projection K ⊗ Δ[0] ⟶ K is an isomorphism.

instance SSet.boundary.isConnected (n : ℕ) : (boundary (n + 2)).toSSet.IsConnected

The boundary ∂Δ[n + 2] is connected: it contains every edge of Δ[n + 2], in particular the edge from 0 to each vertex.