The Stacks project

I think the $t_{H(i)}$ in the diagram should be $t_i$.

Well, I am following the notation: If $t : F \to G$ is a transformation of functors then $t$ is made up of maps $t_X : F(X) \to G(X)$ where $X$ varies over objects of the source category of $F$ and $G$. Since in the statement of the lemma $M$ and $N \circ H$ have source $\mathcal{J}$, I think the notation makes sense. I am not saying the notation is perfect though...

Both $M$ and $N\circ H$ have source category $I$, right? So wouldn't writing $t_i$ be in accordance with the notation?

Oops! Yes. Fixed. Thanks!

An underrated lemma imho. Below is a suggested "abstract abstract nonsense nonsense" style proof. I.e., rather than explicitly deal in "abstract nonsense" (the data of cocones etc.), we instead reduce the claim to symbol-pushing in $\textit{Cat}$ (without invoking $\textit{Cat}$ or any other $2$-categorical notions explicitly).

---

Dependencies:

The following would ideally be included as definitions/lemmata in an earlier section, presumably Section 0013 (section-definition-categories).

1. Given categories $\mathcal{X}$, $\mathcal{Y}$, and $\mathcal{Z}$, define the usual bifunctor and show the bifunctoriality of $$( \circ , \star ) : \text{Fun}( \mathcal{Y} , \mathcal{Z} ) \times \text{Fun}( \mathcal{X} , \mathcal{Y} ) \to \text{Fun}( \mathcal{X} , \mathcal{Z} ) .$$

2. Given categories $\mathcal{X}$ and $\mathcal{Y}$, define the constant functor $$\text{const} : \mathcal{Y} \to \text{Fun}( \mathcal{X} , \mathcal{Y} )$$ as $$\text{const} : y \mapsto ( x \mapsto y )$$ $$\text{const} : \psi \mapsto ( x \mapsto \psi )$$ on objects and morphisms respectively and show that for any functor $F$ and natural transformation $f$ for which the respective compositions are well-defined, $$\text{const} (y) \circ F = \text{const} (y)$$ $$\text{const} (\psi) \star t = \text{const} (\psi) .$$ (There are also formulae for composition on the other side, but they aren't relevant to what follows.)

---

Argument:

Given category $\mathcal{X}$ and diagam $F : \mathcal{X} \to \mathcal{C}$, define the (covariant) functor $$\text{coCones}( - ; F) : \mathcal{C} \to \textit{Sets}$$ as $$c \mapsto \text{Mor} _ { \text{Fun}( \mathcal{X} , \mathcal{C} ) } ( F , \text{const} (c) )$$ $$\phi \mapsto \text{Mor} _ { \text{Fun}( \mathcal{X} , \mathcal{C} ) } ( \text{id} _ F , \text{const} (\phi) ) .$$ I.e., $\text{coCones}( c ; F)$ is the set of cocones under $F$ with vertex $c$ equipped with the corresponding functorial action by morphisms of $\mathcal{C}$ realized as the set of natural transformations from $F$ to the constant functor at $c$.

By the prior discussion in Section 002D (section-limits), $\text{colim} (F)$ is defined as the corepresenting object of $\text{coCones}( - ; F)$ (precisely) when the latter exists. Hence by (the formal dual of) Lemma 001P (lemma-yoneda), it suffices in the context of the current lemma to construct a natural transformation $$\text{coCones}( - ; N) \to \text{coCones}( - ; M)$$ (note the implicit contravariance).

Indeed, the formula $$k \mapsto ( k \star \text{id} _ H ) \circ t$$ prescribes the components (the parametrizing $c \in \text{Ob} (\mathcal{C})$ implicit in the type of $k : N \to \text{const} (c)$) of such a natural transformation; naturality is given by the equation $$( k \mapsto ( ( \text{const} (\phi) \circ k ) \star \text{id} _ H ) \circ t ) = ( k \mapsto \text{const} (\phi) \circ ( k \star \text{id} _ H ) \circ t )$$ or equivalently that (for all $k$) $$( ( \text{const} (\phi) \circ k ) \star \text{id} _ H ) \circ t = \text{const} (\phi) \circ ( k \star \text{id} _ H ) \circ t$$ where the latter follows purely symbolically from the interchange law and the relevant identity above.

---

Note/strenghtening:

As currently formulated, this lemma is prima facie "evil" in the sense that it constructs a morphism (distinguishable up to equality) in terms of a functor (distinguishable only up to isomorphism). The underlying phenomenon is that there is, given $\mathcal{C}$, a (strict) $2$-category $\text{coDiag} _ {\mathcal{C}}$ defined so that

• the objects of $\text{coDiag} _ {\mathcal{C}}$ are the pairs $( \mathcal{I} : \textit{Cat} , M : \mathcal{I} \to \mathcal{C} )$

• the morphisms from $( \mathcal{I} , M )$ to $( \mathcal{J} , N )$ are the pairs $( H : \mathcal{I} \to \mathcal{J} , t : M \to N \circ H )$

• the morphisms from $( G , s )$ to $( H , t )$ are the pairs $( r : G \to H , ( \text{id} _ N \star r ) \circ s = t )$

and we will have turned out to have, via the above formula, in fact constructed a (strict) $2$-functor $$\text{coCones} : \text{coDiag} _ {\mathcal{C}} \to \text{Fun} ( \mathcal{C} , \textit{Sets} )$$ where the codomain is a $1$-category so all the $2$-morphisms of $\text{coDiag} _ {\mathcal{C}}$ (including the noninvertible ones!) are sent to equalities in $\text{Fun} ( \mathcal{C} , \textit{Sets} )$.

The proof is just more symbol pushing: Given $( r , ( \text{id} _ N \star r ) \circ s = t ) : ( G , s ) \to ( H , t )$ as above, we must show that $$( k \mapsto ( k \star \text{id} _ G ) \circ s ) = ( k \mapsto ( k \star \text{id} _ H ) \circ t )$$ or equivalently that (for all $k$) $$( k \star \text{id} _ G ) \circ s = ( k \star \text{id} _ H ) \circ t .$$ This follows from the equality in the hypothesis, the interchange law, and the equality $$k \star r = ( \text{const} ( \text{id} _ c ) \circ k ) \star ( r \circ \text{id} _ G ) = k \star \text{id} _ G$$ where $c$ is the object of $\mathcal{C}$ at whose component we're implicitly working.

(Of course, it doesn't make expository sense to invoke the language of $2$-categories so early in the chapter just to state all this. But what can be said purely $1$-categorically is that any two $( G , s )$ and $( H , t )$ related by an $(r , ( \text{id} _ N \star r ) \circ s = t )$ induce equal maps between colimits.)

---

Ps.:

The above discussion formally dualizes to the corresponding discussion concerning limits (possibly relevant to Stacks) and straightforwardly generalizes to account for weighted (co)limits (presumably outside the scope of Stacks). As always, I am happy to implement and submit the desired subset of the above as a patch/PR.