nLab
simplicial object in an (infinity,1)-category

Context

(,1)-Category theory

Internal (,1)-Categories

Contents

Definition

Definition

For 𝒞 an (∞,1)-category, a simplicial object in 𝒞 is an (∞,1)-functor

X:Δ op𝒞X \colon \Delta^{op} \to \mathcal{C}

from the opposite category of the simplex category into 𝒞.

The (,1)-category of simplicial objects in 𝒞 and morphisms between them is the (∞,1)-category of (∞,1)-functors

𝒞 Δ op=Func (Δ op,𝒞).\mathcal{C}^{\Delta^{op}} = Func_\infty(\Delta^{op}, \mathcal{C}) \,.

For instance (Lurie, def. 6.1.2.2).

Properties

Powering over simplicial sets

Assume that 𝒞 has all (∞,1)-limits. The following is a model for the powering of simplicial objects in 𝒞 by simplicial sets.

Definition

Let 𝒞QCatsSet be an (∞,1)-category incarnated as a quasi-category, and let X:Δ op𝒞 be a simplicial object. Then for KsSet any simplicial set, write

X[K]:Δ /K opΔ opX𝒞X[K] \colon \Delta_{/K}^{op} \to \Delta^{op} \stackrel{X}{\to} \mathcal{C}

for the the composite (∞,1)-functor of X with the projection from (the opposite category of) the category of simplices of K, and write

X(K):lim(Δ /K opΔ opX𝒞)X(K) \colon \underset{\leftarrow}{\lim} \left( \Delta_{/K}^{op} \to \Delta^{op} \stackrel{X}{\to} \mathcal{C} \right)

for the (∞,1)-limit over it (if it exists).

This is discussed in (Lurie HTT 4.2.3, notation 6.1.2.5). See also around (Lurie 2, notation 1.1.7).

Remark

The inclusion Δ /K ndΔ K of the full subcategory on non-degenerate simplicies is a homotopy cofinal functor (as discussed there). Therefore the (,1)-limit in def. 2 may equivalently be taken over this category of non-degenerate simplices.

Example

For K=Δ 1 Δ 0Δ 1 the simplicial set consisting of two consecutive edges, we have for X 𝒞 Δ that

X(K)X 1×X 0X 1X(K) \simeq X_1 \underset{X_0}{\times} X_1

is the homotopy fiber product in

X(K) X 1 X 1 1 0 X 0.\array{ && X(K) \\ & \swarrow && \searrow \\ X_1 &&&& X_1 \\ & {}_{\mathllap{\partial_1}}\searrow && \swarrow_{\mathrlap{\partial_0}} \\ && X_0 } \,.
Example

For K=Δ n itself an n-simplex, for some n the powering reduces to evaluation on that simplex:

X(Δ n)X n.X(\Delta^n) \simeq X_n \,.

This is because the category of non-degenerate simplices of an n-simplex has a terminal object (namely that n-simplex itself), and so its opposite category has an initial object and the (,1)-limit over a diagram with initial object is given by evaluation at that initial object.

Remark

For X 𝒞 Δ op and KK the following are equivalent

  1. the induced morphism of cone (,1)-categoris 𝒞 X[K]𝒞 X[K] is an equivalence of (∞,1)-categories;

  2. the induced morphism of (∞,1)-limits X(K)X(K) is an equivalence.

(The first perspective is used in (Lurie), the second in (Lurie2).)

Proof

In one direction: the limit is the terminal object in the cone category, and so is preserved by equivalences of cone categories. (This direction appears as (Lurie, prop. 4.1.1.8)). Conversely, the limits is the object representing cones, and hence an equivalence of limits induces an equivalence of cone categories.

Proposition

Let X:Δ op𝒞 be a simplicial object which is a groupoid object in an (∞,1)-category.

If KK is a morphism in sSet which is a weak homotopy equivalence and a bijection on vertices, then the induced morphism on slice-(∞,1)-categories

𝒞 /X[K]𝒞 /X[K]\mathcal{C}_{/X[K]} \to \mathcal{C}_{/X[K']}

is an equivalence of (∞,1)-categories (a weak equivalence in the model structure for quasi-categories).

Equivalently, by remark 1, we have an equivalence

X(K)X(K).X(K) \to X(K') \,.

This is (Lurie, prop. 6.1.2.6).

Cohesion

If 𝒞=H is an (∞,1)-topos then 𝒞 Δ op is a cohesive (∞,1)-topos over H. For more see at cohesive (∞,1)-topos - Examples - Simplicial objects.

Internal language

If 𝒞 is a locally cartesian closed (∞,1)-category whose internal language is homotopy type theory, then the internal language of 𝒞 Δ op is that homotopy type theory equipped with the axioms for a linear interval object. (…)

Examples

Internal category objects

Reference

Section 6.1.2 of

Related discussion is also in

Revised on December 4, 2012 10:58:53 by Urs Schreiber (82.169.65.155)