Where else has Proposition B1.3.17 in the Elephant been proved? - MathOverflow most recent 30 from http://mathoverflow.net2013-05-22T20:59:26Zhttp://mathoverflow.net/feeds/question/104640http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/104640/where-else-has-proposition-b1-3-17-in-the-elephant-been-provedWhere else has Proposition B1.3.17 in the Elephant been proved?Chuck2012-08-13T20:43:02Z2012-08-13T23:05:46Z
<p>(I asked the same question <a href="http://math.stackexchange.com/questions/181425/where-else-has-proposition-b1-3-17-in-the-elephant-been-proved" rel="nofollow">here</a> and got some helpful comments, but thought I'd re-ask in case I get a more direct response.)</p>
<p>This is a sort of reference request. Proposition B1.3.17 in Johnstone's Elephant reads:</p>
<p><strong>Proposition 1.3.17</strong> Let $\mathcal{S}$ and $\mathcal{T}$ be categories with pullbacks, $F \colon \mathcal{S} \rightarrow \mathcal{T}$ a functor having a right adjoint $R$, and $\Pi \colon \mathcal{C} \rightarrow \mathcal{T}$ a fibration. Then $F^* \Pi \colon F^* \mathcal{C} \rightarrow \mathcal{S}$ satisfies any comprehension scheme satisfied by $\Pi$.</p>
<p>I find the proof Johnstone offers very confusing (partly because it's very elliptical.) Does anyone know where this was originally proved? I haven't found the result in Benabou's writing (unless it's in the paper in French, referenced as [101] in Johnstone, which I cannot read) nor anywhere else. Is there another version of this proof in print? Or was Johnstone the first to prove this result in this generality?</p>
<p>Furthermore, if someone patient among you actually looks at the proof, could you possibly clarify this for me: What is the notation $\mathcal{T}^{\pi_0\mathcal{D}}$ supposed to describe ($\pi_0 \mathcal{D}$ is described as the "set of connected components of $\mathcal{D}$"? At first I suspected it was (collections of) connected diagrams in $\mathcal{T}$ - i.e. I interpreted as something like a component-wise $[\pi_0 \mathcal{D},\mathcal{T}]$ where the diagrams are sent to $\mathcal{T}$ via $\Pi$ (because of what Johnstone says right before the diagram, namely that "applying $\Pi$ to objects and morphisms of Rect($\mathcal{D},\mathcal{C}$) yields a functor Rect($\mathcal{D},\mathcal{C}) \rightarrow \mathcal{T}^{\pi_0 \mathcal{D}}$"- but then I cannot really make sense of what he says at the last sentence of the first full paragraph of pg. 278, for which interpreting it as the $\pi_0 \mathcal{D}$-fold product of $\mathcal{T}$ makes sense. Basically, what categories are we dealing with on the bottom square of the diagram on pg. 277?</p>