03.12.35 · modern-geometry / homotopy

Simplicial model category and the function complex

shipped3 tiersLean: partial

Anchor (Master): Quillen 1967 *Homotopical Algebra* (Springer LNM 43) §II.1-§II.3 (originator of simplicial model categories and the SM7 axiom); Goerss-Jardine 2009 *Simplicial Homotopy Theory* §II.2-§II.3 (function complexes and the Kan-complex theorem); Hirschhorn 2003 *Model Categories and Their Localizations* §9.1-§9.4 (modern treatment with cofibrantly generated machinery); Hovey 1999 *Model Categories* §4.2-§4.3 (monoidal-model-category framework subsuming simplicial enrichment); Riehl 2014 *Categorical Homotopy Theory* §10 (homotopy-coherent diagrams via simplicial enrichment); Lurie 2009 *Higher Topos Theory* §A.3 (relation to $(\infty, 1)$-categories)

Intuition [Beginner]

A simplicial model category is a model category in which every Hom set has been replaced by a Hom space — concretely, a simplicial set $Map (X, Y)$ that records not only the morphisms from $X$ to $Y$ but also the homotopies between them, the homotopies between homotopies, and so on. Where the underlying model category records only the bare morphism set $Hom (X, Y)$ , the simplicial enrichment records an entire combinatorial object whose vertices are morphisms, whose edges are homotopies, whose triangles are higher coherences, and whose higher-dimensional simplices record the tower of homotopies-between-homotopies.

The framework matters because abstract homotopy theory is fundamentally about spaces of maps, not just sets of maps modulo homotopy. The classical homotopy category $Ho (C)$ remembers $π_{0}$ of the mapping space — the set of homotopy classes — but discards everything in higher dimensions. A simplicial model category retains the full mapping space as a Kan complex, and from this Kan complex you can read off the higher homotopy groups, the higher coherences, and the structure of the derived category as an $(\infty, 1)$ -category rather than just an ordinary category.

The reader should hold a single picture: a simplicial model category is a workshop with three labelled toolboxes (the weak equivalences, fibrations, cofibrations from the underlying model structure) plus a recording device that captures every morphism, every homotopy, and every higher coherence as a combinatorial simplex. The recording device is the simplicial Hom; the calculus of recording is the SM7 pushout-product axiom; the output of recording is the function complex as a Kan complex.

Visual [Beginner]

A schematic showing two objects $X, Y$ of a simplicial model category with the function complex $Map (X, Y)$ drawn as a small simplicial set above them. The vertices of $Map (X, Y)$ are dots labelled $f, g, h$ representing morphisms $X \to Y$ ; the edges are lines labelled $α : f \Rightarrow g$ representing homotopies; one filled triangle records a homotopy of homotopies.

A side diagram shows the SM7 pushout-product configuration: a cofibration $i : A ↪ B$ in the base category, a monomorphism $j : K ↪ L$ in simplicial sets, and the resulting pushout-product map running into the tensor product of $B$ with $L$ , assembled from the smaller tensor pieces at the centre.

The picture captures the central organising principle: the simplicial enrichment promotes every morphism set to a Kan complex of higher coherences, and the SM7 axiom is the compatibility constraint that makes this enrichment interact correctly with the three classes of the underlying model structure.

Worked example [Beginner]

Build the function complex $Map (Δ^{0}, K)$ in the prototypical simplicial model category $sSet$ — simplicial sets with the Kan-Quillen model structure — for a Kan complex $K$ , and check that it recovers $K$ itself.

Step 1. The category is $sSet$ , with objects simplicial sets and morphisms simplicial maps. The model structure has weak equivalences the maps whose geometric realisation is a weak homotopy equivalence, fibrations the Kan fibrations, and cofibrations the monomorphisms. The simplicial enrichment is given by the internal Hom: $Map (K, L)$ is the simplicial set whose $n$ -simplices are the simplicial maps $Δ^{n} \times K \to L$ .

Step 2. The standard $0$ -simplex $Δ^{0}$ is the simplicial set with exactly one $n$ -simplex in every dimension $n \geq 0$ , all of which are degenerate. A simplicial map $Δ^{0} \to K$ is just a $0$ -simplex of $K$ — a vertex.

Step 3. Compute $Map (Δ^{0}, K)$ . By the internal-Hom formula, the $n$ -simplices of $Map (Δ^{0}, K)$ are the simplicial maps $Δ^{n} \times Δ^{0} \to K$ . Since $Δ^{n} \times Δ^{0} = Δ^{n}$ , this is the set of simplicial maps $Δ^{n} \to K$ , which by the Yoneda lemma is the set $K_{n}$ of $n$ -simplices of $K$ . So $Map (Δ^{0}, K) = K$ as a simplicial set.

Step 4. Check the Kan-complex conclusion. The headline theorem says $Map (X, Y)$ is a Kan complex whenever $X$ is cofibrant and $Y$ is fibrant in the underlying model structure. Here $X = Δ^{0}$ is cofibrant (every simplicial set is, in Kan-Quillen — the cofibrations are the monomorphisms, and $\emptyset ↪ Δ^{0}$ is one), and $Y = K$ is fibrant by hypothesis (Kan complexes are exactly the fibrant simplicial sets). The conclusion: $Map (Δ^{0}, K) = K$ is a Kan complex, which we knew from the hypothesis. The framework is consistent.

What this tells us: the function complex recovers the original object as a special case, and the framework's content lies in the substantive function complexes $Map (X, Y)$ for general $X, Y$ . The simplicial enrichment is the natural setting for thinking of every Hom as a homotopy type, with the headline theorem making this rigorous: the Hom is a Kan complex (a combinatorial model for a topological space) whose vertices are morphisms and whose edges record the homotopy relations.

Check your understanding [Beginner]

Exercise (easy, multiple choice).

A simplicial model category $C$ is, in addition to being a model category, enriched over which category?

A. The category of sets. B. The category of topological spaces. C. The category of simplicial sets. D. The category of chain complexes.

Hint

The "simplicial" qualifier refers to the structure used for the enrichment. A simplicial set is the combinatorial model of a space.

Answer

C. The category of simplicial sets. A simplicial model category replaces every $Hom$ set with a simplicial set $Map (X, Y) \in sSet$ , and the composition and unit maps are themselves simplicial. Topological enrichment (option B) gives a topological model category, which is a related but distinct framework. Set-enrichment (option A) is the bare ordinary-category structure with no enrichment, and chain-complex enrichment (option D) is the differential-graded analogue.

Exercise (easy, multiple choice).

The SM7 pushout-product axiom of a simplicial model category says: given a cofibration $i$ in the underlying model category and a monomorphism $j$ of simplicial sets, the pushout-product $i □ j$ is:

A. A weak equivalence. B. A cofibration in the underlying model category. C. A fibration in the underlying model category. D. A Kan fibration of simplicial sets.

Hint

The pushout-product lives in the same category as $i$ . SM7 also asserts that $i □ j$ is acyclic whenever either factor is acyclic.

Answer

B. A cofibration in the underlying model category. The SM7 axiom states that the pushout-product of a cofibration in $C$ with a monomorphism in $sSet$ lives in $C$ and is again a cofibration, and is moreover acyclic whenever either of the two factors is acyclic. This is the precise compatibility condition between the simplicial enrichment and the model structure.

Formal definition [Intermediate+]

Definition (Quillen 1967, simplicial category). A simplicial category is a category $C$ enriched over the cartesian-closed category $sSet$ of simplicial sets. Concretely, for every pair $X, Y \in Ob (C)$ there is a simplicial set $Map_{C} (X, Y) \in sSet$ (the function complex, or simplicial Hom), together with simplicial composition maps $$ \mathrm{Map}\mathcal{C}(Y, Z) \times \mathrm{Map}\mathcal{C}(X, Y) \xrightarrow{\circ} \mathrm{Map}\mathcal{C}(X, Z) $$ and unit maps $id_{X} : Δ^{0} \to Map_{C} (X, X)$ satisfying the associativity and unit axioms in the enriched-category sense. The set of $0$ -simplices $\mathrm{Map}\mathcal{C}(X, Y)_0 $r eco v er s t h e u n d er l y in g$ \mathrm{Hom}$ set of an ordinary category, and the structure of the higher simplices records the homotopy-coherent data.

Definition (Quillen 1967, simplicial model category). A simplicial model category is a model category $C$ that is also a simplicial category, in such a way that the following three axioms hold.

(SM0) Underlying category. The underlying ordinary category of the simplicial enrichment coincides with the underlying ordinary category of the model structure: $Hom_{C} (X, Y) = Map_{C} (X, Y)_{0}$ as sets.

(SM6) Tensor and cotensor. For every $X \in C$ and $K \in sSet$ , there exist objects $X \otimes K \in C$ (the tensor) and $X^{K} \in C$ (the cotensor), together with natural isomorphisms of simplicial sets $$ \mathrm{Map}\mathcal{C}(X \otimes K, Y) \cong \mathrm{Map}\mathbf{sSet}(K, \mathrm{Map}\mathcal{C}(X, Y)) \cong \mathrm{Map}\mathcal{C}(X, Y^K). $$ Equivalently, the bifunctor $- \otimes - : C \times sSet \to C$ is a left adjoint in both variables, with right adjoints $X \mapsto Map_{C} (X, -)$ and $K \mapsto X^{K}$ .

(SM7) Pushout-product axiom. Let $i : A \to B$ be a cofibration in $C$ and $j : K \to L$ a monomorphism in $sSet$ (equivalently, a cofibration in the Kan-Quillen model structure). The pushout-product of $i$ and $j$ is the canonical morphism $$ i \square j : (A \otimes L) \sqcup_{A \otimes K} (B \otimes K) \to B \otimes L $$ from the pushout of $A \otimes L \leftarrow A \otimes K \to B \otimes K$ to the tensor product $B \otimes L$ , induced by $i \otimes id_{L}$ and $id_{B} \otimes j$ . The axiom asserts: $i □ j$ is a cofibration in $C$ , and is moreover a weak equivalence whenever either $i$ or $j$ is a weak equivalence.

Definition (function complex of a simplicial model category). The function complex $Map_{C} (X, Y)$ is the simplicial Hom of the enriched category. In a simplicial model category, the derived function complex (or derived mapping space) is $RMap (X, Y) := Map_{C} (QX, R Y)$ , where $Q$ and $R$ are cofibrant and fibrant replacement functors. The derived function complex is independent of the choice of replacement up to canonical homotopy equivalence of Kan complexes.

Counterexamples to common slips

A simplicial enrichment of a model category is not automatic. The Quillen-Serre model structure on $Top$ is naturally a topological model category (enriched over $Top$ rather than $sSet$ ); the simplicial enrichment requires the singular-complex / realisation adjunction to transfer the topological structure to simplicial sets. The result is a simplicial model category, but the simplicial enrichment is an extra piece of structure beyond the model structure.
The SM7 axiom is not equivalent to saying that $i \otimes id_{K}$ is a cofibration whenever $i$ is a cofibration and $K$ is a simplicial set. The pushout-product is the stronger and correct condition; the bare tensor $i \otimes id_{K}$ being a cofibration is only the special case $j = \emptyset \to K$ (which is not a monomorphism between non-empty simplicial sets in general — the source is empty).
The cotensor $X^{K}$ is not the categorical exponential in $C$ unless $C$ is cartesian closed. The cotensor is the simplicial-set-indexed limit characterised by the SM6 adjunction; it lives in $C$ but its underlying object is a more refined construction than the ordinary product or exponential.
The function complex $Map (X, Y)$ need not be a Kan complex in general — only when $X$ is cofibrant and $Y$ is fibrant. Without these hypotheses, $Map (X, Y)$ is a simplicial set whose homotopy groups do not in general compute the derived mapping space; one must replace to obtain $RMap (X, Y)$ .

Key theorem with proof [Intermediate+]

Theorem (Quillen 1967, §II.2 Proposition 3). Let $C$ be a simplicial model category. For any cofibrant object $X \in C$ and any fibrant object $Y \in C$ , the function complex $Map_{C} (X, Y)$ is a Kan complex.

Proof. We show that every horn $Λ_{k}^{n} \to Map_{C} (X, Y)$ extends to a simplex $Δ^{n} \to Map_{C} (X, Y)$ , for every $n \geq 1$ and every $0 \leq k \leq n$ . By the SM6 adjunction $Map_{sSet} (K, Map_{C} (X, Y)) ≅ Map_{C} (X \otimes K, Y)$ , a horn $Λ_{k}^{n} \to Map_{C} (X, Y)$ corresponds to a morphism $f : X \otimes Λ_{k}^{n} \to Y$ in $C$ .

We seek an extension $\tilde{f} : X \otimes Δ^{n} \to Y$ to a full simplex. The extension exists by an SM7 lifting argument. Consider the commutative square in $C$ : $$ \begin{array}{ccc} X \otimes \Lambda^n_k & \xrightarrow{f} & Y \ \downarrow \mathrm{id}_X \otimes j & & \downarrow p \ X \otimes \Delta^n & \xrightarrow{} & * \end{array} $$ where $j : Λ_{k}^{n} ↪ Δ^{n}$ is the horn inclusion (a monomorphism in $sSet$ ), and $p : Y \to *$ is the unique map to the terminal object (a fibration in $C$ because $Y$ is fibrant).

The left vertical morphism is $id_{X} \otimes j$ . This is the pushout-product of $i_{X} : \emptyset \to X$ (a cofibration because $X$ is cofibrant) with $j : Λ_{k}^{n} \to Δ^{n}$ (a monomorphism in $sSet$ ). Explicitly, $$ i_X \square j : (\emptyset \otimes \Delta^n) \sqcup_{\emptyset \otimes \Lambda^n_k} (X \otimes \Lambda^n_k) \to X \otimes \Delta^n. $$ Since the tensor with $\emptyset$ is initial in $C$ , the pushout simplifies to $X \otimes Λ_{k}^{n}$ , and the pushout-product becomes $id_{X} \otimes j : X \otimes Λ_{k}^{n} \to X \otimes Δ^{n}$ .

The horn inclusion $j : Λ_{k}^{n} \to Δ^{n}$ is an acyclic cofibration in the Kan-Quillen model structure on $sSet$ : it is a monomorphism (cofibration) by definition, and its geometric realisation $∣ j ∣ : ∣ Λ_{k}^{n} ∣ \to ∣ Δ^{n} ∣$ is a deformation retraction, hence a weak homotopy equivalence. So $j$ is an acyclic monomorphism in $sSet$ .

By the SM7 axiom in its acyclic form, the pushout-product $i_{X} □ j$ is an acyclic cofibration in $C$ . The lifting square above has an acyclic cofibration on the left and a fibration on the right; by the M3 lifting axiom of the model category $C$ , a diagonal lift $\tilde{f} : X \otimes Δ^{n} \to Y$ exists with $\tilde{f} \circ (id_{X} \otimes j) = f$ .

The morphism $\tilde{f}$ corresponds under SM6 to a simplicial map $Δ^{n} \to Map_{C} (X, Y)$ extending the original horn map $Λ_{k}^{n} \to Map_{C} (X, Y)$ . The horn-filling condition is satisfied for every $n, k$ , so $Map_{C} (X, Y)$ is a Kan complex. $□$

Bridge. This theorem builds toward 03.12.31 (Quillen model category) by upgrading the bare $Hom$ -set calculus of the model category to a $Map$ -Kan-complex calculus that carries the full homotopy-coherent data, and appears again in 03.12.25 (simplicial sets and geometric realization) where the Kan-Quillen model structure on $sSet$ is the prototype: every fibrant simplicial set is a Kan complex, and the function complex $Map (Δ^{0}, K) = K$ recovers the original Kan complex as a special case. The foundational reason the argument works is that SM7 is exactly the compatibility condition needed for horn-filling: the acyclic-cofibration property of the simplicial horn inclusion transports along the pushout-product to give an acyclic cofibration in $C$ , and the M3 lifting axiom does the rest.

This is exactly the structure that identifies the derived mapping space with the function complex of cofibrant-fibrant replacements: the bridge is between the ordinary $Hom$ set in the homotopy category and the simplicial Kan complex computing it, via the SM7-driven horn-filling argument. The central insight is that the tensor with the standard simplices $Δ^{n}$ provides a coherent system of cylinders, so that homotopies of any height are recorded simultaneously rather than constructed one dimension at a time. Putting these together, the simplicial-model-category framework converts the model-theoretic notion of homotopy into the combinatorial Kan-complex calculus, generalises the classical homotopy-class set $π_{0} Map (X, Y) = [X, Y]$ to the full homotopy type of $Map (X, Y)$ , and is dual to the cocylinder construction in topological model categories that yields the same Kan complex via the singular-complex functor.

Exercises [Intermediate+]

Exercise 2 (easy, true-false).

True or false: the pushout-product axiom SM7 implies that for any cofibration $i : A \to B$ in $C$ , the tensor $i \otimes id_{K} : A \otimes K \to B \otimes K$ is a cofibration in $C$ for every simplicial set $K$ .

Hint

Apply SM7 with $j : \emptyset \to K$ — this is a monomorphism of simplicial sets when $K$ is non-empty, and the pushout-product simplifies.

Answer

True. Take $j : \emptyset \to K$ , the unique map from the empty simplicial set. This is a monomorphism. The pushout-product $i □ j$ is the canonical map $(A \otimes K) ⊔_{A \otimes \emptyset} (B \otimes \emptyset) \to B \otimes K$ ; since the tensor with $\emptyset$ is the initial object of $C$ , the pushout simplifies to $A \otimes K$ , and the pushout-product becomes $i \otimes id_{K} : A \otimes K \to B \otimes K$ . SM7 asserts this is a cofibration in $C$ . The same logic with $j$ replaced by $K \to *$ (a monomorphism if $K$ is non-empty) yields a cotensor-side statement.

Exercise 3 (medium, symbolic).

Compute the function complex $Map_{sSet} (Δ^{1}, K)$ for a Kan complex $K$ , and identify its $0$ -simplices and $1$ -simplices.

Hint

The $n$ -simplices of $Map_{sSet} (Δ^{1}, K)$ are the simplicial maps $Δ^{n} \times Δ^{1} \to K$ . Use the formula for the prism $Δ^{n} \times Δ^{1}$ in terms of $Δ^{n + 1}$ -simplices.

Answer

The $0$ -simplices of $Map_{sSet} (Δ^{1}, K)$ are the simplicial maps $Δ^{0} \times Δ^{1} \to K = Δ^{1} \to K$ , which by Yoneda are the $1$ -simplices $K_{1}$ . So $Map_{sSet} (Δ^{1}, K)_{0} = K_{1}$ : a vertex of the function complex is an edge of $K$ .

The $1$ -simplices are the simplicial maps $Δ^{1} \times Δ^{1} \to K$ . The product $Δ^{1} \times Δ^{1}$ is the square, which has a non-degenerate combinatorial structure: two non-degenerate $2$ -simplices (the two triangles into which the square decomposes) plus their faces. A simplicial map from the square to $K$ records a commutative square in $K$ up to a specified homotopy filling the square diagonally.

Equivalently, $Map_{sSet} (Δ^{1}, K) = K^{Δ^{1}}$ is the path object of $K$ : its vertices are edges of $K$ , its edges are square-shaped homotopies between edges, and the higher simplices record higher coherences. The path-object structure is the foundation of the simplicial-set notion of homotopy: two vertices $a, b \in K_{0}$ are homotopic if and only if there is an edge $a \to b$ in $K^{Δ^{1}}$ projecting to $(a, b)$ under the endpoint map $K^{Δ^{1}} \to K \times K$ . Rubric: full credit for the Yoneda identification of $0$ -simplices and the square-shape description of $1$ -simplices.

Exercise 4 (medium, short-answer).

Show that in the projective model structure on $Ch_{\geq 0} (R)$ , the chain complex $Map (C, D)$ of two chain complexes is a Kan complex when $C$ is cofibrant (i.e. degree-wise projective).

Hint

The Dold-Kan correspondence relates chain complexes to simplicial abelian groups; under this correspondence, the chain-complex Hom becomes a simplicial Hom, and the projective-cofibrant condition transports to a degenerate simplex condition.

Answer

The category $Ch_{\geq 0} (R)$ with the projective model structure (cofibrations the degree-wise injections with projective cokernel, fibrations the degree-wise surjections in positive degree, weak equivalences the quasi-isomorphisms) is a simplicial model category whose simplicial enrichment comes via the Dold-Kan correspondence with simplicial $R$ -modules.

The Dold-Kan correspondence is an equivalence of categories $K : Ch_{\geq 0} (R) ≅ sMod_{R} : N$ , where $N$ is the normalised chain functor and $K$ its inverse. Under this equivalence, the simplicial structure on $sMod_{R}$ (via $Hom_{R} (K \otimes Z [-], -)$ ) transports to a simplicial structure on $Ch_{\geq 0} (R)$ .

For the function complex, $Map_{Ch_{\geq 0} (R)} (C, D)$ is defined via the chain-complex internal Hom: its $n$ -simplices are chain maps $C \otimes \tilde{N} (Δ^{n}) \to D$ , where $\tilde{N} (Δ^{n})$ is the normalised chain complex of the standard $n$ -simplex. When $C$ is degree-wise projective, every horn-filling problem in $Map (C, D)$ reduces to a lifting problem against the surjection $D_{n} ↠ D_{n} / im (boundary)$ , which is solvable because projective modules satisfy the lifting property against surjections.

The conclusion is that $Map (C, D)$ is a Kan complex whenever $C$ is cofibrant and $D$ is fibrant in the projective structure. Since every chain complex is fibrant in the projective structure (fibrations are only required to be surjective in positive degree), the result simplifies: $Map (C, D)$ is a Kan complex for every $C$ degree-wise projective and every $D$ . Rubric: full credit for invoking Dold-Kan and the projective-lifting argument.

Exercise 5 (medium, short-answer).

State and prove the dual SM7 axiom for the cotensor: in a simplicial model category, if $p : E \to B$ is a fibration in $C$ and $j : K \to L$ is a monomorphism in $sSet$ , the cotensor pullback-power $p^{j} : E^{L} \to B^{L} \times_{B^{K}} E^{K}$ is a fibration in $C$ .

Hint

The pullback-power is the dual of the pushout-product. Apply the SM6 adjunctions to convert a lifting problem for $p^{j}$ into a lifting problem for $i □ j$ , and use SM7 for the pushout-product side.

Answer

Statement. In a simplicial model category, if $p : E \to B$ is a fibration and $j : K \to L$ is a monomorphism in $sSet$ , the pullback-power $$ p^j : E^L \to B^L \times_{B^K} E^K $$ is a fibration in $C$ , and is moreover acyclic if either $p$ or $j$ is acyclic.

Proof. Use the lifting characterisation. The pullback-power $p^{j}$ is a fibration iff it has the right lifting property against every acyclic cofibration $i : A \to B^{'}$ in $C$ . A lifting square against $p^{j}$ : $$ \begin{array}{ccc} A & \xrightarrow{} & E^L \ \downarrow i & & \downarrow p^j \ B' & \xrightarrow{} & B^L \times_{B^K} E^K \end{array} $$ is adjoint by SM6 to the lifting square $$ \begin{array}{ccc} (A \otimes L) \sqcup_{A \otimes K} (B' \otimes K) & \xrightarrow{} & E \ \downarrow i \square j & & \downarrow p \ B' \otimes L & \xrightarrow{} & B \end{array} $$ The left morphism is $i □ j$ , the pushout-product of the acyclic cofibration $i$ with the monomorphism $j$ . By SM7, $i □ j$ is an acyclic cofibration in $C$ . The right morphism is the fibration $p$ . By M3 in $C$ , a diagonal lift exists; the lift corresponds under SM6 to a lift in the original square. Hence $p^{j}$ has the right lifting property against every acyclic cofibration $i$ , so $p^{j}$ is a fibration. The acyclic case is symmetric.

This dual formulation is sometimes taken as the primary form of SM7 (Hovey 1999 §4.2 uses the pushout-product, Hirschhorn 2003 §9.1 uses the pullback-power; the two are equivalent by the SM6 adjunction). Rubric: full credit for the adjunction conversion and the SM7 application.

Exercise 6 (medium, symbolic).

In the Kan-Quillen model structure on $sSet$ (viewed as a simplicial model category over itself), compute the function complex $Map (Δ^{1}, Δ^{1})$ and identify its homotopy type.

Hint

Both source and target are cofibrant; the target is not fibrant ( $Δ^{1}$ is not a Kan complex, since horns at vertices cannot be filled in $Δ^{1}$ alone). Pass to the fibrant replacement $Ex^{\infty} (Δ^{1})$ first.

Answer

The standard simplex $Δ^{1}$ is not a Kan complex: the horn $Λ_{1}^{2}$ (with edges $0 \to 1$ and $0 \to 2$ ) cannot be filled to a $2$ -simplex $Δ^{2} \to Δ^{1}$ because $Δ^{1}$ has only two vertices and no $2$ -simplex (other than degenerate ones) maps non-degenerately to it. So $Map (Δ^{1}, Δ^{1})$ in the bare sense is not directly a Kan complex.

The derived function complex is $RMap (Δ^{1}, Δ^{1}) = Map (Δ^{1}, Ex^{\infty} Δ^{1})$ where $Ex^{\infty} Δ^{1}$ is the Kan replacement of $Δ^{1}$ via the Kan $Ex$ -functor (the right adjoint of barycentric subdivision iterated to a colimit). The geometric realisation of $Ex^{\infty} Δ^{1}$ is the unit interval $[0, 1]$ , and $Map (Δ^{1}, Ex^{\infty} Δ^{1})$ is the simplicial path space of $[0, 1]$ , homotopy-equivalent to $[0, 1]$ itself by the contraction onto endpoint maps.

So $RMap (Δ^{1}, Δ^{1}) ≃ [0, 1]$ as a Kan complex up to weak equivalence, with two homotopically-distinct vertices (the identity map and the swap; but the swap is not a simplicial map from $Δ^{1}$ to $Δ^{1}$ because $Δ^{1}$ is the ordered $1$ -simplex, so only the identity exists in $Map_{sSet} (Δ^{1}, Δ^{1})_{0}$ ). More carefully: $Map_{sSet} (Δ^{1}, Δ^{1})_{0} = Hom_{sSet} (Δ^{1}, Δ^{1})$ , and a simplicial map $Δ^{1} \to Δ^{1}$ is an order-preserving map ${0 < 1} \to {0 < 1}$ , of which there are exactly three: $0 \mapsto 0, 1 \mapsto 1$ (identity), $0 \mapsto 0, 1 \mapsto 0$ (collapse to $0$ ), $0 \mapsto 1, 1 \mapsto 1$ (collapse to $1$ ). The function complex is therefore a discrete simplicial set on three vertices in dimension $0$ ; passage to derived $RMap$ does not change this because the discrete simplicial set on three vertices is already a Kan complex.

Rubric: full credit for identifying the three order-preserving maps and noting that the discrete $3$ -point simplicial set is the function complex.

Exercise 7 (hard, short-answer).

Show that the geometric realisation functor $∣ - ∣ : sSet \to Top$ and the singular complex functor $Sing : Top \to sSet$ assemble into a simplicial Quillen equivalence between the Kan-Quillen model structure on $sSet$ and the Quillen-Serre model structure on $Top$ , when $Top$ is given the topological enrichment converted to a simplicial enrichment via $Sing$ .

Hint

A simplicial Quillen equivalence is a Quillen equivalence that is also enriched over $sSet$ : the natural isomorphism $∣ - ∣ ⊣ Sing$ should lift to a natural isomorphism of simplicial mapping spaces, not just $Hom$ sets.

Answer

The adjunction $∣ - ∣ ⊣ Sing$ at the level of $Hom$ sets reads $$ \mathrm{Hom}\mathbf{Top}(|K|, X) \cong \mathrm{Hom}\mathbf{sSet}(K, \mathrm{Sing}(X)) $$ for $K \in sSet$ and $X \in Top$ . To upgrade to a simplicial Quillen equivalence, we promote this to a natural isomorphism of simplicial mapping spaces: $$ \mathrm{Map}\mathbf{Top}^{\mathrm{Sing}}(|K|, X) \cong \mathrm{Map}\mathbf{sSet}(K, \mathrm{Sing}(X)), $$ where $Map_{Top}^{Sing} (X, Y) := Sing (Hom_{Top} (X, Y))$ is the simplicial enrichment of $Top$ transported from the topological enrichment via $Sing$ . Concretely, $Map_{Top}^{Sing} (X, Y)_{n} = Hom_{Top} (X \times ∣ Δ^{n} ∣, Y) = Sing (Y^{X})_{n}$ .

The simplicial enrichment is natural in both variables: a morphism $K \to K^{'}$ in $sSet$ and a morphism $X \to X^{'}$ in $Top$ induce the expected maps on simplicial Hom sets. The adjunction extends to a $sSet$ -enriched adjunction by the naturality.

For the Quillen-equivalence property: $∣ - ∣$ preserves cofibrations and acyclic cofibrations (mapped to relative cell complexes in $Top$ , which are Hurewicz/Serre cofibrations), so the adjunction is Quillen. The Quillen equivalence is Quillen's theorem II.3.1: for cofibrant $K \in sSet$ and fibrant $X \in Top$ (i.e. all spaces, every space is Serre-fibrant), a map $f : ∣ K ∣ \to X$ is a weak equivalence iff its adjoint $\tilde{f} : K \to Sing (X)$ is a weak equivalence. This follows from the unit $K \to Sing (∣ K ∣)$ being a weak equivalence (the CW approximation argument on the simplicial side) and the counit $∣ Sing (X) ∣ \to X$ being a weak equivalence (which is the geometric-realisation theorem for the singular simplicial set, proved by Milnor 1957).

The simplicial enrichment makes this Quillen equivalence into a simplicial Quillen equivalence in the sense of Hovey 1999 §4.2.18, meaning the induced equivalence on derived function complexes $$ \mathrm{RMap}\mathbf{Top}(|K|, X) \cong \mathrm{RMap}\mathbf{sSet}(K, \mathrm{Sing}(X)) $$ is a weak equivalence of Kan complexes for every $K, X$ . This is the foundational compatibility result that makes the simplicial-set model of homotopy theory equivalent to the topological model not just at the level of $π_{0}$ but at the full $\infty$ -categorical level. Rubric: full credit for the simplicial Hom upgrade, the SM6 naturality, and the Milnor-Quillen weak-equivalence argument.

Exercise 8 (hard, short-answer).

Prove that in any simplicial model category $C$ , the homotopy groups of the function complex $RMap (X, Y)$ are given by $$ \pi_n \mathrm{RMap}(X, Y) \cong [S^n \otimes X, Y]\mathcal{C} $$ for $n \geq 1$ , where $S^n = \partial \Delta^{n+1} / \partial \Delta^{n+1}{\text{degenerate}} $i s t h es im pl i c ia l$ n $- s p h er e an d$ [-, -]_\mathcal{C} $d e n o t es m or p hi s m s in$ \mathrm{Ho}(\mathcal{C})$.

Hint

Use the homotopy-group formula in terms of horn-filler equivalence classes, combined with the SM6 adjunction converting $Map (S^{n}, RMap (X, Y))$ into $Map (S^{n} \otimes X, Y)$ .

Answer

By the SM6 adjunction $Map_{sSet} (K, Map_{C} (X, Y)) ≅ Map_{C} (X \otimes K, Y)$ , we have for $K = S^{n}$ : $$ \mathrm{Map}\mathbf{sSet}(S^n, \mathrm{RMap}(X, Y)) \cong \mathrm{Map}\mathcal{C}(QX \otimes S^n, RY) = \mathrm{Map}_\mathcal{C}(S^n \otimes QX, RY). $$

Taking $π_{0}$ (the set of connected components) of both sides: $$ \pi_0 \mathrm{Map}\mathbf{sSet}(S^n, \mathrm{RMap}(X, Y)) = [S^n, \mathrm{RMap}(X, Y)]\mathbf{sSet} = \pi_n \mathrm{RMap}(X, Y), $$ where the last equality is the standard identification of homotopy classes of maps from $S^{n}$ into a Kan complex with the $n$ -th homotopy group (Goerss-Jardine §I.7). The right-hand side: $$ \pi_0 \mathrm{Map}\mathcal{C}(S^n \otimes QX, RY) = [S^n \otimes QX, RY]\mathcal{C} = [S^n \otimes X, Y]_\mathcal{C}, $$ where the last equality uses that morphisms in $Ho (C)$ are represented by morphisms between cofibrant-fibrant replacements modulo homotopy, and $QX, R Y$ are exactly such replacements.

Combining: $π_{n} RMap (X, Y) ≅ [S^{n} \otimes X, Y]_{C}$ , as claimed.

The formula generalises the classical homotopy-class identification $π_{n} Map (X, Y) = [Σ^{n} X, Y]$ for pointed CW complexes in $Top$ , where $Σ^{n} X = S^{n} \land X$ is the iterated suspension. In the simplicial-model-category framework, the suspension $Σ^{n}$ is replaced by the tensor with $S^{n}$ , and the homotopy-group formula is the universal statement of which the topological formula is the $Top$ -instance. Rubric: full credit for the SM6 adjunction, the $π_{0}$ identification on both sides, and the cofibrant-fibrant replacement argument.

Lean formalization [Intermediate+]

The simplicial-model-category framework is in early-stage formalisation in Mathlib through the Mathlib.AlgebraicTopology.* and Mathlib.CategoryTheory.Enriched.* namespaces. The intended shape of the formalisation is schematically the following.

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Closed.Cartesian
import Mathlib.AlgebraicTopology.SimplicialSet.Basic

namespace CategoryTheory

/-- A simplicial enrichment on a category C provides a simplicial
function complex Map(X, Y) and tensor / cotensor functors compatible
with SM6. -/
class SimplicialEnrichment (C : Type*) [Category C] where
  map           : C → C → SSet
  tensor        : C → SSet → C
  cotensor      : C → SSet → C
  tensorAdj     : ∀ (X : C) (K : SSet) (Y : C),
    (map (tensor X K) Y : SSet) ≅ ((SSet.internalHom K (map X Y)) : SSet)
  cotensorAdj   : ∀ (X : C) (K : SSet) (Y : C),
    (map X (cotensor Y K) : SSet) ≅ ((SSet.internalHom K (map X Y)) : SSet)

/-- A simplicial model category is a model category equipped with a
compatible simplicial enrichment satisfying SM0, SM6, SM7. -/
class SimplicialModelCategory (C : Type*) [Category C]
    extends ModelCategory C, SimplicialEnrichment C where
  /-- SM7: the pushout-product of a cofibration in C with a
  monomorphism in SSet is a cofibration in C. -/
  pushoutProduct_cof :
    ∀ {A B : C} (i : A ⟶ B), structure.cofibrations i →
    ∀ {K L : SSet} (j : K ⟶ L), Mono j →
    structure.cofibrations (pushoutProductMor i j)
  /-- SM7: the pushout-product is acyclic when either factor is. -/
  pushoutProduct_acyclic_left :
    ∀ {A B : C} (i : A ⟶ B), structure.cofibrations i →
                              structure.weakEquivalences i →
    ∀ {K L : SSet} (j : K ⟶ L), Mono j →
    structure.weakEquivalences (pushoutProductMor i j)
  pushoutProduct_acyclic_right :
    ∀ {A B : C} (i : A ⟶ B), structure.cofibrations i →
    ∀ {K L : SSet} (j : K ⟶ L), Mono j → SSet.WeakEquiv j →
    structure.weakEquivalences (pushoutProductMor i j)

/-- The headline theorem: in a simplicial model category, Map(X, Y)
is a Kan complex when X is cofibrant and Y is fibrant. -/
theorem map_is_kan_complex
    {C : Type*} [Category C] [SimplicialModelCategory C]
    (X Y : C) (hX : structure.cofibrations (terminal_from X))
    (hY : structure.fibrations (initial_to Y)) :
    SSet.KanComplex (SimplicialEnrichment.map X Y) := by
  sorry  -- horn-filling via SM7 applied to (∅ → X) □ (Λⁿₖ → Δⁿ)

end CategoryTheory

The Lean module accompanying this unit is Codex.Modern.Homotopy.SimplicialModelCategory, which sketches the SM7 pushout-product axiom and the Kan-complex theorem with sorry proof bodies. The formalisation gap is substantive: a complete SimplicialModelCategory API requires the underlying ModelCategory type-class (also pending in Mathlib), the enriched-category formalism with simplicial-set enrichment, the pushout-product construction in the model-category context, and a verified instance for the Kan-Quillen model structure on $sSet$ . Each piece is formalisable from existing Mathlib infrastructure but the assembly into a single usable API is the open target.

Advanced results [Master]

Simplicial enrichment and the SM7 axiom

Theorem (Quillen 1967, §II.2 Axioms SM0-SM7). A simplicial model category is a model category $C$ together with a simplicial enrichment $Map_{C} (-, -) : C^{op} \times C \to sSet$ , tensor and cotensor functors $- \otimes - : C \times sSet \to C$ and $-^{-} : C \times sSet^{op} \to C$ , and a coherence isomorphism implementing SM0, SM6, SM7. The axioms are sufficient to ensure that every classical homotopy-theoretic construction in $C$ enriches to a simplicial-Hom construction, with the SM7 axiom guaranteeing that the enrichment respects the model structure.

The SM7 axiom, written in its pushout-product form, asserts that the bifunctor $□$ on the arrow categories $C^{\to} \times sSet^{\to}$ takes the subcategory $(C_{C}) \times (Mono_{sSet})$ to $C_{C}$ , and takes the larger subcategory where either factor is acyclic to $C_{C} \cap W_{C}$ . This is the precise compatibility condition needed for the simplicial enrichment to interact correctly with the model structure: every classical lifting argument in $C$ has a simplicial version, and the simplicial version transports through SM6 to a horn-filling argument in $sSet$ .

Theorem (Hovey 1999, §4.2, monoidal model categories generalise simplicial model categories). Let $(V, \otimes, 1)$ be a closed symmetric monoidal model category with cofibrant unit. A model category $C$ enriched, tensored, and cotensored over $V$ in such a way that the pushout-product axiom holds for $V$ -cofibrations and $C$ -cofibrations is a $V$ -model category. The case $V = sSet$ with the Kan-Quillen model structure recovers Quillen's notion of a simplicial model category.

This generalisation matters because it shows the simplicial-enrichment framework is one instance of a more general principle: enrichment over any nice monoidal model category yields a parallel theory. Important other cases include $V = Top$ (topological model categories, with the Quillen-Serre model structure on $Top$ ), $V = Ch_{R}$ (differential graded model categories), and $V = Sp^{Σ}$ (spectral model categories, for stable homotopy theory).

Theorem (Hirschhorn 2003, §9.3, properties of the function complex). Let $C$ be a simplicial model category, $X$ cofibrant, $Y$ fibrant. Then:

(i) $Map_{C} (X, Y)$ is a Kan complex (Quillen's theorem above).

(ii) Weak equivalences $f : X^{'} \to X$ between cofibrant objects induce weak equivalences $Map_{C} (X, Y) \to Map_{C} (X^{'}, Y)$ .

(iii) Weak equivalences $g : Y \to Y^{'}$ between fibrant objects induce weak equivalences $Map_{C} (X, Y) \to Map_{C} (X, Y^{'})$ .

(iv) Cofibrations $i : A \to B$ between cofibrant objects induce Kan fibrations $Map_{C} (B, Y) \to Map_{C} (A, Y)$ for $Y$ fibrant.

The properties (ii) and (iii) are crucial for derived-functor calculus: they show that the function complex behaves as expected under weak equivalences, validating the notion of $RMap (X, Y)$ as a homotopy invariant of $X$ and $Y$ . Property (iv) is the simplicial-version of the M3 lifting axiom: cofibrations in $C$ induce fibrations on function complexes, the dual of the more familiar " $Map (X, -)$ preserves fibrations".

Function complex Map(X, Y) as the derived mapping space

Theorem (Dwyer-Kan 1980, Function complexes in homotopical algebra). For any model category $C$ , the simplicial localisation $L^{H} C$ (the hammock localisation of Dwyer-Kan 1980) is a simplicial category whose function complexes compute the derived mapping space. When $C$ is itself a simplicial model category, the natural map $RMap_{C} (X, Y) \to Map_{L^{H} C} (X, Y)$ is a weak equivalence of Kan complexes for every $X, Y \in C$ .

The Dwyer-Kan theorem gives the canonical comparison between two ways of obtaining derived mapping spaces: the simplicial-model-category approach (which requires extra structure but is computationally tractable) and the hammock-localisation approach (which works for any category with weak equivalences but is intrinsically more abstract). The equivalence between the two approaches is the foundational result that makes the simplicial-model-category framework legitimate as a model of $(\infty, 1)$ -categorical homotopy theory.

Theorem (Lurie 2009 §A.3.7, simplicial nerve and $(\infty, 1)$ -category presentation). The homotopy-coherent nerve construction $N^{h c} : sCat \to sSet$ assigns to a simplicial category $C$ a simplicial set $N^{h c} (C)$ whose $n$ -simplices encode homotopy-coherent diagrams of shape $[n]$ in $C$ . When $C$ is a simplicial model category restricted to cofibrant-fibrant objects, $N^{h c} (C_{cf})$ is a quasi-category (an $(\infty, 1)$ -category in the Joyal sense), and the homotopy category of this quasi-category coincides with $Ho (C)$ . The simplicial-model-category framework therefore presents an $(\infty, 1)$ -category in the Joyal-Lurie sense.

This theorem is the bridge from the simplicial-model-category framework to the $(\infty, 1)$ -categorical framework: every simplicial model category presents an $(\infty, 1)$ -category through its function complexes, and the equivalence of presentations is one of the Quillen equivalences in the model category $sCat$ of simplicial categories (Bergner 2007).

Theorem (Goerss-Jardine §II.3, homotopy groups of the function complex). Let $C$ be a pointed simplicial model category, $X$ cofibrant, $Y$ fibrant, with basepoint $f : X \to Y$ in $Map_{C} (X, Y)_{0}$ . Then for $n \geq 1$ : $$ \pi_n(\mathrm{Map}\mathcal{C}(X, Y), f) \cong [\Sigma^n X, Y]{\mathrm{Ho}(\mathcal{C}*)}, $$ *where $Σ^{n} X = S^{n} \otimes X$ is the iterated suspension of $X$ via the simplicial tensor with the simplicial sphere $S^{n}$ , and $[-, -]{\mathrm{Ho}(\mathcal{C}_)}$ denotes morphisms in the pointed homotopy category.

This recovers the classical formula for homotopy groups of mapping spaces in pointed CW complexes, where $π_{n} Map_{*} (X, Y) = [Σ^{n} X, Y]_{*}$ classically. The simplicial-model-category framework upgrades the classical pointed-CW formula to a general theorem holding in any pointed simplicial model category, and identifies the suspension functor $Σ$ as the tensor with the simplicial circle $S^{1} = Δ^{1} / \partial Δ^{1}$ .

Examples — sSet, simplicial groups, dg-algebras

Theorem (Quillen 1967 §II.3, $sSet$ is a simplicial model category). The category $sSet$ of simplicial sets, equipped with the Kan-Quillen model structure, is a simplicial model category. The simplicial enrichment is the internal Hom: $Map_{sSet} (K, L) = L^{K}$ where $L^{K}$ is the simplicial set with $n$ -simplices the simplicial maps $Δ^{n} \times K \to L$ . The tensor is the cartesian product $X \otimes K = X \times K$ , and the cotensor is the internal Hom $X^{K}$ .

The SM7 axiom in this case reduces to the statement that the product of a monomorphism and a monomorphism is a monomorphism, with acyclicity inheriting from either factor. This is verified directly from the Yoneda description of monomorphisms in $sSet$ as degree-wise injections, plus the fact that the Kan-Quillen weak equivalences are stable under products with arbitrary simplicial sets (a consequence of the realisation theorem that $∣ K \times L ∣ ≅ ∣ K ∣ \times ∣ L ∣$ in compactly-generated spaces, due to Milnor 1957).

Theorem (Quillen 1967 §II.4, simplicial groups). The category $sGp$ of simplicial groups, with weak equivalences the maps inducing isomorphisms on $π_{n}$ for $n \geq 0$ and fibrations the maps that are fibrations on the underlying simplicial sets, is a simplicial model category. The simplicial enrichment uses the internal Hom of simplicial groups (which is a simplicial set, not generally a simplicial group, because non-abelian group structure is not preserved by exponentiation). Every cofibrant simplicial group is a free simplicial group; every simplicial group is fibrant (a basic fact, Quillen 1967 §II.4 Proposition 1).

The simplicial-group case is foundational because Kan's loop functor $G : sSet_{*} \to sGp$ (assigning to a pointed simplicial set its simplicial loop group) and the corresponding classifying-space functor $\overset{ˉ}{W} : sGp \to sSet_{*}$ form a Quillen equivalence (Kan 1958, Quillen 1967 §II.4 Theorem 2). This gives a simplicial-group model for pointed connected homotopy types: every connected pointed homotopy type is represented by a simplicial group via this Quillen equivalence.

Theorem (Bousfield-Gugenheim 1976, simplicial commutative dg-algebras over $Q$ ). The category $cdga_{Q}^{\geq 0}$ of commutative differential graded $Q$ -algebras in non-negative degrees, with weak equivalences quasi-isomorphisms and fibrations degree-wise surjections in positive degree, is a simplicial model category. The simplicial enrichment uses the Sullivan polynomial-differential-form algebra: $\mathrm{Map}{\mathbf{cdga}}(A, B)n = \mathrm{Hom}{\mathbf{cdga}}(A, B \otimes \Omega{\mathrm{poly}}^(\Delta^n)) $, w h er e$ \Omega_{\mathrm{poly}}^(\Delta^n) $i s t h e p o l y n o mia l - f or ma l g e b r a o f t h es t an d a r d$ n$-simplex.

The Bousfield-Gugenheim simplicial model structure is the foundation of rational homotopy theory: Sullivan's minimal models compute the rational homotopy type of a space through the cofibrant replacement in this model category, and the function complexes $Map_{cdga} (A, B)$ compute the rational mapping spaces. The framework is Quillen-equivalent to the rationalisation of simply-connected spaces (Quillen 1969, Sullivan 1977).

Theorem (Hovey 1999 §5.4, Dold-Kan transports the simplicial structure to chain complexes). Under the Dold-Kan correspondence $N : sAb \to Ch_{\geq 0} (Z)$ , the simplicial-model-category structure on simplicial abelian groups transports to a simplicial-model-category structure on non-negatively graded chain complexes. The simplicial enrichment is $Map_{Ch} (C, D)_{n} = Hom_{Ch} (C, D \otimes N Z [Δ^{n}])$ , where $N Z [Δ^{n}]$ is the normalised chain complex of the standard simplex.

This is the technical foundation for the dg-categorical approach to derived categories: a dg-category is a category enriched over chain complexes (a dg-enrichment), and the Dold-Kan correspondence converts a dg-enrichment into a simplicial enrichment. Every dg-category therefore presents a simplicial $(\infty, 1)$ -category, and the equivalence between dg-categories and simplicial categories at the level of $(\infty, 1)$ -categorical homotopy theory is the foundational result of Toën's DG categories and derived Morita theory (Toën 2007).

Quillen equivalences and the homotopy-coherent diagram framework

Theorem (Quillen 1967 §II.2.7, simplicial Quillen equivalence). A Quillen adjunction $F ⊣ G : D \to C$ between simplicial model categories is simplicial if it lifts to a $sSet$ -enriched adjunction, i.e. if the natural isomorphism $Hom_{D} (F X, Y) ≅ Hom_{C} (X, G Y)$ enriches to a natural isomorphism $Map_{D} (F X, Y) ≅ Map_{C} (X, G Y)$ of simplicial sets. A simplicial Quillen adjunction is a simplicial Quillen equivalence if the derived adjunction $L F ⊣ R G : Ho (D) \to Ho (C)$ is an equivalence of categories — equivalently, if the natural map on derived function complexes is a weak equivalence for every cofibrant $X$ and fibrant $Y$ .

Simplicial Quillen equivalences are the right notion of equivalence for simplicial model categories: they preserve not only the bare homotopy category but also the entire $(\infty, 1)$ -categorical structure encoded in the function complexes. The geometric-realisation / singular-complex adjunction $∣ - ∣ ⊣ Sing : Top \to sSet$ is a simplicial Quillen equivalence, as is the Dold-Kan correspondence between simplicial abelian groups and non-negatively graded chain complexes (Hovey 1999 Theorem 4.2.5).

Theorem (Riehl 2014 §10, homotopy-coherent diagrams). Let $C$ be a simplicial model category, $I$ a small simplicial category. A homotopy-coherent diagram of shape $I$ in $C$ is a simplicial functor $I \to C$ . The category $Fun^{h c} (I, C)$ of homotopy-coherent diagrams carries a projective model structure (weak equivalences and fibrations defined object-wise) and an injective model structure (weak equivalences and cofibrations defined object-wise), each of which is a simplicial model category. The derived function complexes of the projective and injective structures coincide and compute the $(\infty, 1)$ -categorical functor category $Fun_{\infty} (I, C)$ .

This framework is what makes the simplicial-model-category approach a viable model of $(\infty, 1)$ -category theory: diagrams in the $(\infty, 1)$ -categorical sense (functors that preserve composition only up to homotopy of higher and higher orders) are exactly the simplicial functors out of a simplicial-category model of the diagram shape. The homotopy-coherent framework is the right setting for derived limits, derived colimits, and the entire $(\infty, 1)$ -categorical functor calculus.

Theorem (Lurie 2009 §A.3, simplicial model categories present $(\infty, 1)$ -categories). The homotopy-coherent nerve construction $N^{h c}$ assigns to every fibrant simplicial category a quasi-category (an $(\infty, 1)$ -category in the Joyal sense). When restricted to the simplicial categories arising as cofibrant-fibrant subcategories of simplicial model categories, the construction is an equivalence on $(\infty, 1)$ -categories: every $(\infty, 1)$ -category presented by a simplicial model category is equivalent to one presented by its homotopy-coherent nerve, and the equivalence is a Quillen equivalence between the model category $sCat$ of simplicial categories (Bergner 2007) and the Joyal model category $sSet_{Joyal}$ of simplicial sets with the Joyal model structure.

The Bergner-Joyal Quillen equivalence is one of several presentations of the underlying $(\infty, 1)$ -categorical theory (others include complete Segal spaces, Segal categories, and the Boardman-Vogt model). The simplicial-model-category framework, via the homotopy-coherent nerve, is therefore one of the equivalent presentations, with the advantage that it admits the most concrete computational tools (cofibrant replacement, fibrant replacement, lifting arguments, function complexes computed by SM7).

Synthesis. The simplicial-model-category framework is the foundational reason that abstract homotopy theory can be unified at the level of $(\infty, 1)$ -categories rather than only at the bare $Ho (C)$ level. The central insight is that the simplicial enrichment promotes every Hom set to a Kan complex of higher coherences via the SM7 pushout-product axiom, so that the entire $(\infty, 1)$ -categorical functor calculus, derived limits and colimits, and homotopy-coherent diagram framework all become accessible through standard model-category machinery. Putting these together with the SM6 tensor-cotensor adjunction, every classical homotopy-theoretic construction lifts from the homotopy category to the simplicial-model-category level: the suspension $Σ X = S^{1} \otimes X$ is well-defined on cofibrant objects, the loop space $Ω X = X^{S^{1}}$ on fibrant objects, and the homotopy fibre and homotopy cofibre constructions assemble from pullbacks and pushouts in $C$ refined by the simplicial enrichment.

This pattern recurs in every modern algebraic-topology development: the foundational reason is that the SM7 axiom is the precise compatibility between simplicial enrichment and model structure, the bridge is between the bare homotopy-class set $[X, Y] = π_{0} RMap (X, Y)$ and the entire derived mapping space, and the construction generalises beyond the simplicial case to enrichment over any nice monoidal model category (Hovey 1999). This is exactly the structure that identifies the simplicial-model-category presentation of an $(\infty, 1)$ -category with the quasi-categorical presentation: the homotopy-coherent nerve transports between them, and the resulting Quillen equivalence between $sCat$ and $sSet_{Joyal}$ is the foundational compatibility theorem. The pattern is dual to the cotensor-side formulation in Hirschhorn 2003 §9.1 via the pullback-power axiom: pushout-products on cofibrations / monomorphisms are equivalent to pullback-powers on fibrations / monomorphisms by the SM6 adjunction, so the SM7 axiom can be stated in either direction. Every homotopy-coherent diagram, every derived functor, every Quillen-equivalence transport — all flow from this single five-axiom enrichment.

Full proof set [Master]

Proposition (SM7 acyclic-cofibration consequence). In a simplicial model category, if $i : A \to B$ is an acyclic cofibration in $C$ and $j : K \to L$ is any monomorphism in $sSet$ , the pushout-product $i □ j$ is an acyclic cofibration in $C$ .

Proof. The pushout-product $i □ j$ is a cofibration by SM7 (with $i$ a cofibration and $j$ a monomorphism). For acyclicity, factor $i □ j$ through its source and target of the pushout square: $$ (A \otimes L) \sqcup_{A \otimes K} (B \otimes K) \xrightarrow{i \square j} B \otimes L. $$ Consider the diagram $$ \begin{array}{ccc} A \otimes K & \xrightarrow{i \otimes \mathrm{id}_K} & B \otimes K \ \downarrow \mathrm{id}_A \otimes j & & \downarrow \mathrm{id}_B \otimes j \ A \otimes L & \xrightarrow{i \otimes \mathrm{id}_L} & B \otimes L \end{array} $$ which is a commutative square in $C$ . The two horizontal arrows $i \otimes id_{K}$ and $i \otimes id_{L}$ are acyclic cofibrations by SM7 (apply SM7 with $i$ acyclic and $j = \emptyset \to K$ or $j = \emptyset \to L$ , both monomorphisms when $K, L$ are non-empty). The induced map on the pushout, which is $i □ j$ , is therefore an acyclic cofibration by the 2-out-of-3 property of weak equivalences (M1) applied to the diagonal of the square.

More carefully: the pushout-product factorisation reads $i □ j : (A \otimes L) ⊔_{A \otimes K} (B \otimes K) \to B \otimes L$ , and $(A \otimes L) ⊔_{A \otimes K} (B \otimes K)$ receives a map from $A \otimes L$ which is part of an acyclic cofibration $A \otimes L \to B \otimes L$ (factor through the pushout). The composition $A \otimes L \to (A \otimes L) ⊔_{A \otimes K} (B \otimes K) \to B \otimes L$ equals $i \otimes id_{L}$ , an acyclic cofibration; the first map is the canonical pushout inclusion, hence a cofibration. By M1, $i □ j$ is a weak equivalence. $□$

Proposition (Map preserves weak equivalences in the cofibrant variable). Let $C$ be a simplicial model category, $f : X^{'} \to X$ a weak equivalence between cofibrant objects, $Y$ a fibrant object. The induced morphism $f^ : \mathrm{Map}\mathcal{C}(X, Y) \to \mathrm{Map}\mathcal{C}(X', Y)$ is a weak equivalence of Kan complexes.*

Proof. By the headline theorem (Quillen 1967 §II.2), both $Map_{C} (X, Y)$ and $Map_{C} (X^{'}, Y)$ are Kan complexes. We show $f^{*}$ is a Kan weak equivalence by Ken Brown's lemma applied to the functor $F = Map_{C} (-, Y)^{op} : C \to sSet$ .

We need to check that $F$ sends acyclic cofibrations between cofibrant objects to weak equivalences of Kan complexes. Let $g : A \to B$ be an acyclic cofibration between cofibrant objects in $C$ . Consider the lifting problem for the function-complex map $g^{*} : Map_{C} (B, Y) \to Map_{C} (A, Y)$ . A horn-filling square in the function complex is, by SM6, a lifting square $$ \begin{array}{ccc} A \otimes \Delta^n \sqcup_{A \otimes \Lambda^n_k} B \otimes \Lambda^n_k & \xrightarrow{} & Y \ \downarrow g \square \iota & & \ B \otimes \Delta^n & \xrightarrow{} & * \end{array} $$ where $ι : Λ_{k}^{n} \to Δ^{n}$ is the horn inclusion. By SM7 with $g$ acyclic, $g □ ι$ is an acyclic cofibration. Since $Y \to *$ is a fibration, the lift exists by M3. Hence $g^{*}$ is a Kan fibration with the right lifting property against every horn inclusion at every dimension — every simplicial map $Δ^{n} \to Map_{C} (A, Y)$ lifts to $Δ^{n} \to Map_{C} (B, Y)$ given a compatible lift on the horn. In particular, $g^{*}$ is an acyclic Kan fibration, hence a weak equivalence of Kan complexes.

Ken Brown's lemma now gives: $F$ sends every weak equivalence between cofibrant objects to a weak equivalence in $sSet$ . In particular, $f^{*} = F (f)$ is a weak equivalence. $□$

Proposition (Map preserves weak equivalences in the fibrant variable). Let $C$ be a simplicial model category, $X$ a cofibrant object, $g : Y \to Y^{'}$ a weak equivalence between fibrant objects. The induced morphism $g_ : \mathrm{Map}\mathcal{C}(X, Y) \to \mathrm{Map}\mathcal{C}(X, Y')$ is a weak equivalence of Kan complexes.*

Proof. Symmetric to the previous proposition, using the SM7 dual on the cotensor side (or equivalently, the same proof with the SM6 adjunctions running the other way). The functor $G = Map_{C} (X, -) : C \to sSet$ sends acyclic fibrations between fibrant objects to acyclic Kan fibrations by the pullback-power form of SM7; Ken Brown's lemma applied to the opposite category gives the result. $□$

Proposition (cofibrations induce Kan fibrations on function complexes). Let $C$ be a simplicial model category, $i : A \to B$ a cofibration between cofibrant objects, $Y$ a fibrant object. The induced morphism $i^ : \mathrm{Map}\mathcal{C}(B, Y) \to \mathrm{Map}\mathcal{C}(A, Y) $i s a K an f ib r a t i o n o f s im pl i c ia l se t s, an d i s m or eo v er a cy c l i c w h e n e v er$ i$ is acyclic.*

Proof. We check the right lifting property against horn inclusions. A horn $Λ_{k}^{n} \to Map_{C} (B, Y)$ together with an extension $Δ^{n} \to Map_{C} (A, Y)$ of the horn's image under $i^{*}$ corresponds by SM6 to a lifting square $$ \begin{array}{ccc} A \otimes \Delta^n \sqcup_{A \otimes \Lambda^n_k} B \otimes \Lambda^n_k & \xrightarrow{} & Y \ \downarrow i \square \iota & & \downarrow p \ B \otimes \Delta^n & \xrightarrow{} & * \end{array} $$ where $ι : Λ_{k}^{n} ↪ Δ^{n}$ is the horn inclusion and $p : Y \to *$ is the fibration $Y$ is fibrant. The left morphism is the pushout-product $i □ ι$ of the cofibration $i$ with the acyclic monomorphism $ι$ ; by SM7 (acyclic case), $i □ ι$ is an acyclic cofibration in $C$ . By M3, the lift exists.

The lift corresponds under SM6 to a simplicial map $Δ^{n} \to Map_{C} (B, Y)$ filling the horn and projecting to the given extension on $Map_{C} (A, Y)$ . This is the horn-lift, exhibiting $i^{*}$ as a Kan fibration. The acyclic case follows from the proposition above. $□$

Proposition (the function complex computes derived $Hom$ ). Let $C$ be a simplicial model category, $X, Y \in C$ arbitrary objects. The set $π_{0} RMap (X, Y)$ of connected components of the derived function complex is naturally isomorphic to $Hom_{Ho (C)} (X, Y)$ .

Proof. By definition $RMap (X, Y) = Map_{C} (QX, R Y)$ , where $Q$ is cofibrant replacement and $R$ is fibrant replacement. Since $QX$ is cofibrant and $R Y$ is fibrant, $Map_{C} (QX, R Y)$ is a Kan complex (Quillen's theorem). Its $π_{0}$ is the set of $0$ -simplices modulo the equivalence relation generated by $1$ -simplices: that is, $Hom_{C} (QX, R Y)$ modulo simplicial homotopy.

A simplicial homotopy in $Map_{C} (QX, R Y)$ between two $0$ -simplices $f, g : QX \to R Y$ is a $1$ -simplex of $Map_{C} (QX, R Y)$ , which by SM6 is a simplicial map $Δ^{1} \to Map_{C} (QX, R Y)$ , which by SM6 again is a morphism $Δ^{1} \otimes QX \to R Y$ in $C$ . The object $Δ^{1} \otimes QX$ is a cylinder object for $QX$ in the sense of the model category $C$ , since $Δ^{1}$ is a simplicial cylinder for $Δ^{0}$ . Hence simplicial-homotopy in the function complex coincides with left-homotopy in $C$ .

By Quillen's homotopy-category theorem (Quillen 1967 §I.5, Quillen 2010 Homotopical Algebra Theorem I.5.1), morphisms in $Ho (C)$ from $X$ to $Y$ are in bijection with $Hom_{C} (QX, R Y)$ modulo left-homotopy. Combining: $π_{0} RMap (X, Y) = Hom_{C} (QX, R Y) / simplicialhomotopy = Hom_{C} (QX, R Y) / lefthomotopy = Hom_{Ho (C)} (X, Y)$ . $□$

The full development, with all functoriality bookkeeping and the verification that the derived function complex is well-defined independently of the choice of replacements, occupies Hirschhorn 2003 §9.3 (pp. 178-184) and Hovey 1999 §5.4 (pp. 121-128). The technical content lies in showing that the simplicial enrichment is compatible with the cofibrant-fibrant replacement functors, which requires the M4 factorisation to be functorial (a hypothesis automatic in the modern Hovey-Hirschhorn axiomatisation but added by hand in Quillen's original).

Connections [Master]

Quillen model category 03.12.31. The simplicial-model-category framework of the present unit is the simplicial-enriched refinement of the bare model-category framework of 03.12.31. Where 03.12.31 axiomatises the three classes $W, F, C$ and derives the homotopy category $Ho (C)$ , the present unit adds the simplicial enrichment $Map (-, -)$ and the SM7 compatibility axiom, upgrading $Hom_{Ho (C)} (X, Y)$ from a bare set to a Kan complex carrying higher-coherence data. The two units are a foundation pair: 03.12.31 axiomatises the homotopy category at the $π_{0}$ level, the present unit axiomatises the entire derived mapping space.
Simplicial sets and geometric realization 03.12.25. The prototypical simplicial model category is $sSet$ itself with the Kan-Quillen model structure. The internal Hom $L^{K}$ on simplicial sets is the simplicial enrichment, the cartesian product is the tensor, the headline theorem specialises to: $K^{L}$ is a Kan complex when $L$ is arbitrary and $K$ is a Kan complex. The geometric-realisation / singular-complex adjunction $∣ - ∣ ⊣ Sing$ becomes a simplicial Quillen equivalence in the present framework, connecting the simplicial-enrichment side to the topological-enrichment side.
Kan-Quillen model structure on sSet 03.12.33. The Kan-Quillen structure is the canonical worked example of the simplicial-model-category framework: $sSet$ enriched over itself via the internal Hom $L^{K}$ satisfies SM0, SM6, SM7, and the headline Kan-complex theorem specialises to the statement that $Map (L, K) = K^{L}$ is a Kan complex whenever $K$ is. Every other example of a simplicial model category — simplicial groups, dg-algebras over $Q$ via Bousfield-Gugenheim, symmetric spectra — is verified by checking SM7 against the Kan-Quillen structure on $sSet$ acting via tensor / power, so the foundational reason the present unit's framework computes derived mapping spaces correctly is that 03.12.33 supplies the prototype.
Quillen functor and equivalence 03.12.32. The simplicial-Quillen-equivalence machinery of the present unit refines the bare Quillen-equivalence machinery of 03.12.32. A simplicial Quillen adjunction $F ⊣ G$ between simplicial model categories enriches the derived adjunction $L F ⊣ R G$ to a simplicial adjunction between derived function complexes, so that a simplicial Quillen equivalence preserves the entire $(\infty, 1)$ -categorical structure, not just the bare homotopy category. The Dold-Kan correspondence, the geometric-realisation adjunction, and the Bousfield-Gugenheim simplicial structure on cdga's are all simplicial Quillen equivalences.
Eilenberg-MacLane spaces 03.12.05. The simplicial model structure on simplicial abelian groups (transported from chain complexes via Dold-Kan) provides explicit simplicial models for Eilenberg-MacLane spaces $K (π, n)$ : the chain complex $π [n]$ concentrated in degree $n$ corresponds under Dold-Kan to a simplicial abelian group whose realisation is $K (π, n)$ . The function complexes $Map (X, K (π, n))$ compute the cohomology $H^{n} (X; π)$ as the set $π_{0}$ and the higher cohomology operations as the higher $π_{*}$ via the simplicial-set generalisation of the cohomology-as-homotopy-classes formula.
Sullivan minimal models 03.12.06. The Bousfield-Gugenheim simplicial model structure on commutative dg-algebras over $Q$ provides the simplicial model category in which Sullivan minimal models live. The Sullivan minimal model of a space is its cofibrant replacement in the dg-algebra category, and the function complex $Map_{cdga} (M_{X}, M_{Y})$ computes the rational mapping space $Map (X, Y)_{Q}$ between simply-connected rational spaces. The framework recasts rational-homotopy computations as simplicial-Hom computations in a tractable algebraic model category.
CW complex 03.12.10. The simplicial-model-category framework provides a clean conceptual home for CW approximation: every space has a cofibrant replacement that is a CW complex (in the Quillen-Serre / Hurewicz-Strom hybrid framework), and the simplicial enrichment provides not just the set of homotopy classes $[X, Y]$ but the entire Kan complex $Map (QX, Y)$ whose $π_{n}$ 's record the higher homotopy structure. The Whitehead theorem becomes the special case: weak equivalence of CW pairs lifts to homotopy equivalence because the function complex is contractible at $π_{0}$ and beyond.
Spectrum 03.12.04. The category $Sp^{Σ}$ of symmetric spectra (Hovey-Shipley-Smith 2000) is a simplicial model category in which the simplicial enrichment underpins the stable mapping spaces. The function complex $Map_{Sp^{Σ}} (X, Y)$ computes the stable mapping spectrum $[X, Y]_{Sp}$ at the level of all $π_{n}$ , not just $π_{0}$ , and the SM7 axiom in this case implements the smash-product compatibility with the stable model structure. The framework is the foundation of the modern presentation of stable homotopy theory as the $(\infty, 1)$ -category of spectra.

Historical & philosophical context [Master]

Daniel Quillen introduced the simplicial-model-category framework in 1967 in his Lecture Notes in Mathematics monograph Homotopical Algebra (Springer LNM 43) ^{[Quillen 1967]}, §II.1-§II.2, alongside the more general model-category framework of §I. The motivation was to upgrade the bare model-category axiomatisation so that the homotopy theory of simplicial sets — where the simplicial structure is fundamental — could be treated with the same axiomatic machinery as the homotopy theory of topological spaces and chain complexes. Quillen identified the three additional axioms SM0, SM6, SM7 needed to ensure the simplicial enrichment is compatible with the model structure, and proved the headline theorem: in a simplicial model category, the function complex $Map (X, Y)$ is a Kan complex when $X$ is cofibrant and $Y$ is fibrant. The 1967 monograph also proved that $sSet$ with the Kan-Quillen model structure is the prototypical simplicial model category, and that simplicial groups, simplicial commutative rings, and chain complexes via Dold-Kan all carry simplicial model structures.

The framework was developed further by Paul Goerss and Rick Jardine in their 1999 monograph Simplicial Homotopy Theory (Birkhäuser) ^{[Goerss-Jardine 2009]}, whose §II.2-§II.3 gave the canonical modern exposition of function complexes and their homotopy groups. Philip Hirschhorn's 2003 Model Categories and Their Localizations ^{[Hirschhorn 2003]} developed the SM7 axiom in its modern pushout-product form, with the dual pullback-power formulation as the primary statement; his §9 remains the most thorough single reference. Mark Hovey's 1999 Model Categories (AMS Mathematical Surveys 63) ^{[Hovey 1999]} generalised the framework to monoidal model categories, showing that simplicial enrichment is one instance of a much more general structure (enrichment over any nice symmetric monoidal model category).

The conceptual extension to $(\infty, 1)$ -category theory was carried out by André Joyal and Jacob Lurie in the early 2000s. Joyal's 2002 paper on quasi-categories ^{[Joyal 2002]} introduced the simplicial-set model of $(\infty, 1)$ -categories satisfying inner-horn-extension conditions, and Lurie's 2009 Higher Topos Theory ^{[Lurie 2009]} gave the modern unified treatment. Section A.3 of Lurie's monograph proves the foundational theorem: every simplicial model category, restricted to its cofibrant-fibrant objects, presents an $(\infty, 1)$ -category via the homotopy-coherent nerve, and the resulting Quillen equivalence between $sCat$ (simplicial categories, Bergner 2007 ^{[Bergner 2007]}) and $sSet_{Joyal}$ (Joyal model structure on simplicial sets) makes the two presentations interchangeable.

The applications of simplicial-model-category theory in the decades since Quillen's monograph extend across rational homotopy theory (Sullivan 1977 / Bousfield-Gugenheim 1976, where the simplicial structure on cdga's encodes rational homotopy types), motivic homotopy theory (Morel-Voevodsky 1999, where the $A^{1}$ -model structure on simplicial presheaves on smooth schemes is a simplicial model category), derived algebraic geometry (Toën-Vezzosi 2008, Lurie 2009-), stable homotopy theory via symmetric spectra (Hovey-Shipley-Smith 2000), and the entire formal framework of $(\infty, 1)$ -categorical mathematics. The framework's longevity comes from its combination of axiomatic minimalism — three axioms beyond the basic model structure — and computational power: once SM0, SM6, SM7 are verified for a category, the entire derived mapping-space calculus and homotopy-coherent diagram framework is automatic.

The Dwyer-Kan 1980 Function complexes in homotopical algebra ^{[Dwyer-Kan 1980]} provides the philosophical bridge between the simplicial-model-category presentation and the abstract notion of an $(\infty, 1)$ -category: the simplicial-model-category function complex agrees with the simplicial localisation $L^{H} C$ of the underlying model category, so the simplicial enrichment is genuinely a presentation of the abstract $(\infty, 1)$ -categorical structure, not an extra piece of data. This is the conceptual content of the framework: a simplicial model category is one of several equivalent ways of presenting an $(\infty, 1)$ -category, and the SM7 axiom is the precise compatibility condition needed for the presentation to be honest.

Bibliography [Master]

@book{Quillen1967,
  author    = {Quillen, Daniel G.},
  title     = {Homotopical Algebra},
  series    = {Lecture Notes in Mathematics},
  volume    = {43},
  publisher = {Springer-Verlag},
  year      = {1967}
}

@book{GoerssJardine2009,
  author    = {Goerss, Paul G. and Jardine, John F.},
  title     = {Simplicial Homotopy Theory},
  series    = {Modern Birkh{\"a}user Classics},
  publisher = {Birkh{\"a}user},
  year      = {2009},
  note      = {Reprint of 1999 edition}
}

@book{Hirschhorn2003,
  author    = {Hirschhorn, Philip S.},
  title     = {Model Categories and Their Localizations},
  series    = {Mathematical Surveys and Monographs},
  volume    = {99},
  publisher = {American Mathematical Society},
  year      = {2003}
}

@book{Hovey1999,
  author    = {Hovey, Mark},
  title     = {Model Categories},
  series    = {Mathematical Surveys and Monographs},
  volume    = {63},
  publisher = {American Mathematical Society},
  year      = {1999}
}

@article{DwyerKan1980,
  author    = {Dwyer, William G. and Kan, Daniel M.},
  title     = {Function complexes in homotopical algebra},
  journal   = {Topology},
  volume    = {19},
  year      = {1980},
  pages     = {427--440}
}

@article{Kan1958,
  author    = {Kan, Daniel M.},
  title     = {Adjoint functors},
  journal   = {Transactions of the American Mathematical Society},
  volume    = {87},
  year      = {1958},
  pages     = {294--329}
}

@article{Joyal2002,
  author    = {Joyal, Andr{\'e}},
  title     = {Quasi-categories and {K}an complexes},
  journal   = {Journal of Pure and Applied Algebra},
  volume    = {175},
  year      = {2002},
  pages     = {207--222}
}

@book{Lurie2009,
  author    = {Lurie, Jacob},
  title     = {Higher Topos Theory},
  series    = {Annals of Mathematics Studies},
  volume    = {170},
  publisher = {Princeton University Press},
  year      = {2009}
}

@article{Bergner2007,
  author    = {Bergner, Julia E.},
  title     = {A model category structure on the category of simplicial categories},
  journal   = {Transactions of the American Mathematical Society},
  volume    = {359},
  year      = {2007},
  pages     = {2043--2058}
}

@book{Riehl2014,
  author    = {Riehl, Emily},
  title     = {Categorical Homotopy Theory},
  series    = {New Mathematical Monographs},
  volume    = {24},
  publisher = {Cambridge University Press},
  year      = {2014}
}

@article{BousfieldGugenheim1976,
  author    = {Bousfield, Aldridge K. and Gugenheim, Victor K. A. M.},
  title     = {On {PL} de {R}ham theory and rational homotopy type},
  journal   = {Memoirs of the American Mathematical Society},
  volume    = {179},
  year      = {1976}
}

@article{HoveyShipleySmith2000,
  author    = {Hovey, Mark and Shipley, Brooke and Smith, Jeff},
  title     = {Symmetric spectra},
  journal   = {Journal of the American Mathematical Society},
  volume    = {13},
  year      = {2000},
  pages     = {149--208}
}

@article{Milnor1957,
  author    = {Milnor, John W.},
  title     = {The geometric realization of a semi-simplicial complex},
  journal   = {Annals of Mathematics},
  volume    = {65},
  year      = {1957},
  pages     = {357--362}
}

@incollection{DwyerSpalinski1995,
  author    = {Dwyer, William G. and Spalinski, Jan},
  title     = {Homotopy theories and model categories},
  booktitle = {Handbook of Algebraic Topology},
  editor    = {James, I. M.},
  publisher = {Elsevier},
  year      = {1995},
  pages     = {73--126}
}

Prerequisites

03.12.25
03.12.31

Tier anchors

beginner: Dwyer-Spalinski 1995 *Homotopy theories and model categories* §3-§4 informal opening; Friedman's expository pictures of simplicial mapping spaces
intermediate: Quillen 1967 *Homotopical Algebra* (Springer LNM 43) §II.1-§II.2; Goerss-Jardine 2009 *Simplicial Homotopy Theory* §II.2; Hovey 1999 *Model Categories* §4.2
master: Quillen 1967 *Homotopical Algebra* (Springer LNM 43) §II.1-§II.3 (originator of simplicial model categories and the SM7 axiom); Goerss-Jardine 2009 *Simplicial Homotopy Theory* §II.2-§II.3 (function complexes and the Kan-complex theorem); Hirschhorn 2003 *Model Categories and Their Localizations* §9.1-§9.4 (modern treatment with cofibrantly generated machinery); Hovey 1999 *Model Categories* §4.2-§4.3 (monoidal-model-category framework subsuming simplicial enrichment); Riehl 2014 *Categorical Homotopy Theory* §10 (homotopy-coherent diagrams via simplicial enrichment); Lurie 2009 *Higher Topos Theory* §A.3 (relation to $(\infty, 1)$-categories)

References

TODO_REF
Quillen — Homotopical Algebra · Springer Lecture Notes in Mathematics 43 (1967); originator paper, §II.1 simplicial categories and enrichment, §II.2 axioms SM0, SM6, SM7 for simplicial model categories, §II.2 Proposition 3 (function complex is a Kan complex), §II.3 the Kan-Quillen model structure on sSet as the prototypical simplicial model category
TODO_REF
Goerss-Jardine — Simplicial Homotopy Theory · Birkhäuser Progress in Mathematics 174 (1999, reprint 2009); §II.2 function complexes Map(X, Y) as Kan complexes computed from fibrant-cofibrant replacements; §II.3 homotopy groups of function complexes; §IX simplicial groups as a simplicial model category
TODO_REF
Hirschhorn — Model Categories and Their Localizations · AMS Mathematical Surveys and Monographs 99 (2003); §9.1 simplicial-model-category axioms in the modern formulation, §9.2 the pushout-product axiom and its consequences, §9.3 properties of function complexes, §9.4 simplicial Quillen functors
TODO_REF
Hovey — Model Categories · AMS Mathematical Surveys and Monographs 63 (1999); §4.2 monoidal model categories subsuming the simplicial case via the pushout-product axiom, §4.3 the unit axiom, §5.6 closed symmetric monoidal model categories
TODO_REF
Kan — Adjoint functors · Trans. Amer. Math. Soc. 87 (1958) 294-329; the original source for the adjoint-functor formalism that underpins the tensor-cotensor enrichment in simplicial model categories
TODO_REF
Dwyer-Kan — Function complexes in homotopical algebra · Topology 19 (1980) 427-440; the simplicial-localisation construction giving function complexes for an arbitrary category with weak equivalences, agreeing with the simplicial-model-category function complex when both are available
TODO_REF
Riehl — Categorical Homotopy Theory · Cambridge New Mathematical Monographs 24 (2014); §10 enriched homotopy theory and homotopy-coherent diagrams via simplicial enrichment
TODO_REF
Lurie — Higher Topos Theory · Princeton Annals of Mathematics Studies 170 (2009); §A.3.1-A.3.7 simplicial model categories, the relation between simplicial model categories and quasi-categories via the homotopy-coherent nerve
TODO_REF
Bergner — A model category structure on the category of simplicial categories · Trans. Amer. Math. Soc. 359 (2007) 2043-2058; the model structure on simplicial categories used to compare simplicial enrichment with quasi-category enrichment
TODO_REF
May-Ponto — More Concise Algebraic Topology · University of Chicago Press 2012; Ch. 16 on enriched model categories and simplicial mapping spaces

Lean module

Codex.Modern.Homotopy.SimplicialModelCategory

Mathlib gap

Mathlib has the simplex category, simplicial sets, and partial
categorical infrastructure for enriched categories in
`Mathlib.AlgebraicTopology.SimplicialSet.*` and
`Mathlib.CategoryTheory.Enriched.*`, including the cartesian-closed
structure on `Type` and the simplicial-set machinery for `SSet`. What
is currently absent is the `SimplicialModelCategory` type-class
recording the SM0-SM7 axioms, the construction of the function
complex `Map(X, Y) : SSet` as a simplicial Hom in the enriched
category, the pushout-product axiom SM7 as a stated lemma about
cofibrations and monomorphisms in the underlying model category and
the Kan-Quillen model category, the proof that `Map(X, Y)` is a Kan
complex when `X` is cofibrant and `Y` is fibrant (Quillen 1967 §II.2
Proposition 3), the homotopy-coherent diagram framework via
simplicial enrichment, and the verified instances of `SSet`,
simplicial groups, simplicial commutative rings, and chain complexes
via Dold-Kan as simplicial model categories. The Lean module
associated to this unit states the headline theorems (SM7 implies
cofibration of the pushout-product; the function complex is Kan iff
the target is fibrant) with `sorry` proof bodies pending the
upstream API. This is a high-priority formalisation gap for
Mathlib's algebraic-topology library because every modern
presentation of $(\infty, 1)$-categorical homotopy theory factors
through the simplicial-model-category framework.

Reviewer

TBD

Estimated time

beginner: 22m
intermediate: 50m
master: 100m