Solution (source code)

= Solution

A <diagram in a category> of shape $J$ is a <functor> $D:J\to\mathcal C$. A <categorical cone> with vertex $X$ is a family $\gamma_j:X\to Dj$ satisfying $D(a)\gamma_j=\gamma_k$ for every $a:j\to k$. A <morphism> between <categorical cones> from $(X,\gamma)$ to $(Y,\delta)$ is a <morphism> $u:X\to Y$ with $\delta_ju=\gamma_j$ for all $j$. A <categorical limit> is a <terminal object> in this <category> of cones: each cone has a unique such <morphism> to the limiting cone.

For a finite $J$, form the <products in a category>
$$
P=\prod_{j\in\operatorname{ob}J}Dj,\qquad Q=\prod_{a:j\to k}Dk.
$$
Define $s,t:P\rightrightarrows Q$ with $a$-coordinates $D(a)\pi_j$ and $\pi_k$. The <equalizer> $e:L\to P$ imposes exactly the cone equations. Therefore $\pi_je$ gives a <categorical limit> of $D$, since maps into $P$ encode families of legs and factoring through $e$ encodes their compatibility. The empty <product in a category> is the <terminal object>, covering the empty diagram. This is the <construction of small limits from products and equalizers>, restricted to finite shapes.

Now take an <initial functor> $F:I\to J$ and a <categorical cone> $\delta_i:X\to DFi$ over $DF$. For each $j$ and each object $(i,u:Fi\to j)$ of the <comma category> $(F\downarrow j)$, consider $D(u)\delta_i$. A <morphism> $a:(i,u)\to(i',u')$ there satisfies $u'F(a)=u$, so
$$
D(u')\delta_{i'}=D(u')D(Fa)\delta_i=D(u)\delta_i.
$$
Since $(F\downarrow j)$ is a nonempty <connected category>, this common value is independent of the object. Define it to be $\gamma_j$. This does not require choosing representatives: the value is uniquely determined.

For $b:j\to k$, replacing $(i,u)$ by $(i,bu)$ proves $D(b)\gamma_j=\gamma_k$. Taking $(i,1_{Fi})$ proves $\gamma_{Fi}=\delta_i$. Conversely, extending a restricted cone recovers its original legs, since $\gamma_j=D(u)\gamma_{Fi}$. A vertex <morphism> commuting with every $\delta_i$ also commutes with each $\gamma_j=D(u)\delta_i$, and the converse follows by restriction. Thus extension and restriction are strictly inverse <functors>, not merely an <equivalence of categories>. This proves <cone restriction along an initial functor>.

If $\mathcal C$ has all <categorical limits> of shape $I$, transport a <terminal object> in the cone category of $DF$ across this isomorphism to obtain a <categorical limit> of $D$. Uniqueness of the induced comparison, and its compatibility with <natural transformations> of diagrams, gives
$$
\boxed{\lim_J\cong\lim_I\circ F^*.}
$$
For the converse use the <representable test for initial functors>. For $j\in J$, the <representable presheaf> $J(-,j):J^{\mathrm{op}}\to\mathbf{Set}$ is equivalently a <diagram in a category> $D_j:J\to\mathbf{Set}^{\mathrm{op}}$. Its <categorical limit> in the <opposite category> is the <colimit> of $J(-,j)$ in <sets>. Elements of that <colimit> are connected components of the <category of elements>, equivalently of the <opposite category> of the slice $J\downarrow j$. This slice has <terminal object> $(j,1_j)$, so that <colimit> is a singleton.

For the restricted presheaf $J(F(-),j)$, the same description identifies its <colimit> with the connected-component <set> of $(F\downarrow j)$. Indeed a relation identifying $u':Fi'\to j$ with $u'F(a):Fi\to j$ is exactly a generating edge of the zigzag relation in this <comma category>. The assumed isomorphism of limit <functors> forces this <set> to be a singleton. Therefore $(F\downarrow j)$ is nonempty and connected for every $j$, proving
$$
\boxed{F\text{ is initial}.}
$$