\input phomework \def\fcc{{\bf Fcc}} \def\U{{\sans U}} \def\V{{\sans V}} \def\comp{{\sans comp}} \def\C{{\bf C}} \def\D{{\bf D}} \def\E{{\bf E}} \def\F{{\bf F}} \def\G{{\bf G}} \def\int{{\sans Int}} \def\ext{{\sans Ext}} \def\fst{{\rm fst}} \def\snd{{\rm snd}} \def\pfst{{\sans L}} \def\psnd{{\sans R}} {\it January 2, 2001} \diagramstyle[PostScript=dvips] Choose a universe $\V$. and a universe $\U$ such that $\V\in\U$. Let $\fcc$ be the category of finitely complete $\U$-small categories with functors preserving finite limits as arrows. An {\it internal category} in a finitely complete category $\C$ is an object $H$ of $\C$ and arrows $d_0,d_1\colon H\to H$ and $\comp\colon H\times_H H \to H$ --- where $H\times_H H$ is the pullback \diagram H\times_H H\SEpbk&\rTo^{\snd}&H\cr \dTo<{\fst}&&\dTo>{d_0}\cr H&\rTo_{d_1}&H\cr \enddiagram of $d_1$ and $d_0$ --- such that the following diagrams commute: \diagram && H &&& H && \cr (C1)&& \uTo<{d_0}&\rdTo>{d_1} && \uTo<{d_1}&\rdTo>{d_0} &&(C2)\cr && H&\rTo_{d_0}&H & H&\rTo_{d_1}&H && \cr \enddiagram \diagram && H&\rTo^{\pair{\id_H}{d_1}_H}&H\times_H H&\lTo^{\pair{d_0}{\id_H}_H}&H\cr (C3)&& &\rdCong&\dTo~{\comp}&\ldCong\cr && &&H\cr \enddiagram \diagram && H&\lTo^{\fst}&H\times_H H&\rTo^{\snd}&H\cr (C4)&& \dTo<{d_0}&&\dTo~{\comp}&&\dTo>{d_1}\cr && H&\lTo_{d_0}&H&\rTo_{d_1}&H\cr \enddiagram \diagram (C5)&& H\times_H H\times_H H&\rTo^{\id_H\times_H \comp}&H\times_H H\cr && \dTo<{\comp\times_H\id_H}&&\dTo>\comp\cr && H\times_H H&\rTo_\comp&H\cr \enddiagram An {\it internal functor} from an internal category $(H,d_0,d_1,\comp)$ in $\C$ to an internal category $(H',d_0',d_1',\comp')$ in $\C$ is an arrow $F\colon H\to H'$ in $\C$ such that the following diagrams commute: \diagram && H&\rTo~F&H'\cr && \uTo<{d_0}&&\uTo>{d_0'}\cr (F1)&& H&\rTo~F&H'\cr && \dTo<{d_1}&&\dTo>{d_1'}\cr && H&\rTo~F&H'\cr \enddiagram \diagram && H\times_H H&\rTo^{\pair{F\circ \fst}{F\circ \snd}_{H'}}&H'\times_{H'} H'\cr (F2)&& \dTo<\comp&&\dTo>{\comp'}\cr && H&\rTo_F&H'\cr \enddiagram \shout{Proposition:} Internal categories and internal functors in a finitely complete $\U$-small category $\C$ form a $\U$-small category, $\int(\C)$. \proc{Proof:} It clearly follows from the fact that $\C$ is $\U$-small that the collections of internal categories in $\C$ and internal functors are respectively $\U$-small. We define composition of internal functors in $\C$ by composition of the corresponding arrows in $\C$. \part{Composition is well-defined:} If we have internal functors $F\colon H\to H'$ and $G\colon H'\to H''$ in $\C$, then certainly $G\circ F$ is an arrow of $\C$, but we must check that it is an internal functor $H\to H''$. Preservation of `domain' and `codomain' is an easy diagram-chase: \diagram H&\rTo~F&H'&\rTo~G&H''\cr \uTo<{d_0}&&\uTo>{d_0'}&&\uTo>{d_0''}\cr H&\rTo~F&H'&\rTo~G&H''\cr \dTo<{d_1}&&\dTo>{d_1'}&&\dTo>{d_1''}\cr H&\rTo~F&H'&\rTo~G&H''\cr \enddiagram To see that `composition' is preserved for the composite we must establish the commutativity of \diagram H\times_H H&\rTo^{\pair{GF\fst}{GF \snd}_{H''}}&H''\times_{H''} H''\cr \dTo<\comp&&\dTo>{\comp''}\cr H&\rTo_{GF}&H''\cr \enddiagram given the commutativity of \diagram H\times_H H&\rTo^{\pair{F\fst}{F \snd}_{H'}}&H'\times_{H'} H'&\rTo^{\pair{G\fst'}{G \snd'}_{H''}}&H''\times_{H''} H''\cr \dTo<\comp&&\dTo>{\comp'}&&\dTo>{\comp''}\cr H&\rTo_F&H'&\rTo_G&H''\cr \enddiagram so it suffices to show that $\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'} = \pair{GF\fst}{GF \snd}_{H''}$. But observe that we have $$\fst''\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'} = G\fst' \pair{F\fst}{F \snd}_{H'} = GF\fst$$ and $$\snd''\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'} = G\snd' \pair{F\fst}{F \snd}_{H'} = GF\snd$$ so that $\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'}$ has the property which uniquely characterizes $\pair{GF\fst}{GF \snd}_{H''}$, namely that it fits into the pullback diagram \diagram H\times_H H\cr &\rdTo(2,4)_{GF\fst}\rdDotsto\rdTo(4,2)^{GF\snd}&\cr &&H''\times_{H''} H''&\rTo_{\snd''}&H''\cr &&\dTo>{\fst''}&&\dTo>{d_0''}\cr &&H''&\rTo_{d_1''}&H''\cr \enddiagram \part{Identities exist:} The identity internal functor for an internal category $(H,d_0,d_1,\comp)$ is just the identity arrow on $H$. We need to check that $\id_H$ is an internal functor; preservation of `domain' and `codomain' is trivial, and preservation of `composition' again follows from the universal property of the pullback. That is, we have that $\pair{\id_H\fst}{\id_H\snd}_H = \id_{H\times_H H}$, so that (F2) commutes for $H' = H$ and $F = \id_H$. That these identites behave correctly under composition follows directly from the behavior of identity arrows in $\C$. \part{Composition is associative:} Associativity of composition in $\int(\C)$ is again a direct conseqence of associativity of composition in $\C$. \cqed \shout{Proposition:} Let $\C$ be a finitely complete $\U$-small category. Then $\int(\C)$ is finitely complete. \proc{Proof:} \part{Terminal object:} The terminal object of $\int(\C)$ is the internal category whose `object of homomorphisms' $H$ is the terminal object $1_\C$ of $\C$. The arrows $d_0,d_1,\comp$ are all then necessarily the unique endomorphism $!\colon 1_\C \to 1_\C$. The universal property of the terminal object of $\int(\C)$ is satisfied precisely because it is satisfied for the terminal object of $\C$. \part{Pairwise products:} Suppose $(H,d_0,d_1,\comp),(H',d_0',d_1',\comp')$ are two internal categories in $\C$. We define the product in $\int(\C)$ `pointwise', i.e. $(H\times H', d_0\times d_0', d_1\times d_1', \comp \times \comp')$. There appears to be a type mismatch; the type of $\comp\times \comp'$ is $(H\times_H H) \times (H'\times_{H'} H') \to H\times H'$, and we want it to be $(H\times H') \times_{H\times H'} (H\times H') \to H \times H'$. However, $(H\times H') \times_{H\times H'} (H\times H')$ and $ (H\times_H H) \times (H'\times_{H'} H')$ are uniquely isomorphic since $\times$ is a right adjoint and so preserves limits, in particular pullback diagrams. That $H\times H'$ {\it et al.} is in fact an internal category follows from further application of preservation of limits by the product. It remains to check that the universal property of the product holds; suppose we have an internal category $(H'',d_0'',d_1'',\comp'')$ and internal functors $F\colon H'' \to H$ and $G\colon H'' \to H'$. Now $\pair F G$ (where pairing is in $\C$) is the unique morphism in $\C$ such that $\pfst \pair F G = F$ and $\psnd \pair F G = G$, where $\pfst,\psnd$ are the projections from $H\times H'$, again in $\C$. It is easy to check that these projections are in fact internal functors, and that the pairing is an internal functor. \part{Equalizers:} Suppose we have two internal parallel functors \diagram H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr \enddiagram we can find the equalizer in $\C$ to obtain an object $H''$ and an arrow $E\colon H''\to H$ in $\C$: \diagram H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr %&\luDotsto&\uTo\cr %&&H^{(3)}\cr \enddiagram Our first priority is to find structure to make $H''$ an internal category. Consider the diagram \diagram H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr &&\uTo<{d_0}&&\uTo>{d_0'}\cr H''&\rTo_E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr \enddiagram and notice that since $F,G$ are internal functors and $E$ equalizes $F,G$, we have $F d_0 E = d_0' F E = d_0' G E = G d_0 E$. That is, $d_0 E$ also equalizes $F,G$, which provides us an arrow $d''_0\colon H''\to H''$ such that the following diagram commutes: \diagram H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr \uDotsto<{d''_0}&&\uTo<{d_0}&&\uTo>{d_0'}\cr H''&\rTo_E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr \enddiagram Similarly, we get $d_1''$ out of the diagram \diagram H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr \uDotsto<{d''_1}&&\uTo<{d_1}&&\uTo>{d_1'}\cr H''&\rTo_E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr \enddiagram since $d_1 E$ equalizes $F,G$, and we get $\comp''$ out of the diagram \diagram H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr \uDotsto<{\comp''}&&\uTo<\comp&&\uTo>{\comp'}\cr H''\times_{H''} H''&\rTo_{\pair{E \fst''}{E \snd''}_{H}}&H\times_H H&\pile{\rTo^{\pair{F \fst}{F\snd}_{H'}}\cr \rTo_{\pair{G \fst}{G\snd}_{H'}}\cr}&H'\times_{H'} H'\cr \enddiagram and observing that $$\eqalign{ \pair{F \fst}{F\snd}_{H'} \pair{E \fst''}{E \snd''}_{H} &= \pair{FE \fst''}{FE\snd''}_H\cr &= \pair{GE \fst''}{GE\snd''}_H\cr &= \pair{G \fst}{G\snd}_{H'} \pair{E \fst''}{E \snd''}_{H}\cr }$$ Now it is easy to check that $(H'', d_0'', d_1'', \comp'')$ is an internal category; for example, by choice $d_0''$ is the unique arrow such that $E d_0'' = d_0 E$, yet $E d_1'' d_0'' = d_1 E d_0'' = d_1 d_0 E = d_0 E$, so it must be that $d_1'' d_0'' = d_0''$. It falls out of the diagrams already shown that $E$ is an internal functor $H''\to H$. Now suppose we have a situation as depicted in the diagram \diagram H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr &\luDotstoI\cr &&H^{(3)}\cr \enddiagram where $H^{(3)}$ is an internal category and $I$ is an internal functor equalizing $F,G$. The universal property of the equalizer in $\C$ guarantees a unique arrow $J$ making the diagram commute. To see that $J$ is internal functorial, consider the following diagram: \diagram H''&&&\rTo^{d_0''}&&&H''\cr \uToJ\cr &\ruTo~I&&&&\luTo~I&\cr H^{(3)}&&&\rTo_{d_0^{(3)}}&&&H^{(3)}\cr \enddiagram the internal trapezoids commute because $E,I$ are internal functors, and the triangles commute by choice of $J$. Hence $E d_0'' J = E J d_0^{(3)}$, and because $E$ (being an equalizer) is mono, we know $d_0'' J = J d_0^{(3)}$. The proofs that $J$ preserves `codomain' and `composition' are similar. Therefore we conclude that $E$ is the equalizer of $F,G$ in $\int(\C)$. \cqed \shout{Proposition:} $\C \mapsto \int(\C)$ as defined above is the object part of a functor $\int\colon \fcc \to \fcc$. \proc{Proof:} Let $\F\colon \C \to \D$ be an arrow in $\fcc$, i.e. a finite limit preserving functor from $\C$ to $\D$. Now $\int(\F)$ also needs to be a finite limit preserving functor, but from $\int(\C)$ to $\int(\D)$. Suppose we have an internal category $(H,d_0,d_1,\comp)$ in $\C$. Then we define $\int(\F)(H,d_0,d_1,\comp) := (\F H, \F d_0, \F d_1, \F \comp)$. Because $\F$ preserves composition and finite products, $(\F H, \F d_0, \F d_1, \F \comp)$ is an internal category in $\D$. The action of $\int(\F)$ on arrows of $\int(\C)$ is the obvious one; $\int(\F)(F) := \F F$. Now it is possible to see that $\int(\F)$ is functorial since $\int(\F)(\id_H) = \F(\id_H) = \id_{\F H} = \id_{\int(\F)(H)}$ for any internal category object $H$ in $\C$, and $\int(\F)(G \circ F) = \F(G \circ F) = \F(G) \circ \F(F) = \int(\F)(G) \circ \int(\F)(F)$ for any internal functors $F\colon H\to H'$ and $G\colon H'\to H''$ in $\C$. Now we check that $\int(\F)$ preserves finite limits; We have first of all that $\int(\F)(1_{\int(\C)}) = (\F 1_{\int(\C)}, \F !, \F !, \F !) = (1_{\int(\D)}, !, !, !)$ because $\F$ preserves the terminal object. Moreover, just by unrolling definitions again we see $$\eqalign{ \int(\F)((H, d_0, d_1, \comp) \times ( H', d_0', d_1', \comp')) &= \int(\F)(H\times H', d_0 \times d_0', d_1 \times d_1', \comp\times \comp') \cr &= (\F(H\times H'), \F(d_0 \times d_0'), \F(d_1 \times d_1'), \F(\comp\times \comp')) \cr &= (\F H\times \F H', \F d_0 \times \F d_0', \F d_1 \times \F d_1', \F \comp\times \F\comp') \cr &= (\F H, \F d_0, \F d_1, \F \comp) \times (\F H', \F d_0', \F d_1', \F\comp') \cr &= (\F H, \F d_0, \F d_1, \F \comp) \times (\F H', \F d_0', \F d_1', \F\comp') \cr &= \int(\F)(H, d_0, d_1, \comp) \times \int(\F)( H', d_0', d_1', \comp') \cr }$$ and similarly $\int(\F)$ preserves equalizers because $\F$ does. Finally, we want $\int$ itself to be functorial. Suppose we have arrows $\F\colon \C\to \D$ and $\G\colon \D\to \E$ in $\fcc$. Then $$\eqalign{ \int(\G \circ \F)(H, d_0, d_1, \comp) &= ((\G\circ \F)(H), (\G\circ \F)(d_0), (\G\circ \F)(d_1), (\G\circ \F)(\comp))\cr &= (\G(\F(H)), \G(\F(d_0)), \G(\F(d_1)), \G(\F(\comp)))\cr &= \int(\G)(\F(H), \F(d_0), \F(d_1), \F(\comp))\cr &= \int(\G)(\int(\F)(H, d_0, d_1, \comp))\cr &= (\int(\G) \circ \int(\F))(H, d_0, d_1, \comp)\cr }$$ and for any object $\C$ of $\fcc$ we know $$\eqalign{ \int(\id_\C)(H, d_0, d_1, \comp) &= (\id_\C(H), \id_\C(d_0), \id_\C(d_1), \id_\C(\comp))\cr &= (H, d_0, d_1, \comp)\cr }$$ and so $\int(\id_\C) = \id_{\int(\C)}$, hence $\int\colon \fcc \to \fcc$ is functorial.\cqed \shout{Conjecture:} There exists a functor $\ext\colon \fcc \to \fcc$ such that $\int\dashv \ext$. \shout{Conjecture:} $\fcc$ is countably cocomplete. \shout{Corollary:} There exists a finitely complete $U$-small category $\C$ such that $\int(\C) \cong \C$. \proc{Proof:} Let $\Sets_\V$ be the ($\U$-small) category of all $\V$-small sets. There exists a functor $F\colon \Sets_\V\to \int(\Sets_\V)$ defined by $$F(S) := (S, \id_S, \id_S, \id_S)$$ and $$F(f) := f$$ So we can form the diagram \diagram D&:=&\Sets_\V&\rTo^f&\int(\Sets_\V)&\rTo^{\int(f)}&\int^2(\Sets_\V)&\rTo^{\int^2(f)}\cdots \enddiagram and set $\C := \dirlim\, D$ to obtain \diagram \Sets_\V&\rTo^f&\int(\Sets_\V)&\rTo^{\int(f)}&\int^2(\Sets_\V)&\rTo^{\int^2(f)}\cdots\cr &\rdTo<{i_0}&\dTo~{i_1}&\ldTo~{i_2}&\cdots\cr &&\C\cr \enddiagram Now $\int$, being a left adjoint, preserves colimits, so we have that \diagram \int(\Sets_\V)&\rTo^{\int(f)}&\int^2(\Sets_\V)&\rTo^{\int^2(f)}&\int^3(\Sets_\V)&\rTo^{\int^3(f)}\cdots\cr &\rdTo<{\int(i_0)}&\dTo~{\int(i_1)}&\ldTo~{\int(i_2)}&\cdots\cr &&\int(\C)\cr \enddiagram is also a colimit diagram. That is, $\int(\C) = \dirlim\, \int(D)$. Now if we can show that $\C$ is the colimit of $\int(D)$, then $\C \cong \int(\C)$. Certainly $\C$ together with $i_1,i_2,i_3,\ldots$ is a cocone over $\int(D)$, so there exists a unique $h\colon \int(\C) \to \C$ such that \diagram &\int^{n+1}(\Sets_\V)\cr \ldTo(1,2)<{\int(i_n)}&&\rdTo(1,2)>{i_{n+1}}\cr \int(\C)&\rTo_h&\C\cr \enddiagram commutes for every $n\in \N$. Also $\int(\C)$ together with $\int(i_0) \circ f, \int(i_0),\int(i_1),\int(i_2),\ldots$ is a cocone over $\D$, so there exists a unique $k\colon \C \to \int(\C)$ such that \diagram &\Sets_\V\cr \ldTo(1,2)<{\int(i_0) \circ f}&&\rdTo(1,2)>{i_{0}}\cr \int(\C)&\lTo_k&\C\cr \enddiagram commutes and \diagram &\int^{n+1}(\Sets_\V)\cr \ldTo(1,2)<{\int(i_n)}&&\rdTo(1,2)>{i_{n+1}}\cr \int(\C)&\lTo_k&\C\cr \enddiagram commutes for every $n\in \N$. Notice that $h,k$ are morphisms in the category of cocones over $\int(D)$, and therefore so too is $k\circ h\colon \int(\C)\to\int(\C)$. Hence $kh = \id_{\int(\C)}$ since $\int(\C) = \dirlim\, \int(D)$. But $h,k$ are also morphisms in the category of cocones over $D$ ($h$ is because $h\circ \int(i_0) \circ f = i_1 \circ f = i_0$) so $hk = \id_{\C}$ since $\C = \dirlim\, D$. That is, $h,k$ are an inverse pair, and $\C\cong \int(\C)$.\cqed \end $$I := \pair{\pair{\pfst_{H\times H'}\fst_{H\times H'}}{\pfst_{H\times H'}\snd_{H\times H'}}_H} {\pair{\psnd_{H\times H'}\fst_{H\times H'}}{\psnd_{H\times H'}\snd_{H\times H'}}_{H'}}$$