Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2012
   • (edited Nov 13th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThe 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?

   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?

2. • CommentRowNumber2.
   • CommentAuthorZhen Lin
   • CommentTimeNov 13th 2012
   • (edited Nov 13th 2012)
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexLet $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$.

   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$.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, 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](http://ncatlab.org/nlab/show/internal+hom#ExampleInSliceCategories)_.

   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.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2012
   • (edited Nov 14th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexBy the way, I came to this when polishing the discussion at _[Hamiltonian vector field -- on n-plectic smooth ∞-groupoids](http://ncatlab.org/nlab/show/Hamiltonian+vector+field#OnNPlecticInfinityGroupoids)_. 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeNov 13th 2012
   • (edited Nov 14th 2012)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI 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].$$

   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].$$
6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeNov 14th 2012
   • (edited Nov 14th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, Todd! I have moved that [here to the entry](http://ncatlab.org/nlab/show/internal+hom#ExampleInSliceCategories), 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](http://ncatlab.org/nlab/show/internal+hom#RememberingTopMorphismInHomInSlice) is true. In the construction which you just gave I'd need to think about that, maybe. (?))

   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. (?))

7. • CommentRowNumber7.
   • CommentAuthorTodd_Trimble
   • CommentTimeNov 14th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexWell, 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!)

   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!)

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeNov 14th 2012
   • (edited Nov 14th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItex(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... ;-)

   (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… ;-)

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeNov 14th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexZhen, 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$.

   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$.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2012
    • (edited Nov 14th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHere 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) } \,. $$

    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) } \,.$$
11. • CommentRowNumber11.
    • CommentAuthorZhen Lin
    • CommentTimeNov 14th 2012
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItex@Mike: I don't work on type theory, so I'm just inventing my own notations here...

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

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexI suppose in HoTT you can derive the fiber sequence of #8 easily in few lines.

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