Functorial choice of pullbacks in a locally cartesian closed $(\infty,1)$-category - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-19T19:22:18Z http://mathoverflow.net/feeds/question/82578 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/82578/functorial-choice-of-pullbacks-in-a-locally-cartesian-closed-infty-1-categor Functorial choice of pullbacks in a locally cartesian closed $(\infty,1)$-category Guillaume Brunerie 2011-12-03T20:23:33Z 2011-12-04T23:30:04Z <p>In a locally cartesian closed category $\mathcal C$, for every map $f:A\to B$, there is an associated pullback functor $f^* : \mathcal C/B \to\mathcal C/A$. Moreover, if $g:B\to C$, the two functors $(g\circ f)^*$ and <code>$f^*\circ g^*$</code> are <em>canonically isomorphic</em>, but they have no reason to be "equal". Even in the category of sets, the usual choice of pullbacks is only functorial up to isomorphism (see <a href="http://www.springerlink.com/content/5077x3h92151072u/fulltext.pdf" rel="nofollow">this paper of Hofmann</a>)</p> <p>This gives a pseudo functor from $\mathcal C^\mathrm{op}$ to $\mathcal{Cat}$. The fact that this is only a pseudo functor and not a functor causes some problems when trying to interpret dependent type theory in locally cartesian closed categories (see for example the previous paper of Hofmann, or <a href="http://archive.numdam.org/ARCHIVE/DIA/DIA_1990__23_/DIA_1990__23__43_0/DIA_1990__23__43_0.pdf" rel="nofollow">this paper of Curien</a>).</p> <p>I was wondering what happens when you pass to $(\infty,1)$-categories. Intuitively, the fact that pullback are only functorial up to isomorphism should not be a problem anymore, because $(\infty,1)$-functors are also only functorial up to isomorphism anyway.</p> <p>So my question is, <strong>if $\mathcal C$ is a <a href="http://ncatlab.org/nlab/show/locally+cartesian+closed+%28infinity,1%29-category" rel="nofollow">locally cartesian closed $(\infty,1)$-category</a>, does there always exists a functorial choice of pullbacks?</strong> (by which I mean an $(\infty,1)$-functor from $\mathcal C^\mathrm{op}$ to $(\infty,1)\mathcal{Cat}$ sending objects to slice categories and morphisms to pullback functors)</p> http://mathoverflow.net/questions/82578/functorial-choice-of-pullbacks-in-a-locally-cartesian-closed-infty-1-categor/82654#82654 Answer by Dylan Wilson for Functorial choice of pullbacks in a locally cartesian closed $(\infty,1)$-category Dylan Wilson 2011-12-04T22:20:27Z 2011-12-04T22:20:27Z <p>Okay so I think the answer is that, yes, you can define such a functor. The main reasons are as follows:</p> <ol> <li>Pullbacks themselves are only defined up to coherent homotopy equivalence.</li> <li>Compositions in an infinity category (like $Cat_\infty$) are only defined up to coherent equivalence.</li> <li>Any two good choices of a "pullback functor" $f^*: \mathcal{C}/A \rightarrow \mathcal{C}/B$ must be equivalent.</li> </ol> <p>I'm sure there's some highly general proposition in HTT where Lurie proves something where this result is a special case, but I couldn't seem to find such a thing so I've written down some words that I think constitute a (rather messy) proof... I think a lot of what I say is probably unnecessary, so I'll try to clean it up a bit later:</p> <p><a href="http://washington.academia.edu/DylanWilson/Teaching/29740/Functoriality_of_pullbacks_in_infty-categories" rel="nofollow">write up</a></p> <p>(also- it'd be really nice if I could actually just post documents here since I don't really have a webpage, I just sort of made one up on some site that I'm not even sure everyone can see...? Is there a way to do this?)</p> http://mathoverflow.net/questions/82578/functorial-choice-of-pullbacks-in-a-locally-cartesian-closed-infty-1-categor/82658#82658 Answer by Rune Haugseng for Functorial choice of pullbacks in a locally cartesian closed $(\infty,1)$-category Rune Haugseng 2011-12-04T23:30:04Z 2011-12-04T23:30:04Z <p>The easiest thing to do is probably to appeal to the equivalence between functors $\mathcal{C}^{\text{op}} \to \text{Cat}_{\infty}$ and Cartesian fibrations over $\mathcal{C}$. Roughly speaking, a Cartesian fibration $\mathcal{E} \to \mathcal{C}$ corresponds to a functor that sends $c \in \mathcal{C}$ to the fibre <code>$\mathcal{E}_{c}$</code> of the fibration at $c$ and a morphism $f \colon c \to d$ in $\mathcal{C}$ to a functor <code>$f^* \colon \mathcal{E}_{d} \to \mathcal{E}_{c}$</code> that takes an object $x$ in <code>$\mathcal{E}_{d}$</code> to the source of a Cartesian arrow over $f$ with target $x$. This functor is unique up to a contractible space of choices.</p> <p>The "evaluation at 1" functor $\text{Fun}(\Delta^1, \mathcal{C}) \to \mathcal{C}$ is a Cartesian fibration precisely when $\mathcal{C}$ has pullbacks - a "Cartesian arrow" in $\text{Fun}(\Delta^1, \mathcal{C})$ is the same things as a pullback diagram - so the corresponding functor sends $c \in \mathcal{C}$ to the fibre <code>$\mathcal{C}_{/c}$</code> of this map and a morphism $f$ in $\mathcal{C}$ to "pullback by $f$".</p>