$\def\A{\mathcal{A}} \def\C{\mathcal{C}} \def\D{\mathcal{D}} \def\ind{\operatorname{Ind}} \def\op{\mathrm{op}} \def\Hom{\operatorname{Hom}}$I am trying to understand the following result from Kashiwara, Schapira, Categories and Sheaves (in the following, I will be using the notation and terminology from the book):

Let $\mathcal{C}$ and $\mathcal{C}^{\prime}$ be two categories. By Proposition 6.1.9, the projection functors $\mathcal{C} \times \mathcal{C}^{\prime} \rightarrow \mathcal{C}$ and $\mathcal{C} \times \mathcal{C}^{\prime} \rightarrow \mathcal{C}^{\prime}$ define the functor $$ \tag{6.1.2} \label{map} \theta: \operatorname{Ind}(\mathcal{C} \times \mathcal{C}^{\prime}) \rightarrow \operatorname{Ind}(\mathcal{C}) \times \operatorname{Ind}(\mathcal{C}^{\prime}) $$

Proposition 6.1.12. The functor $\theta$ in \eqref{map} is an equivalence.

Proof. A quasi-inverse to $\theta$ is constructed as follows. To $A \in \ind(\C)$ and $A'\in\ind(\C')$, associate $\underset{\underset{((X\to A),(X'\to A'))\in\C_A\times\C'_{A'}}{\longrightarrow}}{“\operatorname{lim}”}(X,X')$. Since $\C_A\times\C'_{A'}$ is cofinally small and filtrant, it belongs to $\ind(\C\times\C')$. $\square$

(The notation $\underset{\longrightarrow}{“\operatorname{lim}”}$ means inductive limit in the category of presheaves, i.e., if $\alpha:I\to\C$ is some diagram, then $\underset{\longrightarrow}{“\operatorname{lim}”}\alpha:=\varinjlim (\mathrm{h}_C\circ\alpha)$, where $\mathrm{h}_\C:\C\to\operatorname{Fct}(\C^\op,\mathbf{Set})$ is the Yoneda embedding.)

I'm having trouble verifying that the map described in the proof is a quasi-inverse for $\theta$. Denote the map by $\mu: \operatorname{Ind}(\mathcal{C}) \times \operatorname{Ind}(\mathcal{C}^{\prime}) \rightarrow\operatorname{Ind}(\mathcal{C} \times \mathcal{C}^{\prime})$, i.e., \begin{equation*} \tag{1}\label{mu} \mu(A,A')=\underset{\underset{((X\to A),(X'\to A'))\in\C_A\times\C'_{A'}}{\longrightarrow}}{“\operatorname{lim}”}(X,X'). \end{equation*} On the other hand, for $B\in\ind(\C\times\C')$, we have $$ \tag{2}\label{theta} \theta(B)=\left(\underset{\underset{((X,X')\to B)\in(\C\times\C')_B}{\longrightarrow}}{“\operatorname{lim}”}X,\underset{\underset{((X,X')\to B)\in(\C\times\C')_B}{\longrightarrow}}{“\operatorname{lim}”}X'\right)=(A,A'). $$

My first question is:

(Q1). To compute $\mu(\theta(B))$, we plug \eqref{theta} into \eqref{mu}. But now, how come that we obtain $B$ back? I'm a little bit clueless (same problem to compute $\theta(\mu(A,A'))$ by plugging \eqref{mu} into \eqref{theta}).

I came up with an alternative proof. My second question is:

(Q2). Is Lemma 4 or my proof of Proposition 5 written or hinted at somewhere in the literature?

The proof below requires inspecting closely the properties of the functor $\iota_\C:\C\to\ind(\C)$ to intrinsically characterize an ind-localization functor (Lemma 4 below), to later realize that $\iota_\C\times\iota_{\C'}:\C\times\C'\to\ind(\C)\times\ind(\C')$ satisfies these properties (Proposition 5 below).

Proposition 1. Let $F:\C\to\D$ be a functor, and assume $\D$ admits all small filtrant limits. Then the functor $\iota_\C^\dagger F:\ind(\C)\to\D$ exists, is finitary¹ and satisfies $\iota_\C^\dagger F\circ\iota_\C\cong F$. Conversely, if a functor $\widetilde{F}:\ind(\C)\to\D$ satisfies the following two conditions:

1. $\widetilde{F}\circ\iota_\C\simeq F$,
2. $\widetilde{F}$ commutes with any small filtrant limits with values in $\C$ (i.e., for any small filtrant diagram $\alpha:I\to\C$, $\widetilde{F}(\underset{\longrightarrow}{“\operatorname{lim}”}\alpha)\simeq\varinjlim(F\circ\alpha)$,

then $\widetilde{F}\simeq\iota_\C^\dagger F$.

Proof. This is the ind-counterpart of [KS, Proposition 2.7.1] and the proof is the same, but now one uses that $\C_A$ is cofinally small and filtrant for each $A\in\ind(\C)$ [KS, Proposition 6.1.5], so that all $\C_A$-indexed diagrams in $\D$ have an inductive limit. $\square$

Write $\Hom^{fl}(\C,\D)$ for the full subcategory of $\Hom(\C,\D)$ made up of finitary functors (i.e., the functors that preserve all filtrant limits that exist in $\C$).

Definition 2. Let $\C$ be a category. An ind-localization of $\C$ is a functor $\iota:\C\to\widetilde{\C}$ such that the precomposition functor $$ \tag{3}\label{fun} \iota_*:\Hom^{fl}(\widetilde{\C},\D)\to\Hom(\C,\D) $$ is an equivalence of categories, whenever $\D$ has all small filtrant limits.

Corollary 3. $\iota_\C:\C\to\ind(\C)$ is an ind-completion. Moreover, a quasi-inverse to $\iota_{\C,*}$ as in \eqref{fun} is given by $\iota_\C^\dagger$.

Proof. This result is the ind-counterpart of [KS, Corollary 2.7.4] and the proof is the same. $\square$

So far we know that the functor $\iota_\C$ is fully faithful (it is in fact the Yoneda embedding), right exact,¹ right small,² [KS, Corollary 6.1.6], and dense³ [KS, Proposition 2.6.3]. There is the following sort of converse:

Lemma 4. Suppose $\iota:C\to\widetilde{C}$ is a functor which is fully faithful, right exact, right small and dense. Let $F:\C\to\D$ be a functor where $\D$ has all small inductive limits. Then the left Kan extension $\iota^\dagger F$ exists and $\iota^\dagger F\circ\iota\simeq F$. Moreover, $\iota$ is the ind-localization of $\C$ if and only if $\iota^\dagger F$ is finitary for all $F:\C\to\D$ where $\D$ has all small inductive limits. In this case, $\iota^\dagger$ is a quasi-inverse to \eqref{fun}.

Proof. We argue as in the proof of Proposition 1: Given $A\in\widetilde{C}$, the inductive limit $\displaystyle\varinjlim_{(\iota(X)\to A)\in\C_A}F(X)$ exists since $\C_A$ is cofinally small and filtrant (hence there is a cofinal functor $I\to\C_A$ with $I$ small and filtrant) and $\D$ has all filtrant limits. Thus this limit defines $\iota^\dagger F(A)$, so $\iota^\dagger F$ exists [KS, Theorem 2.3.3]. By loc. cit., $\iota^\dagger F\circ\iota\cong F$, for $\iota$ is fully faithful. If $\iota$ is an ind-localization of $\C$, then $\iota^\dagger F$ is finitary (argued before). Conversely, suppose $\iota^\dagger F$ is finitary for all such $F$. Then reasoning as in the proofs of Proposition 1 and Corollary 3 we conclude that $\iota^\dagger$ is a quasi-inverse to $\iota_*$ as in \eqref{fun} (density of $\iota$ provides the uniqueness property from the statement of Proposition 1). $\square$

Proposition 5. $\iota_\C\times\iota_{\C'}:\C\times\C'\to\ind(\C)\times\ind(\C')$ is an ind-localization.

Proof. We verify the hypotheses of Lemma 4 on $\iota_\C\times\iota_{\C'}$. This functor is fully faithful since it is a product of fully faithful functors. Since $(\C\times\C')_{(A,A')}=\C_A\times\C'_{A'}$ for $(A,A')\in\ind(\C)\times\ind(\C')$, it is also right exact and right small (the product of filtrant categories is filtrant, then use [KS, Proposition 3.2.6] to prove that the product of filtrant and cofinally small categories is cofinally small). The functor $\iota_\C\times\iota_{\C'}$ is dense: For $(A,A')\in\ind(\C)\times\ind(\C')$, we have to show that $(A,A')=\varinjlim((\iota_\C\times\iota_{\C'})\circ\Pi)$, where $\Pi:(\C\times\C')_{(A,A')}=\C_A\times\C'_{A'}\to\C\times\C'$ is the projection. For a test element $(T,T')\in\ind(\C)\times\ind(\C')$ we have \begin{align*} &\phantom{=}\varprojlim_{((X,X')\to(A,A'))\in \C_A\times\C'_{A'}} \Hom_{\ind(\C)\times\ind(\C')}((X,X'),(T,T'))\\ &=\varprojlim_{((X,X')\to(A,A'))\in \C_A\times\C'_{A'}} \Hom_{\ind(\C)}(X,T)\times\Hom_{\ind(\C')}(X',T')\\ &\simeq\varprojlim_{(X\to A)\in \C_A} \left(\varprojlim_{(X'\to A')\in \C'_{A'}} \Hom_{\ind(\C)}(X,T)\times\Hom_{\ind(\C')}(X',T') \right)\\ &\simeq\varprojlim_{(X\to A)\in \C_A}\left( \Hom_{\ind(\C)}(X,T)\times \varprojlim_{(X'\to A')\in \C'_{A'}} \Hom_{\ind(\C')}(X',T') \right)\\ &\simeq\varprojlim_{(X\to A)\in \C_A} \Hom_{\ind(\C)}(X,T)\times \varprojlim_{(X'\to A')\in \C'_{A'}} \Hom_{\ind(\C')}(X',T'), \end{align*} where in the last two isomorphisms we have used that filtrant limits commute with finite products in the category of sets, \begin{align*} &\simeq \Hom_{\ind(\C)}\bigg(\varinjlim_{(X\to A)\in \C_A}X,T\bigg)\times \Hom_{\ind(\C')}\bigg(\varinjlim_{(X'\to A')\in \C'_{A'}}X',T'\bigg)\\ &=\Hom_{\ind(\C)}(A,T)\times \Hom_{\ind(\C')}(A',T')\\ &=\Hom_{\ind(\C)\times\ind(\C')}((A,A'),(T,T')), \end{align*} This exhibits $(A,A')$ as the inductive limit of $(\iota_\C\times\iota_{\C'})\circ\Pi$.

Finally, given a functor $F:\C\times\C'\to\D$ where $\D$ has all small filtrant limits, we have to show that $(\iota_\C\times\iota_{\C'})^\dagger F$ is finitary. By [MO], it suffices to show that $\Hom_{\ind(\C)\times\ind(\C')}((X,X'),-):\ind(\C)\times\ind(\C')\to\mathbf{Set}$ is finitary for $(X,X')\in\C\times\C'$. Indeed, let $(\alpha,\alpha'):I\to\ind(\C)\times\ind(\C')$ be a filtrant diagram, and let $(T,T')\in\ind(\C)\times\ind(\C')$. Then $\varinjlim(\alpha,\alpha')=(\varinjlim\alpha,\varinjlim\alpha')$ [ref] and \begin{align*} &\phantom{=}\Hom_{\ind(\C)\times\ind(\C')}((X,X'),(\varinjlim\alpha,\varinjlim\alpha'))\\ &=\Hom_{\ind(\C)}(X,\varinjlim\alpha) \times\Hom_{\ind(\C')}(X',\varinjlim\alpha')\\ &\cong\varinjlim\Hom_{\ind(\C)}(X,\alpha)\times\varinjlim\Hom_{\ind(\C')}(X',\alpha') &\text{by [KS, eq. (2.6.1)],}\\ &\cong\varinjlim(\Hom_{\ind(\C)}(X,\alpha)\times\Hom_{\ind(\C')}(X',\alpha')) &\text{since filtrant limits commute}\\ &&\text{with finite projective limits,}\\ &=\varinjlim\Hom_{\ind(\C)\times\ind(\C')}((X,X'),(\alpha,\alpha')), \end{align*} as desired. $\square$

References

[KS] Kashiwara, Schapira, Categories and Sheaves

[MO] John Bourke, When do Kan extensions preserve limits/colimits?, https://mathoverflow.net/a/112206

A functor $F:\C\to\C'$ is:

¹finitary if it preserves all small filtrant limits,

²right exact if the category $\C_U$ is filtrant for any $U\in\C'$,

³right small if the category $\C_U$ is cofinally small for any $U\in\C'$ (a category $\D$ is cofinally small if there is a cofinal functor $I\to \D$, where $I$ is small),

⁴dense if $\displaystyle U\cong\varinjlim_{(F(X)\to U)\in\C_U} F(X)$ for all $U\in\C'$ (here is the full list of equivalent definitions).