## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeNov 13th 2012
• (edited Nov 13th 2012)

The following I can prove via the Yoneda lemma, but I suspect that there is a more intrinsic and more meaningful proof, can anyone help me?

So: for $f : X \to Y$ a morphism in some locally cartesian closed category $\mathbf{H}$ and for $A,B \in \mathbf{H}_{/X}$ I am concerned with the statement that there exists a natural morphism

$\prod_{f} \left[ A, B \right] \to \left[ \sum_f A, \sum_f B \right] \,.$

This is clear. For some value of clear. One way to get there is to consider any $U \in \mathbf{H}_{/Y}$ and compute

\begin{aligned} \mathbf{H}_{/Y}( U, \prod_f [A,B] ) & \simeq \mathbf{H}_{/X}( f^* U, [A,B] ) \\ & \simeq \mathbf{H}_{/X}(f^* U \times A, B) \\ & \stackrel{}{\to} \mathbf{H}_{/Y}( \sum_f( f^* U \times A ), \sum_f B ) \\ & \stackrel{Frob.Rec.}{\simeq} \mathbf{H}_{/Y}( U \times \sum_f A , \sum_f B ) \\ & \simeq \mathbf{H}_{/Y}(U, \sum_f A , \sum_f B) \end{aligned} \,.

Since this is natural in $U$, the claimed morphism follows from the Yoneda lemma.

But there must be a nice way to do this without going through Yoneda. How do you prove this in type theory, for instance?

• CommentRowNumber2.
• CommentAuthorZhen Lin
• CommentTimeNov 13th 2012
• (edited Nov 13th 2012)

Let $y$ be a variable of type $Y$. Let $\lambda x \colon X(y) . \, \phi_{y,x}$ be an element of the fibre of the LHS over $y$. Your morphism sends this to the map $\lambda \langle a, x \rangle \colon \sum_{x \colon X(y)} A(x) . \, \langle \phi_{y,x} (a), x \rangle$ in the fibre of the RHS over $y$.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeNov 13th 2012

Thanks, I see. That’s obvious enough, now that you say it. I really need to start getting more fluent with this. I am a clear case here of being able to read the language easily, but bad at speaking it freely.

On the other hand, that formulation is lacking, at least in typographical appearance, the nice structure of the expression $\prod_f [A,B] \to [\sum_f A, \sum_f B]$, which rhymes with $f^*[C,D] \simeq [f^* C, f^* D]$. Is there something one can do about that?

By the way, just for the record I added a note on this at internal hom – Examples – In slice categories.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeNov 13th 2012
• (edited Nov 14th 2012)

By the way, I came to this when polishing the discussion at Hamiltonian vector field – on n-plectic smooth ∞-groupoids. Previously I had discussed the canonical morphism

$\mathbf{QuantMorph}(X,\omega) \to \mathbf{Aut}(X)$

from the quantomorphism $\infty$-group of a prequantized $\infty$-stack $X$ to $X$ only somewhat more informally. The above question comes form thinking about how to formalize this nicely. The $\infty$-group of Hamiltonian symplectomorphisms of $(X,\omega)$ is the $\infty$-image of this map.

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeNov 13th 2012
• (edited Nov 14th 2012)

I guess another way of looking at it is like this: we have a composite

$A \to [[A, B], B] \stackrel{[counit, unit]}{\to} [f^\ast \prod_f [A, B], f^\ast \sum_f B] \cong f^\ast [\prod_f [A, B], \sum_f B]$

(the rhyme you were after, perhaps) which transforms to

$\sum_f A \to [\prod_f [A, B], \sum_f B]$

or equivalently to

$\prod_f [A, B] \to [\sum_f A, \sum_f B].$
• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeNov 14th 2012
• (edited Nov 14th 2012)

Thanks, Todd! I have moved that here to the entry, too, just for the record.

(Strictly speaking one should add some discussion that this indeed coincides with the previous construction above. But I’ll call it quits for tonight. In the previous construction I can easily see that remark 4 is true. In the construction which you just gave I’d need to think about that, maybe. (?))

• CommentRowNumber7.
• CommentAuthorTodd_Trimble
• CommentTimeNov 14th 2012

Well, I just took your Yoneda-based proof and ploddingly translated it into the proof in #5 (which I later shortened slightly, to make just three displayed lines instead of four). So while my method was stolid and pedestrian, I am reasonably confident it gives the same construction. (But please do check!)

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeNov 14th 2012
• (edited Nov 14th 2012)

(Still here after all…)

I don’t doubt it! I just thought in the entry where I now have the two constructions consecutively, one should eventually add a remark on why they are in fact equivalent. (Of course it’s probably impossible to construct a canonical such morphism which is not equivalent to all the other canonical constructions! :-)

But for something else: next I want to find a nice canonical proof of the fact that for $\nabla \colon \sum_f \nabla \to X$ given we have a fiber sequence

$\Omega_\nabla [\sum_f \nabla,X] \to \prod_{f} \left[\nabla, \nabla \right] \to \left[ \sum_f \nabla , \sum_f \nabla \right]$

(now explicitly working in an $\infty$-topos). But unless this comes to me while I am brushing my teeth now, this will have to wait until tomorrow… ;-)

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeNov 14th 2012

Zhen, do you really write $\langle a,x\rangle : \sum_{x:X} A(x)$ with $a:A(x)$? I’ve always seen dependent pairs ordered like $\langle x,a\rangle$.

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeNov 14th 2012
• (edited Nov 14th 2012)

Here is the proof of the fiber sequence in #8 (it’s elementary, of course).

Compute the homotopy fiber of $\prod_f[\nabla,\nabla] \to [\sum_f \nabla, \sum_f \nabla]$ in the $\infty$-Yoneda-picture of #1 for each $U$ separately. Since $\mathbf{H}_{/Y}(U,-)$ preserves pullbacks, the result follows generally if it follows naturally for each $U$.

Then use that by the standard formula for the hom-space in a slice $\infty$-category the morphism

$\mathbf{H}_{/X}(f^* U \times \nabla, \nabla) \to \mathbf{H}_{/Y}( U \times \sum_f \nabla, \sum_f \nabla )$

is the left vertical morphism in the $\infty$-pullback

$\array{ \mathbf{H}_{/X}(f^* U \times \nabla, \nabla) &\to& * \\ \downarrow && \downarrow^{\mathrlap{\vdash f^* U \times \nabla}} \\ \mathbf{H}_{/Y}( U \times \sum_f \nabla, \sum_f \nabla ) &\stackrel{\nabla \circ (-)}{\to}& \mathbf{H}_{/Y}(U \times \sum_f \nabla, X) } \,.$

So by the pasting law its further $\infty$-fiber is indeed

$\array{ \mathbf{H}_{/Y}(U,\Omega_\nabla [\sum_f \nabla, X]) &\to& \mathbf{H}_{/X}(f^* U \times \nabla, \nabla) &\to& * \\ \downarrow && \downarrow && \downarrow^{\mathrlap{\vdash f^* U \times \nabla}} \\ * &\stackrel{}{\to}& \mathbf{H}_{/Y}( U \times \sum_f \nabla, \sum_f \nabla ) &\stackrel{\nabla \circ (-)}{\to}& \mathbf{H}_{/Y}(U \times \sum_f \nabla, X) } \,.$
• CommentRowNumber11.
• CommentAuthorZhen Lin
• CommentTimeNov 14th 2012

@Mike: I don’t work on type theory, so I’m just inventing my own notations here…

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeNov 14th 2012

I suppose in HoTT you can derive the fiber sequence of #8 easily in few lines.