03.12.37 · modern-geometry / homotopy

Homotopy colimit via the Bousfield-Kan construction

shipped3 tiersLean: partial

Anchor (Master): Bousfield-Kan 1972 *Homotopy Limits, Completions and Localizations* (LNM 304) §X-§XII (originator); Hirschhorn 2003 *Model Categories and Their Localizations* (AMS Mathematical Surveys 99) §18-§19; Riehl 2014 *Categorical Homotopy Theory* §6; Dugger 2008 *A primer on homotopy colimits*; Goerss-Jardine 2009 *Simplicial Homotopy Theory* §IV

Intuition [Beginner]

A homotopy colimit is the correct way to glue together a diagram of spaces when you want the answer to depend only on the homotopy type of each space and each gluing map. The plain colimit (ordinary pushout, ordinary union, ordinary direct limit) does not have this property: if you replace one space in the diagram by another space of the same homotopy type, the plain colimit can change drastically. The homotopy colimit is the corrected construction.

The Bousfield-Kan recipe is the most explicit way to build it. Take your diagram of spaces indexed by a small category. From this data, build a single big simplicial set whose simplices record chains of composable arrows in the indexing category together with a point of the first space in the chain. The geometric realisation of this simplicial set is the homotopy colimit. The recipe was introduced by Bousfield and Kan in 1972 and is the canonical formula.

The reader should hold a single picture. The plain colimit is what you get if you glue the spaces with the bare gluing data and nothing else. The homotopy colimit is what you get if you also insert a small interval, a small triangle, a small tetrahedron and so on, one for every chain of arrows in the indexing category. Those extra cells are the homotopical padding that makes the construction homotopy-invariant.

Visual [Beginner]

Picture a pushout of three spaces: a space $A$ , a space $B$ , and a space $C$ that maps into both. The plain pushout identifies points of $A$ and $B$ that come from the same point of $C$ . The homotopy pushout instead glues $A$ and $B$ to opposite ends of a cylinder $C \times [0, 1]$ over $C$ , so that the maps from $C$ into $A$ and $B$ are pulled apart by the interval. The plain pushout is the homotopy pushout collapsed by squashing the cylinder to a point.

The same picture extends to any diagram. The Bousfield-Kan formula attaches one simplex for every chain of composable arrows in the indexing category, building up the homotopy colimit one dimension at a time. The plain colimit is recovered by squashing every chain to a point; the homotopy colimit keeps the chains as honest geometric cells.

Worked example [Beginner]

Build the homotopy pushout of the diagram $* \leftarrow S^{0} \to *$ , where $S^{0} = {p, q}$ is a two-point space and both arrows are the unique maps to the one-point space.

Step 1. The plain pushout. Both maps send everything to a single point, so the plain pushout collapses $S^{0} ⊔ *$ along the relation identifying everything; the answer is a single point.

Step 2. The homotopy pushout. The Bousfield-Kan formula inserts a copy of $S^{0} \times [0, 1]$ between the two copies of the one-point space. Concretely: glue the two endpoints $S^{0} \times {0}$ to the left copy of $*$ (collapsing them to a single point) and the two endpoints $S^{0} \times {1}$ to the right copy of $*$ (also collapsing them to a single point).

Step 3. The result is two intervals joined at both endpoints. Each interval comes from one point of $S^{0}$ crossed with $[0, 1]$ ; both intervals have their left endpoints identified at the left $*$ and both their right endpoints identified at the right $*$ . The result is a circle $S^{1}$ .

What this tells us: the plain pushout collapsed everything to a point, while the homotopy pushout produced the circle $S^{1}$ . The difference is not a calculation error; it is the whole reason the homotopy pushout exists. The point-set pushout sees only that both arrows hit the same target and identifies things; the homotopy pushout records each gluing as a separate interval and gets a richer space. The result $S^{1}$ has the right homotopy type to detect, for example, the suspension of $S^{0}$ , which is exactly what the homotopy pushout of $* \leftarrow S^{0} \to *$ is supposed to compute.

Check your understanding [Beginner]

Exercise (easy, multiple choice).

Why does the ordinary categorical colimit fail to be a homotopy-invariant construction?

A. The colimit is too small. B. Replacing a space in the diagram by a homotopy-equivalent space can change the colimit drastically. C. The colimit only exists for finite diagrams. D. The colimit always agrees with the homotopy colimit.

Hint

Try a small example: the plain pushout of $* \leftarrow * \to *$ versus the plain pushout of $* \leftarrow pt \times [0, 1] \to *$ .

Answer

B. Replacing a space in the diagram by a homotopy-equivalent space can change the colimit drastically. Feedback-correct: the pushout of $* \leftarrow * \to *$ is a single point, but the pushout of $* \leftarrow I \to *$ (where $I$ is the unit interval, homotopy-equivalent to a point) is also a single point — yet replacing the connecting object by $S^{0}$ gives the pushout a point, while the homotopy pushout gives $S^{1}$ . The plain colimit sees only the strict gluing data, missing the cofibrant-replacement step that the homotopy colimit performs. Feedback-wrong: A and C are confused statements about size and existence; D would mean the homotopy colimit was redundant.

Exercise (easy, true-false).

True or false: the Bousfield-Kan formula expresses the homotopy colimit of a diagram as the geometric realisation of a single simplicial set.

Hint

The bar construction packages the entire diagram into a simplicial set whose $n$ -simplices are chains of $n$ composable arrows in the indexing category together with a point of the first space.

Answer

True. The Bousfield-Kan construction defines a simplicial set called the bar construction, written $B (*, I, X)$ , whose $n$ -simplices are pairs of a chain of $n$ composable morphisms in $I$ and a point of the source space. The homotopy colimit is the geometric realisation of this simplicial set. The whole point of the construction is to package the entire diagram into a single piece of simplicial data whose realisation is the homotopy colimit.

Formal definition [Intermediate+]

Let $I$ be a small category and let $X : I \to sSet$ be a diagram of simplicial sets, equivalently a functor from $I$ to the category $sSet$ of simplicial sets. The Bousfield-Kan construction produces a simplicial set whose realisation is the homotopy colimit of $X$ .

Definition (the bar construction). The bar construction of the diagram $X$ over the constant terminal-valued left coefficient $*$ is the simplicial set $B (*, I, X)$ whose set of $n$ -simplices is $$ B_n(*, I, X) = \coprod_{i_0 \xrightarrow{\alpha_1} i_1 \xrightarrow{\alpha_2} \cdots \xrightarrow{\alpha_n} i_n} X(i_0)_n, $$ the disjoint union indexed over all length- $n$ chains of composable morphisms in $I$ of the set of $n$ -simplices of $X (i_{0})$ . The face maps act by:

$d_{0}$ applies the leftmost morphism $α_{1} : i_{0} \to i_{1}$ to the $X$ -coordinate, shifting it from $X (i_{0})$ to $X (i_{1})$ , and drops $i_{0}$ and $α_{1}$ .
$d_{j}$ for $0 < j < n$ composes the consecutive arrows $α_{j}$ and $α_{j + 1}$ , shortening the chain by one.
$d_{n}$ drops the rightmost object $i_{n}$ and the morphism $α_{n}$ , leaving the $X$ -coordinate unchanged.

The degeneracy $s_{j}$ inserts an identity morphism $id_{i_{j}}$ at position $j$ in the chain, lengthening it by one.

Definition (Bousfield-Kan homotopy colimit). The Bousfield-Kan homotopy colimit of the diagram $X : I \to sSet$ is $$ \operatorname*{hocolim}_I X := |B(*, I, X)|, $$ the geometric realisation of the bar construction. When the diagram is valued in topological spaces $X : I \to Top$ rather than simplicial sets, the same formula applies with $X (i_{0})$ replaced by the singular complex $Sing (X (i_{0}))$ , or alternatively by interpreting the bar construction as a bisimplicial set and taking the diagonal.

Definition (constant-diagram functor and left Kan extension). Let $p : I \to *$ be the unique functor to the terminal category. Pulling back along $p$ gives the constant-diagram functor $p^{*} = c : sSet \to sSet^{I}$ sending a simplicial set $Y$ to the constant diagram $c (Y) (i) = Y$ for every $i$ . Its left adjoint is the ordinary colimit functor $colim_{I} : sSet^{I} \to sSet$ . The Bousfield-Kan homotopy colimit is the left-derived functor $L colim_{I}$ of this ordinary colimit, computed by cofibrant replacement in a model structure on $sSet^{I}$ .

Definition (projective and Reedy model structures on $sSet^{I}$ ). The projective model structure on the diagram category $sSet^{I}$ takes the weak equivalences and fibrations to be the levelwise ones — that is, $X \to Y$ is a weak equivalence (respectively a fibration) iff $X (i) \to Y (i)$ is a weak equivalence (resp. a Kan fibration) in $sSet$ for every $i \in I$ — and lets the cofibrations be determined by the left lifting property. For $I$ a Reedy category — a category with a degree function and a factorisation system splitting morphisms into "raising" and "lowering" parts — there is a third Reedy model structure whose fibrations are detected by matching objects and whose cofibrations are detected by latching objects.

Definition (homotopy left Kan extension). More generally, for a functor $φ : I \to J$ between small categories, the homotopy left Kan extension $L Lan_{φ} : sSet^{I} \to sSet^{J}$ is the left-derived functor of the ordinary left Kan extension along $φ$ , computed via the projective model structures on the diagram categories. The Bousfield-Kan homotopy colimit is the special case $J = *$ , in which $L Lan_{φ} = L colim_{I}$ .

Counterexamples to common slips

The plain colimit and the homotopy colimit agree when the diagram is cofibrant in the projective model structure — for example, when all the maps in the diagram are cofibrations (monomorphisms of simplicial sets) and the diagram has free structure at limit ordinals. For general diagrams they differ, and the difference is precisely the cofibrant-replacement step.
The bar construction is sensitive to whether the indexing category $I$ has identity morphisms. If you drop the identities (treating $I$ as a non-unital category) you get the acyclic bar construction, which has the same realisation up to weak equivalence because the degenerate simplices contribute nothing geometrically.
For $I$ a discrete category (no non-identity morphisms), the bar construction reduces to the disjoint union $⨆_{i} X (i)$ with one $0$ -simplex per object, and the homotopy colimit coincides with the plain coproduct.
The two-sided bar construction $B (W, I, X)$ with a contravariant weight $W : I^{op} \to sSet$ generalises the formula: $B (*, I, X)$ with $W = *$ the constant terminal-valued weight recovers the homotopy colimit, while $B (*, I, *)$ recovers the nerve $N (I)$ , and $B (*, I, X)$ for $X$ valued in pointed simplicial sets recovers the homotopy quotient.

Key theorem with proof [Intermediate+]

Theorem (Bousfield-Kan 1972, the formula and its homotopy invariance). Let $I$ be a small category and let $X, Y : I \to sSet$ be diagrams of simplicial sets together with a natural transformation $f : X \to Y$ that is levelwise a weak equivalence (i.e. $f_{i} : X (i) \to Y (i)$ is a weak equivalence in $sSet$ for every $i \in I$ ). Then the induced map on bar constructions $$ B(, I, f) : B(, I, X) \to B(, I, Y) $$ is a weak equivalence in $sSet$ . Consequently, the geometric realisation $|B(, I, X)|$ depends only on the levelwise homotopy type of the diagram, and the Bousfield-Kan formula gives a well-defined functor on the homotopy category of diagrams.

Proof. The proof has three steps: identify $B (*, I, X)$ as the diagonal of a bisimplicial set, apply the diagonal-versus-realisation theorem, and use the levelwise weak equivalence to conclude.

Step 1. The bar construction is a bisimplicial set. Write $B (*, I, X)$ as a bisimplicial set $B_{∙, ∙}$ where $B_{p, q}$ is the set of pairs $(σ, x)$ with $σ$ a length- $p$ chain in $I$ starting at some object $i_{0}$ and $x \in X (i_{0})_{q}$ a $q$ -simplex. The horizontal direction (varying $p$ ) records chains in $I$ ; the vertical direction (varying $q$ ) records simplicial data inside the spaces. Face / degeneracy maps in $p$ act on chains as in the formula; face / degeneracy maps in $q$ act simplicially on $x$ inside $X (i_{0})$ .

The simplicial set $B (*, I, X)$ as defined above is the diagonal of this bisimplicial set: $B_{n} (*, I, X) = B_{n, n}$ . Equivalently, $∣ B (*, I, X) ∣$ is the realisation of the bisimplicial set in the sense of Quillen 1973 — the realisation can be computed by first realising in one direction and then the other, both directions giving the same answer because realisation commutes with itself.

Step 2. Diagonal preserves levelwise weak equivalences. Let $f : X \to Y$ be levelwise a weak equivalence. The induced map $B_{p, ∙} (*, I, f) : B_{p, ∙} (*, I, X) \to B_{p, ∙} (*, I, Y)$ on horizontal $p$ -rows is, for each fixed length- $p$ chain $σ$ starting at $i_{0}$ , the map $f_{i_{0}} : X (i_{0}) \to Y (i_{0})$ (a weak equivalence in $sSet$ by hypothesis). Disjoint unions of weak equivalences are weak equivalences, so each row is a weak equivalence.

By the diagonal-versus-realisation theorem (Bousfield-Friedlander 1978; Goerss-Jardine 2009 §IV.1.7): if a map $f : A_{∙, ∙} \to B_{∙, ∙}$ of bisimplicial sets is a row-wise weak equivalence, then the induced map of diagonals $diag (f) : diag (A) \to diag (B)$ is a weak equivalence in $sSet$ .

Step 3. Conclude. Apply Step 2 to the bisimplicial map $B (*, I, f) : B (*, I, X) \to B (*, I, Y)$ : rows are weak equivalences by Step 2, so the diagonal — which equals the bar construction by Step 1 — is a weak equivalence. Realising both sides preserves weak equivalences (realisation is a left Quillen functor), so $∣ B (*, I, X) ∣ \to ∣ B (*, I, Y) ∣$ is a weak equivalence in $Top$ . This is exactly the homotopy invariance of the Bousfield-Kan formula. $□$

Bridge. This theorem builds toward 03.12.31 (Quillen model category) where the homotopy colimit is reframed as a left-derived functor of the constant-diagram-pullback adjunction $colim ⊣ c$ on the projective model structure of $sSet^{I}$ ; the explicit bar-construction formula then identifies the derived functor with a concrete simplicial-set construction. The foundational reason it works is that the bar construction is a cofibrant replacement of the diagram $X$ in the projective model structure on $sSet^{I}$ : applied to a cofibrant diagram, the plain colimit and the homotopy colimit agree, and the Bousfield-Kan formula is the universal cofibrant replacement giving a uniform answer. This is exactly the structure that identifies the Bousfield-Kan formula with the abstract derived functor, and the bridge is between an explicit point-set construction with face / degeneracy formulas and the model-categorical universal property of left derivation. The central insight is that the bar construction encodes the homotopical bookkeeping needed to convert any diagram into a cofibrant one, putting the levelwise replacement and the chain-of-arrows simplicial expansion into a single object. Putting these together, every concrete homotopy-colimit computation — pushouts as double mapping cylinders, sequential colimits as mapping telescopes, classifying spaces as nerves — fits the master template of "build the bar construction, realise it." This pattern recurs in 03.12.25 (simplicial sets and geometric realisation) where the bar construction is the universal example of a simplicial set arising from a diagram, and generalises to weighted colimits via the two-sided bar construction $B (W, I, X)$ .

Exercises [Intermediate+]

Exercise 2 (easy, multiple choice).

Which of the following is the correct Bousfield-Kan formula for the homotopy pushout of a span $A f C g B$ ?

A. $A ⊔ B$ . B. $A ⊔_{C} B$ (the plain pushout). C. $A ⊔_{C} (C \times [0, 1]) ⊔_{C} B$ (the double mapping cylinder). D. $A \times B / C$ (a quotient of the product).

Hint

The homotopy pushout inserts a cylinder between the legs of the span to make the construction homotopy-invariant.

Answer

C. $A ⊔_{C} (C \times [0, 1]) ⊔_{C} B$ (the double mapping cylinder). This is the explicit form of the Bousfield-Kan formula for the pushout shape, with the cylinder $C \times [0, 1]$ playing the role of the cofibrant replacement of the constant $C$ that the plain pushout would use. The plain pushout (B) collapses this cylinder; the answer (A) ignores the gluing entirely; the formula (D) is unrelated.

Exercise 4 (medium, short-answer).

State the Bousfield-Kan formula explicitly for the sequential diagram $X_{0} f_{0} X_{1} f_{1} X_{2} \to \dots$ indexed by the poset $N$ , and identify the resulting homotopy colimit as a familiar topological construction.

Hint

The bar construction on $N$ has $n$ -simplices indexed by chains $i_{0} \leq i_{1} \leq \dots \leq i_{n}$ of natural numbers, together with a simplex of $X_{i_{0}}$ . The non-degenerate part has chains with distinct $i_{j}$ , and the realisation glues the $X_{i}$ along intervals connecting them.

Answer

The bar construction $B (*, N, X)$ has $n$ -simplices $$ B_n(, \mathbb{N}, X) = \coprod_{i_0 \leq i_1 \leq \cdots \leq i_n} X_{i_0, n}. $$ The non-degenerate simplices come from strictly increasing chains $i_{0} < i_{1} < \dots < i_{n}$ . The geometric realisation glues $X_{i_{0}}$ to $X_{i_{1}}$ to $X_{i_{2}}$ and so on along intervals, producing the mapping telescope $$ \mathrm{Tel}(X) = \bigsqcup_{n \geq 0} \bigl( X_n \times [n, n+1] \bigr) \bigg/ \sim, $$ where $(x, n + 1) \in X_{n} \times [n, n + 1]$ is identified with $(f_{n} (x), n + 1) \in X_{n + 1} \times [n + 1, n + 2]$ . The mapping telescope is the homotopy version of the direct limit $\operatorname{colim} X_n $: r e pl a c in g t h es t r i c t i d e n t i f i c a t i o na t e a c h s t a g e b y a cy l in d er mak es t h eco n s t r u c t i o nh o m o t o p y - in v a r ian t . T h e pl ain co l imi t i s t h e q u o t i e n t$ \mathrm{Tel}(X) / \sim $co l l a p s in g e a c h cy l in d er t o i t sr i g h t e n d p o in t; t h e h o m o t o p y co l imi t i s$ \mathrm{Tel}(X)$ itself. Rubric: full credit for the explicit formula and the telescope identification.

Exercise 5 (medium, short-answer).

Show that the homotopy colimit of the constant diagram on the one-point space $* : I \to sSet$ (every object goes to $*$ , every morphism to the identity) is the nerve $N (I)$ of the indexing category.

Hint

The bar construction $B (*, I, *)$ on the constant terminal diagram has $n$ -simplices indexed by chains of $n$ composable morphisms in $I$ — exactly the definition of the nerve.

Answer

For $X = *$ the constant diagram, $X (i_{0}) = *$ has a single $n$ -simplex for every $n$ . The set of $n$ -simplices of the bar construction is $$ B_n(*, I, *) = \coprod_{i_0 \to i_1 \to \cdots \to i_n} _n = {\text{chains of $n$ composable morphisms in $I$ }}, $$ which is the standard definition of the nerve $N (I)_{n}$ of the small category $I$ . The face and degeneracy maps in $B(, I, ) $ma t c h t h es t an d a r df a ce / d e g e n er a cy ma p s in t h e n er v e . H e n ce$ \operatorname{hocolim}_I * = |N(I)|$, the geometric realisation of the nerve. Rubric: full credit for matching the simplicial-set data to the nerve definition.

Exercise 6 (medium, short-answer).

Identify the homotopy colimit of the diagram $* ⇉ *$ indexed by the category with two objects $0, 1$ and two parallel morphisms $0 \to 1$ .

Hint

The plain colimit of two parallel maps is the coequaliser; here both maps are the unique map of points, so the plain colimit is a point. The homotopy colimit is the coequaliser of two parallel maps $pt ⇉ pt$ in the homotopy sense.

Answer

The indexing category has two objects $0, 1$ and two parallel non-identity arrows $α, β : 0 \to 1$ . The nerve $N (I)$ has:

two $0$ -simplices ( $0$ and $1$ ),
two non-degenerate $1$ -simplices ( $α$ and $β$ ),
no non-degenerate $2$ -simplices (the two arrows do not compose to a single arrow because they are parallel, not chained).

Hence $∣ N (I) ∣$ is a graph with two vertices and two edges between them, which is the circle $S^{1}$ . By Exercise 5, $hocolim_{I} * = ∣ N (I) ∣ = S^{1}$ . The plain colimit was a single point; the homotopy colimit picks up the loop $α β^{- 1}$ in the indexing category and realises it as the geometric circle. Rubric: full credit for the nerve computation and the $S^{1}$ identification.

Exercise 7 (hard, short-answer).

Prove that for a small category $I$ and a diagram $X : I \to sSet$ that is cofibrant in the projective model structure (so that levelwise weak equivalences out of $X$ are detected by maps of cofibrant objects), the natural map $hocolim_{I} X \to colim_{I} X$ from the homotopy colimit to the plain colimit is a weak equivalence.

Hint

Use the universal property of the bar construction: $B (*, I, X)$ is a functorial cofibrant replacement of $X$ in the projective model structure, and the natural map $B (*, I, X) \to X$ (viewed in $sSet^{I}$ ) is a levelwise weak equivalence. Apply $colim$ to both sides.

Answer

The bar construction $B (*, I, X)$ assembled into a diagram (replacing the "shifting" face $d_{0}$ with a structure map encoded by the chain) admits a natural augmentation $ϵ : B (*, I, X) \to X$ in $sSet^{I}$ given on $n$ -simplices by collapsing the chain $i_{0} \to \dots \to i_{n}$ to its endpoint $i_{n}$ and applying the composite morphism to the $X$ -coordinate. This map $ϵ$ is a levelwise weak equivalence (in fact a simplicial-homotopy equivalence on each object).

Now apply the plain colimit $colim_{I}$ . By definition of the bar construction, $colim_{I} B (*, I, X) = ∣ B (*, I, X) ∣$ (the diagonal-versus-coend identification), i.e. the bar-construction-realisation equals the colimit of the bar construction.

The natural map $colim_{I} ϵ : colim_{I} B (*, I, X) \to colim_{I} X$ is therefore the comparison map $hocolim_{I} X \to colim_{I} X$ .

For $X$ projectively cofibrant, $colim_{I}$ preserves weak equivalences between cofibrant diagrams (Ken Brown's lemma applied to the Quillen adjunction $colim_{I} ⊣ c$ in the projective model structure on $sSet^{I}$ ). The bar construction $B (*, I, X)$ is itself cofibrant (it is a transfinite composition of pushouts of generating cofibrations by construction). So $colim_{I} ϵ$ is a weak equivalence between cofibrant objects, completing the proof.

This is the conceptual statement that the homotopy colimit corrects the plain colimit only when the input fails to be cofibrant; cofibrant diagrams already see their plain colimit as their homotopy colimit. Rubric: full credit for the augmentation, the colimit-equals-realisation step, and the cofibrancy / Ken Brown conclusion.

Exercise 8 (hard, short-answer).

Identify the homotopy colimit of the diagram $X : B G \to sSet$ indexed by the one-object groupoid $B G$ (with automorphism group $G$ ) sending the unique object to the one-point space and every group element to the identity, and explain why the result is the classifying space $B G$ .

Hint

By Exercise 5, the homotopy colimit of the constant terminal diagram is the nerve of the indexing category. For $I = B G$ a one-object groupoid, the nerve is $N (B G)$ , which is the standard simplicial model of $B G$ .

Answer

Apply Exercise 5: $hocolim_{B G} * = ∣ N (B G) ∣$ . The nerve $N (B G)$ has one $0$ -simplex (the unique object), one $n$ -simplex per chain $g_{1}, g_{2}, \dots, g_{n}$ of group elements (interpreted as morphisms $* g_{1} * g_{2} \dots g_{n} *$ in the groupoid). This is exactly the standard simplicial model of the classifying space: $N (B G)_{n} = G^{n}$ , with face maps composing adjacent elements (or dropping the leftmost / rightmost) and degeneracies inserting identities.

The geometric realisation $∣ N (B G) ∣$ is the classifying space $B G$ as constructed by Milgram-Segal in the 1960s. For $G$ discrete, $B G$ is a $K (G, 1)$ , i.e. an Eilenberg-MacLane space whose only non-zero homotopy group is $π_{1} (B G) = G$ . For $G$ a topological group, the same nerve construction gives the topological classifying space, and the universal principal $G$ -bundle $E G \to B G$ is recovered by the bar construction $E (*, G, *) = ∣ B (*, G, *) ∣$ where one of the coefficients is the constant group action of $G$ .

The conclusion: the Bousfield-Kan formula on the one-object groupoid $B G$ with constant terminal diagram is the geometric definition of $B G$ , recovering the standard Milnor-Milgram-Segal construction of classifying spaces from the abstract homotopy-colimit framework. Rubric: full credit for the nerve identification, the connection to $K (G, 1)$ , and the EG / BG relationship.

Lean formalization [Intermediate+]

Mathlib has the simplex category and simplicial objects in Mathlib.AlgebraicTopology.SimplexCategory and Mathlib.AlgebraicTopology.SimplicialObject, the geometric realisation SSet.toTop, and substantial colimit and adjunction infrastructure in Mathlib.CategoryTheory.Limits.* and Mathlib.CategoryTheory.Adjunction.*. The Bousfield-Kan apparatus is absent. The intended formalisation in the companion module Codex.Modern.Homotopy.HomotopyColimitBK is schematically:

import Mathlib.AlgebraicTopology.SimplicialSet.Basic
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Functor.Category

namespace Codex.Modern.Homotopy.HomotopyColimitBK

open CategoryTheory

/-- A small indexing category I and a diagram X : I ⥤ sSet of
    simplicial sets. The Bousfield-Kan bar construction
    Bar(*, I, X) is the simplicial set whose n-simplices are
    pairs (chain of n composable arrows in I, n-simplex of the
    source space). -/
def barConstruction {I : Type*} [Category I]
    (X : I ⥤ SSet) : SSet :=
  sorry

/-- The Bousfield-Kan homotopy colimit hocolim_I X is the
    realisation of the bar construction. -/
def hocolim {I : Type*} [Category I] (X : I ⥤ SSet) : SSet :=
  barConstruction X

/-- Bousfield-Kan formula (1972 §XII.5.1): the homotopy colimit
    defined via cofibrant replacement in the projective model
    structure equals the bar construction. -/
theorem hocolim_eq_bar {I : Type*} [Category I] (X : I ⥤ SSet) :
    True := True.intro

/-- Pushout-as-double-mapping-cylinder: the homotopy pushout of
    a span A ← C → B is the double mapping cylinder
    A ⊔_C (C × Δ¹) ⊔_C B. -/
theorem hocolim_pushout_eq_mapping_cylinder
    (A B C : SSet) (f : C ⟶ A) (g : C ⟶ B) :
    True := True.intro

/-- Sequential hocolim as mapping telescope. -/
theorem hocolim_sequential_eq_telescope
    (X : ℕ → SSet) (f : ∀ n, X n ⟶ X (n + 1)) :
    True := True.intro

/-- Classifying space as hocolim of the constant terminal
    diagram on the one-object groupoid BG. -/
theorem classifying_space_eq_hocolim (G : Type) :
    True := True.intro

end Codex.Modern.Homotopy.HomotopyColimitBK

The formalisation gap is substantive. The required pieces: a SSet-valued bar construction with the explicit face / degeneracy formulae of Bousfield-Kan 1972 §XII.2; the projective and Reedy model structures on sSet^I as named instances of ModelCategory (depending on the model-category formalisation tracked in the sibling 03.12.31 unit); the derived left Kan extension along the unique functor $I \to *$ identified with the homotopy colimit; the comparison theorem between the bar-construction realisation and the derived left Kan extension. Each piece is formalisable from existing Mathlib infrastructure once the ModelCategory type-class lands. The companion module ships theorems as True placeholders against the eventual full implementation.

Advanced results [Master]

The Bousfield-Kan bar-construction formula

Theorem 1 (Bousfield-Kan 1972 §XII.5.1, the comparison theorem). Let $I$ be a small category, let $X : I \to sSet$ be a diagram of simplicial sets, and let $\mathbf{L} \operatorname{colim}_I X $d e n o t e t h e l e f t - d er i v e df u n c t or o f$ \operatorname*{colim}_I : \mathbf{sSet}^I \to \mathbf{sSet} $a t$ X $, co m p u t e d v ia co f ib r an t r e pl a ce m e n t in t h e p r o j ec t i v e m o d e l s t r u c t u r eo n$ \mathbf{sSet}^I$. Then there is a natural weak equivalence* $$ |B(, I, X)| \simeq \mathbf{L} \operatorname{colim}_I X $$ identifying the geometric realisation of the bar construction with the derived colimit.

The proof identifies $B (*, I, X)$ as a functorial cofibrant replacement of $X$ in $sSet^{I}$ . The augmentation $B (*, I, X) \to X$ is a levelwise weak equivalence (Exercise 7), and $B (*, I, X)$ is built as a transfinite composition of pushouts of generating projective cofibrations, hence is cofibrant. Applying $colim_{I}$ to a cofibrant replacement computes the left-derived functor. The colimit of the bar construction equals its realisation by a diagonal-versus-coend identification: $colim_{I} B_{∙} (*, I, X) = diag_{n} B_{∙, n} (*, I, X) = B_{n} (*, I, X)$ .

Theorem 2 (Bousfield-Kan 1972 §XI.3.3, the two-sided bar construction). Let $W : I^{op} \to sSet$ be a contravariant weight functor and $X : I \to sSet$ a covariant diagram. The two-sided bar construction $B (W, I, X)$ has $n$ -simplices $$ B_n(W, I, X) = \coprod_{i_0 \xrightarrow{\alpha_1} i_1 \xrightarrow{\alpha_2} \cdots \xrightarrow{\alpha_n} i_n} W(i_n)_n \times X(i_0)_n. $$ *Its realisation $∣ B (W, I, X) ∣$ is the weighted homotopy colimit of $X$ by $W$ . For $W = *$ the constant terminal weight, this recovers the ordinary Bousfield-Kan formula; for $W$ representable on a generic object $j$ (i.e. $W = Hom_{I} (-, j)$ ), this recovers $X (j)$ up to homotopy.*

The two-sided bar construction is the universal source of homotopy-colimit formulae. Specialising $W$ to different weights recovers homotopy pushouts, mapping telescopes, homotopy fibres (as one-sided fibred bar constructions), and the cobar construction (its dual). The functoriality of $B (W, I, X)$ in both $W$ and $X$ is at the heart of the categorical-homotopy-theory framework of Riehl 2014.

Pushout as double mapping cylinder

Theorem 3 (homotopy pushout as double mapping cylinder). Let $A f C g B$ be a span of simplicial sets (equivalently of topological spaces, replacing $sSet$ by $Top$ throughout). The Bousfield-Kan homotopy pushout is the double mapping cylinder $$ A \sqcup_C^{\mathrm{h}} B \simeq A \sqcup_{C \times {0}} (C \times \Delta^1) \sqcup_{C \times {1}} B, $$ where $Δ^{1}$ is the standard $1$ -simplex (a single interval). The map $C \times {0} \to A$ is $f$ , and $C \times {1} \to B$ is $g$ . The plain pushout $A ⊔_{C} B$ is recovered by collapsing the interval $Δ^{1}$ to a point.

The proof unfolds the bar construction on the pushout shape, which is the category with three objects ${0, 1, 2}$ and morphisms $0 \to 1$ and $0 \to 2$ (the legs of the span). The non-degenerate simplices of $B (*, I, X)$ are at most $1$ -dimensional, indexed by the two non-identity morphisms, and the realisation glues $C \times [0, 1]$ along its endpoints to $A$ and $B$ .

The double mapping cylinder is the standard topological model of the homotopy pushout, going back to Borsuk-Eilenberg-Steenrod. Its homotopy invariance is the foundational property that makes "long exact sequences of cofibre sequences" possible: replacing the legs of the span by homotopy-equivalent maps changes the plain pushout but not the homotopy pushout.

Theorem 4 (Mather's cube theorem, Mather 1976). Consider a cube of homotopy pushout squares. If five of the six faces are homotopy pushout squares, then so is the sixth.

This is the higher-dimensional manifestation of the homotopy-invariance of the double mapping cylinder. The proof uses the Bousfield-Kan formula applied to a $3$ -dimensional cube-shaped diagram and a careful identification of the squares with appropriate bar constructions.

Mapping telescope: sequential hocolim

Theorem 5 (sequential hocolim is the mapping telescope). Let $X_{0} f_{0} X_{1} f_{1} X_{2} \to \dots$ be a sequence of simplicial sets and let $Tel (X) = ⨆_{n} X_{n} \times [n, n + 1] / \sim$ be the mapping telescope. Then $\operatorname{hocolim}_{\mathbb{N}} X \simeq \mathrm{Tel}(X) $. M or eo v er, t h e na t u r a l ma p$ \mathrm{Tel}(X) \to \operatorname*{colim}_n X_n $f r o m t h e t e l esco p e t o t h e pl ain d i r ec tl imi t i s a w e ak e q u i v a l e n ce i f f t h es t r u c t u r e ma p s$ f_n$ are eventually levelwise weak equivalences.*

The proof identifies the bar construction on $N$ with the simplicial set whose non-degenerate $n$ -simplices are pairs of a strictly increasing chain $i_{0} < i_{1} < \dots < i_{n}$ in $N$ and a simplex of $X_{i_{0}}$ . Its realisation is the union over $n$ of $X_{n} \times Δ^{1}$ glued via $f_{n}$ along the right ends, which is exactly the telescope.

The mapping telescope is the canonical computational model of a sequential homotopy colimit. It appears in chromatic homotopy theory (as $Tel_{n}$ of a sequence of vanishing maps), in stable homotopy as the suspension spectrum $Σ_{+}^{\infty} X$ realised as $hocolim_{n} Ω^{n} Σ^{n + 1} X$ , and in K-theory as $K (R) = hocolim_{n} B GL_{n} (R)^{+}$ .

Classifying spaces

Theorem 6 (Segal 1968 / 1974, the classifying space as a hocolim). Let $G$ be a topological group and $B G$ its one-object groupoid. The Bousfield-Kan homotopy colimit of the constant terminal diagram is $$ \operatorname*{hocolim}_{BG} * \simeq |N(BG)| = BG, $$ the geometric realisation of the nerve of $B G$ , which is the classifying space of $G$ . Moreover, the bar construction $B(, G, ) $o n t h e a c t i o n c a t e g or y$ //G $(o bj ec t s a r e$ g \in G $a c t in g o na c h ose nba se p o in t) r eco v er s t h e u ni v er s a l p r in c i p a l$ G $- b u n d l e$ EG \to BG$.*

Segal 1974 (Categories and cohomology theories, Topology 13) gave the modern formulation: classifying spaces are nerves, and the universal bundle $E G \to B G$ is recovered functorially by a bar construction. The construction generalises to topological categories (giving classifying spaces of foliations à la Haefliger), to topological groupoids (giving classifying spaces of stacks), and to operads (giving Stasheff-style classifying spaces for $A_{\infty}$ structures).

Reedy and projective model structures

Theorem 7 (Reedy 1974, the Reedy model structure). Let $I$ be a Reedy category — a small category equipped with a degree function $de g : Ob (I) \to N$ and two subcategories $I^{+}, I^{-} \subseteq I$ (the "raising" and "lowering" parts) satisfying a unique-factorisation axiom. The diagram category $sSet^{I}$ carries a Reedy model structure with

(a) weak equivalences the levelwise weak equivalences,

(b) cofibrations the maps $f : X \to Y$ such that the relative latching map $X (i) ⊔_{L_{i} X} L_{i} Y \to Y (i)$ is a cofibration in $sSet$ for every $i \in I$ ,

(c) fibrations the maps $f : X \to Y$ such that the relative matching map $X (i) \to Y (i) \times_{M_{i} Y} M_{i} X$ is a fibration in $sSet$ for every $i \in I$ .

The Reedy model structure is the canonical compromise between the projective and injective structures: cofibrations are detected by latching objects (smaller than cofibrancy in the projective structure), and fibrations are detected by matching objects (smaller than fibrancy in the injective structure). For $I = Δ^{op}$ the Reedy model structure on bisimplicial sets is the foundation of the Bousfield-Friedlander spectral sequence and the diagonal-versus-realisation theorem.

Theorem 8 (Hirschhorn 2003 §18, the explicit Reedy hocolim formula). For $I$ a Reedy category, the Bousfield-Kan formula $|B(, I, X)| $co in c i d es w i t h t h e R ee d y - co f ib r an t - r e pl a ce m e n t f or m u l a f or t h e h o m o t o p y co l imi t . C o n cr e t e l y, t h e R ee d y co f ib r an t r e pl a ce m e n t o f a d ia g r am$ X $in$ \mathbf{sSet}^I$ is iteratively built by latching, and the colimit of the Reedy cofibrant replacement equals the bar-construction realisation up to weak equivalence.*

This is the technical content underlying the bar-construction approach: the bar construction is one explicit functorial cofibrant replacement, and there is a one-parameter family of equivalent replacements via the Reedy framework.

Homotopy left Kan extension

Theorem 9 (Riehl 2014 §6.2, homotopy left Kan extension as the derived adjoint). Let $φ : I \to J$ be a functor between small categories. The pullback functor $\varphi^ : \mathbf{sSet}^J \to \mathbf{sSet}^I $ha s a l e f t a d j o in t$ \operatorname{Lan}\varphi : \mathbf{sSet}^I \to \mathbf{sSet}^J $(t h eor d ina r y l e f t K an e x t e n s i o n) . T h e d er i v e d l e f t a d j o in t$ \mathbf{L} \operatorname{Lan}\varphi $e x i s t s w i t h r es p ec tt o t h e p r o j ec t i v e m o d e l s t r u c t u r eso n$ \mathbf{sSet}^I $an d$ \mathbf{sSet}^J $, an d t h e B o u s f i e l d - K an f or m u l a f or$ \mathbf{L} \operatorname{Lan}\varphi X $a t an o bj ec t$ j \in J$ is* $$ (\mathbf{L} \operatorname{Lan}\varphi X)(j) \simeq |B(*, \varphi / j, X|{\varphi / j})|, $$ *where $φ / j$ is the comma category of objects in $I$ over $j$ via $φ$ and $X|{\varphi / j}$ is the restriction.*

This is the most general form of the Bousfield-Kan formula and the foundational identity underlying the categorical-homotopy-theory framework. Specialising to $J = *$ recovers the ordinary homotopy colimit; specialising to $φ$ a fully faithful functor recovers a left-Kan-extension formula; specialising to $φ$ a Grothendieck fibration recovers the "homotopy colimit over each fibre" formula.

Synthesis. The Bousfield-Kan formula is the foundational reason that homotopy colimits exist as a uniform construction across topology, simplicial sets, chain complexes, and more general model categories. The central insight is that the bar construction packages the cofibrant-replacement step of the projective model structure on $sSet^{I}$ into an explicit simplicial-set formula whose realisation computes the derived left Kan extension; this is exactly the bridge between the abstract derived-functor framework of Quillen 1967 and the concrete point-set constructions that homotopy theorists actually compute with. Putting these together, every classical "homotopy colimit" computation — pushouts as double mapping cylinders, sequential limits as mapping telescopes, classifying spaces as nerves, derived smash products as bar constructions on monoid actions — fits the master template of "build $B (*, I, X)$ , realise it." The pattern recurs in 03.12.31 (Quillen model categories) where the framework of cofibrant replacement and left-derived functors that the bar construction implements is axiomatised, generalises to the weighted-colimit framework via the two-sided bar construction $B (W, I, X)$ where varying $W$ encodes every kind of homotopy-coherent diagram, and identifies the homotopy colimit with the universal property of left-derived left adjoints in the calculus of Quillen functors.

The bridge is between Bousfield-Kan's 1972 explicit simplicial recipe and the modern $(\infty, 1)$ -categorical viewpoint where every small $\infty$ -category $I$ has a category $Fun (I, S)$ of $S$ -valued diagrams and a colimit functor $colim_{I} : Fun (I, S) \to S$ . In the $\infty$ -categorical world the colimit is automatically homotopy-invariant — there is no plain-vs-homotopy distinction because $S$ already incorporates homotopy. The Bousfield-Kan formula is what the $\infty$ -categorical colimit reduces to when $S$ is presented by the Kan-Quillen model structure on $sSet$ and $I$ is presented by an ordinary small category. The classical 1972 framework and the modern $\infty$ -categorical framework are equivalent presentations of the same homotopy theory.

Full proof set [Master]

Proposition 1 (the bar construction is a cofibrant replacement in the projective model structure). Let $I$ be a small category and $X : I \to sSet$ a diagram. The bar construction $B(, I, X) $a sse mb l e d in t o a d ia g r am$ \widetilde{B}(, I, X) : I \to \mathbf{sSet} $(v ia t h e " s hi f t in g " f a ce$ d_0 $a s t h es t r u c t u r e ma p) i sco f ib r an t in t h e p r o j ec t i v e m o d e l s t r u c t u r eo n$ \mathbf{sSet}^I $, an d t h e na t u r a l a ug m e n t a t i o n$ \widetilde{B}(, I, X) \to X$ is a levelwise weak equivalence.*

Proof. The proof has two parts: cofibrancy and the weak-equivalence claim.

Cofibrancy. The diagram $B (*, I, X)$ is built by a transfinite filtration $F_{0} \subseteq F_{1} \subseteq F_{2} \subseteq \dots$ indexed by simplicial degree, where $F_{p}$ consists of the simplices coming from chains of length $\leq p$ together with their iterated faces / degeneracies. Each inclusion $F_{p} ↪ F_{p + 1}$ is a pushout of generating projective cofibrations: at each $i \in I$ , the chain $i \to i_{1} \to \dots \to i_{p}$ together with its non-degenerate simplices contributes a copy of the free $I$ -diagram on the standard simplex $Δ^{p}$ pushed out along boundary inclusions. Free $I$ -diagrams on standard simplices are cofibrant in the projective structure (they are the generating projective cofibrations), and pushouts of cofibrations are cofibrations.

Levelwise weak equivalence. The augmentation $B (*, I, X) \to X$ at object $i \in I$ has the form $B_{∙} (*, I, X) (i) \to X (i)$ where the source has $n$ -simplices the chains $i \to i_{1} \to \dots \to i_{n}$ starting at $i$ together with an $n$ -simplex of $X (i)$ , and the augmentation collapses the chain to its starting object.

The fibre of the augmentation over a fixed $n$ -simplex $x \in X (i)$ is the simplicial set $N (i / I)$ , the nerve of the under-category $i / I$ (objects: arrows out of $i$ in $I$ ; morphisms: composites). The under-category $i / I$ has an initial object — the identity arrow $id_{i}$ — so its nerve $N (i / I)$ is contractible (a category with an initial object has a contractible nerve, by an explicit simplicial homotopy collapsing onto the initial vertex).

The augmentation is a fibration with contractible fibres at each $n$ -simplex, hence a weak equivalence by the standard fibration-with-contractible-fibres argument in $sSet$ . $□$

Proposition 2 (Bousfield-Kan formula for pushouts). Let $A f C g B$ be a span of simplicial sets, viewed as a diagram $X : I \to sSet$ where $I$ is the pushout shape with objects ${0, 1, 2}$ and arrows $0 \to 1$ , $0 \to 2$ . Then $$ |B(*, I, X)| \cong A \sqcup_{C \times {0}} (C \times \Delta^1) \sqcup_{C \times {1}} B. $$

Proof. Compute the bar construction explicitly. The non-degenerate chains in $I$ are:

length $0$ : the three identity chains ${0}, {1}, {2}$ ;
length $1$ : the two non-identity arrows $0 \to 1$ and $0 \to 2$ ;
length $\geq 2$ : none, because the indexing category has no $2$ -composable non-identity arrow chains.

Substituting into the bar-construction formula: the $0$ -simplices are $X (0)_{0} ⊔ X (1)_{0} ⊔ X (2)_{0} = C_{0} ⊔ A_{0} ⊔ B_{0}$ . The non-degenerate $1$ -simplices over the chain $0 \to 1$ are pairs $(0 \to 1, x \in X (0)_{1}) = (0 \to 1, c \in C_{1})$ , with face maps $d_{0}$ applying $f : C \to A$ on the $X$ -coordinate and $d_{1}$ being the identity on $C$ . Symmetrically for $0 \to 2$ with $g : C \to B$ .

The realisation glues two copies of the standard $1$ -simplex $Δ^{1}$ for each $C$ -point: one going from $C$ (at vertex $0$ ) to $A$ (at vertex $1$ ) via $f$ , and one going from $C$ to $B$ via $g$ . The result is exactly the double mapping cylinder $A ⊔_{C \times {0}} (C \times Δ^{1}) ⊔_{C \times {1}} B$ with the left endpoint glued to $A$ via $f$ and the right endpoint glued to $B$ via $g$ . $□$

Proposition 3 (the bar construction commutes with realisation up to weak equivalence). Let $I$ be a small category and $X : I \to sSet$ a diagram. Then $$ |B(, I, X)| \cong B(, I, |X|), $$ where on the right side $∣ X ∣ : I \to Top$ is the levelwise geometric realisation and the bar construction is computed in $Top$ via the analogous formula.

Proof. Both sides are realisations of bisimplicial objects; the left one is the bar construction in $sSet$ realised, the right one is the levelwise realisation followed by the topological bar construction. By the Fubini theorem for bisimplicial realisations (Quillen 1973, Goerss-Jardine 2009 §IV.1.2), the two iterated realisations agree.

More explicitly: the realisation $∣ - ∣ : sSet \to Top$ preserves colimits (as a left adjoint to $Sing$ ), preserves finite products (by Milnor's 1957 theorem on compactly generated spaces), and commutes with the bar construction in the relevant sense. The bar construction is itself a colimit (coproduct of pieces indexed by chains), so realisation commutes with it, completing the identification. $□$

Proposition 4 (homotopy invariance of the homotopy colimit). Let $f : X \to Y$ be a natural transformation of diagrams $X, Y : I \to sSet$ that is levelwise a weak equivalence. Then the induced map $B(, I, f) : B(, I, X) \to B(, I, Y) $i s a w e ak e q u i v a l e n ce in$ \mathbf{sSet}$.*

Proof. This is the Key Theorem proved in the Intermediate tier above. We restate the load-bearing steps. Form both bar constructions as diagonals of bisimplicial sets $B_{∙, ∙} (*, I, -)$ . The induced map at horizontal-level $p$ and vertical-level $q$ is $$ \coprod_{i_0 \to \cdots \to i_p} X(i_0)q \to \coprod{i_0 \to \cdots \to i_p} Y(i_0)q, $$ the disjoint union over chains of $f{i_0, q} $. D i s j o in t u ni o n so f w e ak e q u i v a l e n ces a r e w e ak e q u i v a l e n ces (in t h e l e v e l w i sese n seo n s im pl i c ia l se t s) . B y t h e B o u s f i e l d - F r i e d l an d er d ia g o na l l e mma (G oer ss - J a r d in e 2009§ I V .1.7), t h e d ia g o na l o f a r o w - w i se w e ak e q u i v a l e n ceo f bi s im pl i c ia l se t s i s a w e ak e q u i v a l e n ce . H e n ce$ B(*, I, f) $i s a w e ak e q u i v a l e n ce .$ \square$

Proposition 5 (mapping telescope from the bar construction). Let $X_{0} f_{0} X_{1} f_{1} X_{2} \to \dots$ be a sequential diagram. Then $$ |B(*, \mathbb{N}, X)| \cong \mathrm{Tel}(X) := \bigsqcup_{n \geq 0} (X_n \times \Delta^1) \big/ \sim, $$ where $\sim$ identifies $(x, 1) \in X_{n} \times Δ^{1}$ with $(f_{n} (x), 0) \in X_{n + 1} \times Δ^{1}$ for every $n$ and every $x \in X_{n}$ .

Proof. Compute the bar construction on $I = N$ (as a poset, hence a small category with at most one arrow between objects). The non-degenerate chains $i_{0} < i_{1} < \dots < i_{p}$ in $N$ have one chain per strictly increasing sequence; the shortest non-identity chains are the length- $1$ chains $n \to n + 1$ (and longer chains, which by repeated subdivision contribute only via degeneracies after collapse).

The $p = 0$ contribution gives one $0$ -simplex per object: $⨆_{n} X_{n}$ as a $0$ -truncated simplicial set. The $p = 1$ contribution from the chain $n \to m$ for $n < m$ gives the bar simplicies $X_{n} \times Δ^{1}$ glued at the $1$ -vertex via the composite $X_{n} \to X_{m}$ . For the canonical "next-step" chains $n \to n + 1$ with the structure map $f_{n}$ , the realisation glues $X_{n} \times Δ^{1}$ to $X_{n + 1}$ along its right endpoint via $f_{n}$ , producing the mapping telescope formula.

Chains of length $\geq 2$ contribute only via degenerate simplices in the $N$ -shape: the non-degenerate part of the bar construction is at most $1$ -dimensional in the chain direction. This is because every chain $i_{0} < i_{1} < \dots < i_{p}$ in $N$ with $p \geq 2$ has a face that retracts to the longest single arrow $i_{0} \to i_{p}$ , and the higher-dimensional simplices collapse by simplicial homotopy onto the $1$ -skeleton.

Hence $∣ B (*, N, X) ∣$ is the union of the $X_{n} \times Δ^{1}$ glued by $f_{n}$ at the right endpoints, which is exactly the mapping telescope. $□$

Proposition 6 (nerve identification for the constant terminal diagram). For any small category $I$ and the constant terminal diagram $ : I \to \mathbf{sSet} $, t h e ba r co n s t r u c t i o ni s t h e n er v eo f$ I$:* $$ B(*, I, ) = N(I). $$ Consequently, $\operatorname{hocolim}_I * = |N(I)|$.

Proof. The bar construction has $n$ -simplices $$ B_n(*, I, *) = \coprod_{i_0 \to \cdots \to i_n} _n = {\text{length- $n$ chains of composable morphisms in $I$ }}. $$ This is exactly the definition of the nerve $N (I)_{n}$ . The face maps in the bar construction collapse the leftmost or rightmost arrow / compose adjacent arrows / drop endpoints, matching the face maps of the nerve. The degeneracies insert identities, matching the nerve's degeneracies. Hence $B(, I, ) = N(I) $a ss im pl i c ia l se t s, an d$ \operatorname{hocolim}_I * = |N(I)| $a s d es i r e d .$ \square$

Connections [Master]

Quillen model category 03.12.31. The Bousfield-Kan construction is the explicit point-set realisation of the left-derived functor $L colim_{I} : Ho (sSet^{I}) \to Ho (sSet)$ in the projective model structure on the diagram category. The Quillen-adjunction framework guarantees the existence of the derived functor; the bar construction gives the concrete formula. The connection is foundational: every theorem in the present unit either uses the projective model structure directly (homotopy invariance via Ken Brown) or proves a statement that the projective model structure axiomatises.
Simplicial sets and geometric realization 03.12.25. The Bousfield-Kan formula outputs a simplicial set $B (*, I, X)$ whose geometric realisation is the homotopy colimit. Every step of the construction lives in the simplicial-set framework: the bar construction is a simplicial-set operation, the diagonal is a bisimplicial-set operation, and the realisation is the standard $∣ - ∣$ functor. The unit therefore depends critically on the simplicial-set machinery of 03.12.25 and showcases its most powerful application.
Kan-Quillen model structure on sSet 03.12.33. The homotopy-invariance and Ken-Brown-lemma arguments of the present unit are carried out in the Kan-Quillen model structure on $sSet$ , in which every simplicial set is cofibrant and the fibrant replacement comes from the small-object argument applied to the generating acyclic cofibrations $Λ_{k}^{n} ↪ Δ^{n}$ . The diagram-category model structure $sSet^{I}$ in which $hocolim_{I}$ is the left-derived left adjoint inherits its weak equivalences and fibrations level-wise from 03.12.33, so the left-Quillen functor status of $colim_{I}$ rests entirely on the prototype model structure developed there. The bar construction $B (*, I, X)$ is then the explicit point-set realisation of the derived left Kan extension along $I \to *$ .
CW complex 03.12.10. The realisation $∣ B (*, I, X) ∣$ is a CW complex (in fact $Δ$ -complex), and the Bousfield-Kan construction is the standard machine for producing CW models of homotopy types. Pushouts as double mapping cylinders, sequential hocolims as telescopes, and classifying spaces as nerve realisations are all CW complexes built from the bar construction. The CW structure inherits one cell per non-degenerate simplex of the bar construction.
Suspension 03.12.03. The unreduced suspension $Σ X = X ⋆ S^{0}$ is the homotopy pushout $* \leftarrow X \to *$ . The Bousfield-Kan formula applied to this span recovers the double mapping cylinder $X \times Δ^{1} / (X \times {0}, X \times {1})$ , which is the standard suspension construction. Iterating gives $Σ^{n} X$ as iterated homotopy colimits, with the iterated suspension recovered via the bar construction on a tower of pushout shapes.
Singular homology 03.12.11. The Mayer-Vietoris long exact sequence and the spectral sequence of a homotopy colimit (the Bousfield-Kan spectral sequence) are direct consequences of the bar-construction filtration. Singular homology applied to $∣ B (*, I, X) ∣$ produces a spectral sequence with $E_{2}^{p, q} = colim_{I}^{p} H_{q} (X)$ converging to $H_{p + q} (hocolim_{I} X)$ , generalising Mayer-Vietoris (the spectral sequence on a pushout shape) to arbitrary indexing categories.
Spectral sequences [03.13.*]. The Bousfield-Kan spectral sequence (developed in the sibling unit on Bousfield-Kan spectral sequences, currently pending) is the systematic computational tool for evaluating $H_{*} (∣ B (*, I, X) ∣)$ from the levelwise cohomology of the diagram. Its construction is the filtration by simplicial degree of the bar construction; the $E_{1}$ -term is the chain complex of the levelwise homology along the chains in $I$ , and the $E_{2}$ -term computes derived functors of the colimit on the indexing category. The unit on this spectral sequence will build directly on the bar-construction formula proved here.
Eilenberg-MacLane spaces 03.12.05. The Eilenberg-MacLane space $K (π, n)$ for $n \geq 1$ is a homotopy colimit of an iterated suspension diagram of $K (π, 0)$ : $K (π, n) ≃ Σ^{n} K (π, 0) / (identifications)$ . The Bousfield-Kan formula gives the explicit simplicial-set model, recovering Eilenberg-MacLane's 1953 nerve construction for abelian $π$ as the bar construction on the constant diagram $* : B π \to sSet$ shifted in degree.
Fundamental groupoid 03.12.08. The classifying space of a groupoid $G$ (in the sense of the fundamental groupoid framework of 03.12.08) is $∣ N (G) ∣$ , which by Proposition 6 of the present unit is $hocolim_{G} *$ . The two perspectives — the fundamental groupoid as a homotopy-theoretic invariant of a space, and the classifying space as a homotopy colimit of a constant diagram — agree on a $K (π, 1)$ via this Bousfield-Kan formula. The connection makes the equivalence between groupoid models and classifying-space models concrete.

Historical & philosophical context [Master]

Aldridge Bousfield and Daniel Kan introduced the homotopy-colimit construction now bearing their names in the 1972 monograph Homotopy Limits, Completions and Localizations (Springer Lecture Notes in Mathematics 304) ^{[Bousfield-Kan 1972]}. The monograph grew out of work in the late 1960s on $p$ -completion and $p$ -localisation of spaces — operations that required a precise sense in which a space could be "completed at $p$ " via a tower of fibrations. The Bousfield-Kan formula for the homotopy limit of the tower (the $p$ -completion) and the dual formula for the homotopy colimit (the bar construction) were the technical heart of the monograph. The bar-construction approach was inspired by Eilenberg-MacLane's 1953 bar construction for classifying spaces of groups and by Milnor's 1956 construction of the universal bundle, which is essentially the bar construction $B (*, G, *)$ on the action category of $G$ .

The Bousfield-Kan formula sat alongside earlier related constructions. Roy Vogt's 1973 Convenient categories of topological spaces for homotopy theory (Archiv. Math. 22) ^{[Vogt 1973]} proved a closely related theorem on homotopy-invariant colimits in topological-category settings. Graeme Segal's 1968 Classifying spaces and spectral sequences (Publ. Math. IHES 34) ^{[Segal 1968]} used the same nerve-of-a-category construction to define classifying spaces of topological categories, foundational for foliation theory and the Segal-McDuff approach to stable homotopy. By 1974, Segal's Categories and cohomology theories (Topology 13) ^{[Segal 1974]} had consolidated the simplicial-categorical viewpoint.

The model-categorical reformulation came in stages. Quillen 1967 (Homotopical Algebra, LNM 43) ^{[Quillen 1967]} had set up the framework of model categories and derived functors but did not explicitly address diagram categories or homotopy colimits. The projective model structure on $sSet^{I}$ was developed by Bousfield-Kan themselves in the 1972 monograph (implicitly) and given a full Quillen-style treatment by Christopher Reedy 1974 in unpublished notes (the Reedy model structure carries his name; the Reedy unique-factorisation axiom was published in a 1974 preprint and circulated widely before its formal publication). Philip Hirschhorn's 2003 Model Categories and Their Localizations (AMS Mathematical Surveys 99) ^{[Hirschhorn 2003]} gave the first complete published treatment of the Reedy and projective model structures on arbitrary diagram categories, and rigorously identified the bar-construction realisation with the derived left Kan extension along the unique functor $I \to *$ . The Dwyer-Spalinski 1995 Homotopy theories and model categories (Handbook of Algebraic Topology Ch. 2) ^{[Dwyer-Spalinski 1995]} gave the canonical pedagogical introduction.

The Bousfield-Kan framework was a foundational input to the $(\infty, 1)$ -categorical revolution. André Joyal's 2002 work on quasi-categories ^{[Joyal 2002]} and Jacob Lurie's 2009 Higher Topos Theory ^{[Lurie 2009]} developed an alternative model in which the homotopy colimit is the universal cocone in an $\infty$ -category and is automatically homotopy-invariant. The Bousfield-Kan formula remains the standard computational tool: every concrete homotopy-colimit calculation in chromatic homotopy theory (since Hopkins-Mahowald in the 1980s), motivic homotopy theory (since Morel-Voevodsky 1999), topological cyclic homology (since Bökstedt-Hsiang-Madsen 1993), and equivariant stable homotopy (Mandell-May 2002, Hill-Hopkins-Ravenel 2009) reduces in practice to a bar-construction computation. Emily Riehl's 2014 Categorical Homotopy Theory (Cambridge) ^{[Riehl 2014]} gave the modern weighted-colimit perspective, presenting the two-sided bar construction $B (W, I, X)$ as the universal tool from which every homotopy-coherent diagrammatic construction descends. Dan Dugger's 2008 A primer on homotopy colimits ^{[Dugger 2008]} remains the standard pedagogical introduction for users of the formula across applied areas.

Bibliography [Master]

@book{BousfieldKan1972,
  author    = {Bousfield, Aldridge K. and Kan, Daniel M.},
  title     = {Homotopy Limits, Completions and Localizations},
  series    = {Lecture Notes in Mathematics},
  volume    = {304},
  publisher = {Springer-Verlag},
  year      = {1972}
}

@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}
}

@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}
}

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

@unpublished{Dugger2008,
  author    = {Dugger, Daniel},
  title     = {A primer on homotopy colimits},
  note      = {Preprint, University of Oregon},
  year      = {2008}
}

@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{Quillen1967,
  author    = {Quillen, Daniel G.},
  title     = {Homotopical Algebra},
  series    = {Lecture Notes in Mathematics},
  volume    = {43},
  publisher = {Springer-Verlag},
  year      = {1967}
}

@article{Segal1968,
  author    = {Segal, Graeme},
  title     = {Classifying spaces and spectral sequences},
  journal   = {Publications Math{\'e}matiques de l'IH{\'E}S},
  volume    = {34},
  year      = {1968},
  pages     = {105--112}
}

@article{Segal1974,
  author    = {Segal, Graeme},
  title     = {Categories and cohomology theories},
  journal   = {Topology},
  volume    = {13},
  year      = {1974},
  pages     = {293--312}
}

@article{Vogt1973,
  author    = {Vogt, Rainer M.},
  title     = {Convenient categories of topological spaces for homotopy theory},
  journal   = {Archiv der Mathematik},
  volume    = {22},
  year      = {1973},
  pages     = {545--555}
}

@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{Mather1976,
  author    = {Mather, Michael},
  title     = {Pull-backs in homotopy theory},
  journal   = {Canadian Journal of Mathematics},
  volume    = {28},
  year      = {1976},
  pages     = {225--263}
}

Prerequisites

03.12.25
03.12.31

Tier anchors

beginner: Dwyer-Spalinski 1995 *Homotopy theories and model categories* §10 informal opening on homotopy limits and colimits
intermediate: Bousfield-Kan 1972 *Homotopy Limits, Completions and Localizations* (LNM 304) §XI-§XII; Dwyer-Spalinski 1995 §10; Hirschhorn 2003 *Model Categories and Their Localizations* §18
master: Bousfield-Kan 1972 *Homotopy Limits, Completions and Localizations* (LNM 304) §X-§XII (originator); Hirschhorn 2003 *Model Categories and Their Localizations* (AMS Mathematical Surveys 99) §18-§19; Riehl 2014 *Categorical Homotopy Theory* §6; Dugger 2008 *A primer on homotopy colimits*; Goerss-Jardine 2009 *Simplicial Homotopy Theory* §IV

References

TODO_REF
Bousfield-Kan — Homotopy Limits, Completions and Localizations · Springer Lecture Notes in Mathematics 304 (1972); originator monograph. §XI bar construction and homotopy colimits, §XII.2 the simplicial replacement BB(*, I, X), §XII.5.1 the realisation formula, §X-§XI tower of fibrations side, §IX.5 completion at a prime
TODO_REF
Hirschhorn — Model Categories and Their Localizations · AMS Mathematical Surveys and Monographs 99 (2003); §18 Reedy model structure on diagram categories, §18.5 cofibrant replacement and the explicit hocolim formulae, §19.6 Bousfield-Kan and the comparison theorem with the bar construction
TODO_REF
Dwyer-Spalinski — Homotopy theories and model categories · Handbook of Algebraic Topology (Elsevier 1995) Ch. 2 pp. 73-126; §10 homotopy colimits as left-derived left adjoints, pushout-as-double-mapping-cylinder worked example
TODO_REF
Riehl — Categorical Homotopy Theory · Cambridge New Mathematical Monographs 24 (2014); §6 homotopy limits and colimits, Bousfield-Kan formula derived from the two-sided bar construction, weighted-colimit perspective
TODO_REF
Dugger — A primer on homotopy colimits · preprint, expository (2008); the canonical pedagogical introduction with detailed pushout / telescope examples and the cofibrant-replacement viewpoint
TODO_REF
Goerss-Jardine — Simplicial Homotopy Theory · Birkhäuser Progress in Mathematics 174 (1999, repr. 2009); §IV bisimplicial sets and diagonal, §IV.1 Bousfield-Kan and homotopy colimits, §IV.5 spectral sequence
TODO_REF
Quillen — Homotopical Algebra · Springer Lecture Notes in Mathematics 43 (1967); §II derived functors of left adjoints, the original framework underlying the Bousfield-Kan construction
TODO_REF
Segal — Categories and cohomology theories · Topology 13 (1974) 293-312; the classifying-space-as-nerve construction underlying the Bousfield-Kan bar-construction approach to BG

Lean module

Codex.Modern.Homotopy.HomotopyColimitBK

Mathlib gap

Mathlib has the simplex category and simplicial objects in
`Mathlib.AlgebraicTopology.SimplexCategory` and
`Mathlib.AlgebraicTopology.SimplicialObject`, geometric realisation
via `SSet.toTop` in `Mathlib.AlgebraicTopology.GeometricRealization`,
and substantial colimit infrastructure in
`Mathlib.CategoryTheory.Limits.*`. The Bousfield-Kan apparatus is
absent: the bar construction `Bar(*, I, X)` as a named simplicial
object built from a small category `I` and a diagram `X : I ⥤ sSet`
with the explicit face / degeneracy formulae of Bousfield-Kan 1972
§XII.2; the projective and Reedy model structures on the diagram
category `sSet^I` as named instances; the comparison theorem
identifying the derived-left-Kan-extension homotopy colimit with the
bar-construction realisation; the explicit pushout-as-double-mapping-
cylinder identification; and the sequential-hocolim-as-mapping-
telescope identification. The companion module
`Codex.Modern.Homotopy.HomotopyColimitBK` ships theorem statements as
`True` placeholders awaiting the underlying model-category
formalisation package.

Reviewer

TBD

Estimated time

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