I'm reading about inverse images of sheaves. I'll restate the definition to clarify the notation.
Let $f:X\to Y$ be continuous and $\mathscr{G}$ be a sheaf on $Y$. We define $$ f^+\mathscr{G}(U)=\varinjlim_{V\supset f(U)}\mathscr{G}(V), $$ where $V$ runs through all open sets in $Y$ containing $f(U)$. Then we define $f^{-1}\mathscr{G}$ to be the sheafification of $f^+\mathscr{G}$.
Now I'm trying to compute the stalks of $f^{-1}\mathscr{G}$. We have
$$ \left(f^{-1} \mathscr{G}\right)_x \cong\left(f^{+} \mathscr{G}\right)_x=\underset{U\ni x}{\varinjlim}\left(f^{+}\mathscr{G}\right)(U) =\varinjlim_{U\ni x}\varinjlim_{V\supset f(U)} \mathscr{G}(V)=\varinjlim_{V\ni f(x)} \mathscr{G}(V)=\mathscr{G}_{f(x)}. $$ There is one step I'm confused of: the step where the two direct limits are combined into one. It is intuitive clear that as $V$ runs through open sets containing $f(U)$, where $U$ runs through open sets containing $x$, it's the same as $V$ running through open sets containing $f(x)$.
However, can someone give a rigorous category-theoretic justification of this step? I was able to write down a (potential) proof using the definition of inductive limits, but it was quite long and tedious. Is there a simple way to tell that the two inductive limits can be combined into one?
Similarly: let $g: Y \rightarrow Z$ be a second continuous map and let $\mathscr{H}$ be a presheaf on $Z$. Then $$ f^{+}\left(g^{+} \mathscr{H}\right)(U)=\varinjlim_{V\supset f(U)}g^+\mathscr{H}(V)=\varinjlim_{V\supset f(U)}\varinjlim_{W\supset g(V)}\mathscr{H}(W)=\varinjlim_{W\supset g(f(U))}\mathscr{H}(W)=(g \circ f)^{+} \mathscr{H} $$ Same question: Is there a category-theoretic justification for the step where we combine the two inductive limits into one?
It would also be great if someone could explain what it means for these constructions to be functorial. For example, the author (Gortz & Wedhorn) asserts that the above isomorphism is functorial in $\mathscr{H}$.
In general, it is annoying to work with the explicit expression of colimits but for stalks of sheaves, the situation is much more clear, there is a smart way to write things down (of course, this just follows from the definition). For a presheaf $\mathscr{F}$, ou can show the follows $$\mathscr{F}_x = \left \{[s,U] \mid U \ \text{open and} \ s \in\mathscr{F}(U) \right \}$$ where $[s,U] = [t,V]$ if $s_{\mid U \cap V} = t_{\mid U \cap V}$ and the additiion and the multiplication are given by $$[s,U]+[t,V] = [s_{\mid U \cap V} + t_{\mid U \cap V}, U \cap V] \ \ \ \ [s,U][t,V] = [s_{\mid U \cap V}t_{\mid U \cap V}, U \cap V].$$ The same strategy can be used to express $\varinjlim_{f(U) \subset V} \mathscr{G}(V)$ and you end up with $$\varinjlim_{x \in U}\varinjlim_{f(U) \subset V} \mathscr{G}(V) = \left \{[[s,V],U] \mid x \in U, f(U) \subset V, s \in \mathscr{G}(V) \right \}$$ and this is canonically bijective to $$ \left \{[[s,V],f^{-1}(V)] \mid f(x) \in V, s \in \mathscr{G}(V) \right \} =\left \{[s,V] \mid f(x) \in V, s \in \mathscr{G}(V) \right \} = \mathscr{G}_{f(x)}.$$ A similar proof shows that the connection isomorphism $(f^+(g^+\mathscr{H})) \simeq (g \circ f)^+\mathscr{H}$ is canonical.