Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 12 of 12
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?
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$.
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.
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.
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].$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. (?))
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!)
(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… ;-)
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$.
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) } \,.$@Mike: I don’t work on type theory, so I’m just inventing my own notations here…
I suppose in HoTT you can derive the fiber sequence of #8 easily in few lines.
1 to 12 of 12