A question about fibrations of simplicial sets and their fibers

I couldn't think of a title for this, but here we go:

Fix $p:S\rightarrow T$, a left fibration of simplicial sets, and an edge $f:\Delta^1 \rightarrow T$. Let $t$ be the first vertex of $f$, and $t'$ be the second vertex.
We name the induced map, $q: S^{\Delta^1}\rightarrow S^{\{1 \}}\times_{T^{\{1 \}}} T^{\Delta^1}$.

Now let $X$ be the simplicial set of sections of the projection $S\times_T \Delta^1\rightarrow \Delta^1$, where the pullback is taken with respect to the map $p:S\rightarrow T$ and the fixed edge $f:\Delta^1 \rightarrow T$.

More notation: We'll denote by $S_{t'}$ the fiber $S \times_T \Delta^0$ where $\Delta^0 \rightarrow T$ is given by the inclusion of the vertex $t'$ and $S\rightarrow T$ is given again by p. We give a fiber $q':X \rightarrow S_{t'}$ of $q$ over the edge $f$ (This is about where I stop understanding what's going on).

What we'd like to show is: $q$ and $q'$ have the same fibers over points of $S^{\{1 \}}\times_{T^{\{1 \}}} T^{\Delta^1}$ where the second projection is the edge f. Remember that exponentiation denotes the internal Hom.

The problem is this simplicial set of sections. What are its maps out, and why do they naturally go to $S_{t'}$ and agree with q? I feel like the key to this is understanding how the exponential is mapping into the pullback, but it's not really clear to me how that should work.

This fact is stated in HTT by Lurie in the proof of proposition 2.1.3.1, but I don't really see how it's obvious.

A link to the relevant proof/page: http://books.google.com/books?id=CTe68E8wK4QC&lpg=PP1&ots=o8qYDiX4mt&dq=lurie%20higher%20topos%20theory&pg=PA67#v=onepage&q=&f=false

Update: "Work" I've done thusfar: $$\ \ \matrix{&S^{\Delta^1}_f &\to & S^{\Delta^1}& \cr &\downarrow &Pb &\downarrow \cr S_{t'}\cong &L_f & \to & L & \to & S^{\{1\}} & \cr &\downarrow &Pb&\downarrow&Pb&\downarrow p \cr &\Delta^{0} & \to & T^{\Delta^1} & \to & T^{\{1\}} \cr &&f&&d_1}\ \$$

Note that $d_1$ denotes the face map at the vertex 1. Also, $L:= S^{\{1 \}}\times_{T^{\{1 \}}} T^{\Delta^1}$, and The point here is that it should be "morally" the same to give a pullback of $\Delta^1\to T \leftarrow S$ as giving a pullback $\Delta^0\to T^{\Delta^1} \leftarrow S^{\Delta^1}$ with respect to the edge f. So we'd like to show that $X$, the simplicial set of sections of the projection noted before is somehow isomorphic to $S^{\Delta^1}_f$, since this shows that $q$ and $q'$ agree where they're needed to. So what I'm struggling with at this point is showing this last idea.

-
Why are the question and only answer community wiki? Both seem pretty focused and non-wiki-esque to me. – Chris Schommer-Pries Jan 19 '10 at 14:26
Because I made like 30 revisions to it. – Harry Gindi Jan 19 '10 at 14:38
Now that I look, 15 revisions. – Harry Gindi Jan 19 '10 at 14:48
Since this page is the first result on google for "simplicial set of sections", the remaining details for the proof are available at: ncatlab.org/nlab/show/weak+factorization+system , which at the bottom of the page, proves that all morphisms with the right lifting property are stable under pullback. – Harry Gindi Jan 20 '10 at 7:23

1 Answer

I've got to agree with you; it's not the best-written proof in HTT. Let me go through it glacially slowly (for my own sake!) to see if I can write something that will help clarify the role of $X$.

Let me write $Map(U,V)$ instead of $V^U$. I find it easier to parse on the internet.

First, what is our $X$? It's the simplicial set of sections of $S\times_T\Delta^1\to\Delta^1$, that is, it is the fiber product

$Map(\Delta^1,S\times_T\Delta^1)\times_{Map(\Delta^1,\Delta^1)}\Delta^0$, where $\Delta^0$ maps in by inculsion of $id$. So (since $Map(\Delta^1,-)$ is a right adjoint) we get: $$X=Map(\Delta^1,S\times_T\Delta^1)\times_{Map(\Delta^1,\Delta^1)}\Delta^0=Map(\Delta^1,S)\times_{Map(\Delta^1,T)}Map(\Delta^1,\Delta^1)\times_{Map(\Delta^1,\Delta^1)}\Delta^0$$ $$=Map(\Delta^1,S)\times_{Map(\Delta^1,T)}\Delta^0$$ where $\Delta^0$ is mapping in by inclusion $f$.

Now we've got our map $$q:Map(\Delta^1,S)\to Map(\{1\},S)\times_{Map(\{1\},T)}Map(\Delta^1,T),$$ whose fibers over $f$ we seek. That is, we just include $$S_{t'}=Map(\{1\},S)\times_{Map(\{1\},T)}\Delta^0\to Map(\{1\},S)\times_{Map(\{1\},T)}Map(\Delta^1,T)$$ (which is itself the pullback of $f:\Delta^0\to Map(\Delta^1,T)$ along the projection, of course) and we pull back to get $q'$.

So the result is a pullback of a pullback. (If I knew how, I'd draw the two pullback squares here.) The composite pullback is the pullback of $f:\Delta^0\to Map(\Delta^1,T)$ along $Map(\Delta^1,S)\to Map(\Delta^1,T)$. But this is what we called $X$. So our result is a map $q':X\to S_{t'}$, and its fiber over any vertex of $S_{t'}$ must coincide with the fiber over the corresponding vertex of $Map(\{1\},S)\times_{Map(\{1\},T)}Map(\Delta^1,T)$, since that will be a pullback of a pullback as well.

Edit (Harry): I typed up the final version of the diagram. If the letters aren't explained, you can deduce what they are just by either looking at Clark's argument or just tracing the pullbacks. Every square is a pullback, so everything is very easy to deal with. $$\ \ \matrix{ X&\cong&S^{\Delta^1}_f &\to &Y^{\Delta^1}&\to& S^{\Delta^1}& \cr &\searrow&\downarrow &Pb &\downarrow&Pb&\downarrow \cr L_f&\cong &S_{t'} & \to &L'&\to& L & \to & S^{\{1\}} & \cr &&\downarrow &Pb&\downarrow&Pb&\downarrow&Pb&\downarrow p \cr &&\Delta^{0} & \to &(\Delta^1)^{\Delta^1} &\to& T^{\Delta^1} & \to & T^{\{1\}} \cr &&&id&&(f)^{\Delta^1}&&d_1}\ \$$

-
Oh hell, the curly braces around the 1 don't show up! Hopefully the readability hasn't suffered too much. – Clark Barwick Jan 19 '10 at 14:22
I fixed them since it's community wiki, and I awarded you the bounty. Thank you very much. Just for your reference, if you put backticks around your dollar signs, it escapes them from markdown, so they don't often get as screwed up. If you see a line overflowing of the page, if you just give it a few lines of room, it'll force it back into order. – Harry Gindi Jan 19 '10 at 14:45
Do you know of a good place to find definitions of things like that? Or is it something you just get used to with more experience in the subject? – Harry Gindi Jan 19 '10 at 14:58
Thank you very much! I'm not really sure where one can find a systematic treatment of things like "the simplicial set of sections"; I mostly picked it up by spending a lot of my time confused and on occasion reverse-engineering the definitions. Usually, if it's not in HTT or Goerss-Jardine or Curtis's Advances paper, I had to guess at the definition. Maybe someone else has other references? – Clark Barwick Jan 19 '10 at 20:11
Do you know the full title of Curtis's paper? – Harry Gindi Jan 19 '10 at 22:17