Tanti funtori nel lemma di Yoneda
\( \newcommand{\cat}[1]{\mathbf{#1}} \)\( \newcommand{\op}{\mathrm{op}} \)\( \newcommand{\Set}{\cat{Set}} \)Ciao! Se \( c \) e \( c^\prime \) sono oggetti della categoria \( \cat C \), il loro hom-set è \( \cat C(c,c^\prime) \); se \( \cat C \) e \( \cat D \) sono categorie, la categoria dei funtori \( \cat C\to\cat D \) è \( \cat D^{\cat C} \).
Sia \( \cat C \) una categoria (localmente piccola), sia \( c\in \cat C \) un oggetto di \( \cat C \), e sia \( F\colon \cat C\to \Set \) un funtore di \( \cat C \) verso la categoria degli insiemi. Il lemma di Yoneda è spesso enunciato dicendo che la biiezione
\[
\begin{aligned}
\eta_{c,F}\colon \Set^{\cat C}(\cat C(c,{-}),F) &\xrightarrow{{\cong}} F(c)\\
\alpha &\mapsto \alpha_c(1_c)
\end{aligned}
\] è naturale in \( c \) e in \( F \). Esplicitamente, "naturale in \( c \)" significa che, considerati il funtore composto \( \Set^{\cat C}(y({-}),F)\colon \cat C\to \Set \) dei funtori \( y\colon \cat C^\op\to\Set^{\cat C} \) curried del bifuntore \( \cat C({-},{-})\colon \cat C^\op \times \cat C\to \Set \) e \( \Set^{\cat C}({-},F)\colon (\Set^{\cat C})^\op\to \Set \) rappresentato da \( F \), la famiglia \( \eta_{{-},F} = \left(\eta_{c,F}\right)_{c\in\cat C} \), a funtore \( F\colon \cat C\to \Set \) fissato, è una naturale tra questi ragazzi. In modo simile si esplicita "naturale in \( F \) (a \( c \) fissato)".
Seguendo un argomento imperscrutabile, "[...] the Yoneda lemma asserts that evaluating at the representing object's identity morphism defines a natural isomorphism"[1] dal bifuntore \( \Set^{\cat C}(y({-}),{-}) \) di \( \cat C\times \Set^{\cat C} \) in \( \Set \), al funtore di valutazione \( \mathrm{ev}\colon \cat C\times \Set^{\cat C}\to \Set \) che mappa
\[
\begin{CD}
(c,F) @. F(c)\\
@V{(f,\beta)}VV @VV{F^\prime(f)\circ\beta_c}V\\
(c^\prime,F^\prime) @. F^\prime(c^\prime)
\end{CD}
\]
Guardando la firma di \( \eta_{c,F} \) sarei stato in grado di costruire direttamente i due bifuntori di cui sopra. Quello che cerco di capire, invece, è che relazione ci sia tra due coppie di funtori "come quelli che ho esplicitati riguardo la naturalità in \( c \)/in \( F \)", e un bifuntore "come quello sopra".
La domanda più precisa, ma che fa schifo lo stesso, è: esiste una nozione precisa di appiccicare due trasformazioni naturali come quella tra \( \Set^{\cat C}(y({-}),F) \) e \( \Set^{\cat C}({-},F) \) e quella tra [...] e [...] del lemma di Yoneda per ottenere una naturale come \( \Set^{\cat C}(y({-}),{-})\Rightarrow\mathrm{ev} \)?
Il problema qui è che se \( F_1,G_1\colon \cat C_1\to \cat D_1 \) e \( F_2,G_2\colon \cat C_2\to \cat D_2 \), e \( \alpha\colon F_1\Rightarrow G_1 \) e \( \beta\colon F_2\Rightarrow G_2 \), allora posso sì dire che \( \alpha\times\beta \) (definita in modo ovvio) è una naturale tra \( F_1\times F_2 \) e \( G_1\times G_2 \); ma i funtori precedenti in un certo senso "collassano il dominio di arrivo" in \( \Set \).
[1] E. Riehl, Category theory in context, paragrafo 2.2.
Sia \( \cat C \) una categoria (localmente piccola), sia \( c\in \cat C \) un oggetto di \( \cat C \), e sia \( F\colon \cat C\to \Set \) un funtore di \( \cat C \) verso la categoria degli insiemi. Il lemma di Yoneda è spesso enunciato dicendo che la biiezione
\[
\begin{aligned}
\eta_{c,F}\colon \Set^{\cat C}(\cat C(c,{-}),F) &\xrightarrow{{\cong}} F(c)\\
\alpha &\mapsto \alpha_c(1_c)
\end{aligned}
\] è naturale in \( c \) e in \( F \). Esplicitamente, "naturale in \( c \)" significa che, considerati il funtore composto \( \Set^{\cat C}(y({-}),F)\colon \cat C\to \Set \) dei funtori \( y\colon \cat C^\op\to\Set^{\cat C} \) curried del bifuntore \( \cat C({-},{-})\colon \cat C^\op \times \cat C\to \Set \) e \( \Set^{\cat C}({-},F)\colon (\Set^{\cat C})^\op\to \Set \) rappresentato da \( F \), la famiglia \( \eta_{{-},F} = \left(\eta_{c,F}\right)_{c\in\cat C} \), a funtore \( F\colon \cat C\to \Set \) fissato, è una naturale tra questi ragazzi. In modo simile si esplicita "naturale in \( F \) (a \( c \) fissato)".
Seguendo un argomento imperscrutabile, "[...] the Yoneda lemma asserts that evaluating at the representing object's identity morphism defines a natural isomorphism"[1] dal bifuntore \( \Set^{\cat C}(y({-}),{-}) \) di \( \cat C\times \Set^{\cat C} \) in \( \Set \), al funtore di valutazione \( \mathrm{ev}\colon \cat C\times \Set^{\cat C}\to \Set \) che mappa
\[
\begin{CD}
(c,F) @. F(c)\\
@V{(f,\beta)}VV @VV{F^\prime(f)\circ\beta_c}V\\
(c^\prime,F^\prime) @. F^\prime(c^\prime)
\end{CD}
\]
Guardando la firma di \( \eta_{c,F} \) sarei stato in grado di costruire direttamente i due bifuntori di cui sopra. Quello che cerco di capire, invece, è che relazione ci sia tra due coppie di funtori "come quelli che ho esplicitati riguardo la naturalità in \( c \)/in \( F \)", e un bifuntore "come quello sopra".
La domanda più precisa, ma che fa schifo lo stesso, è: esiste una nozione precisa di appiccicare due trasformazioni naturali come quella tra \( \Set^{\cat C}(y({-}),F) \) e \( \Set^{\cat C}({-},F) \) e quella tra [...] e [...] del lemma di Yoneda per ottenere una naturale come \( \Set^{\cat C}(y({-}),{-})\Rightarrow\mathrm{ev} \)?
Il problema qui è che se \( F_1,G_1\colon \cat C_1\to \cat D_1 \) e \( F_2,G_2\colon \cat C_2\to \cat D_2 \), e \( \alpha\colon F_1\Rightarrow G_1 \) e \( \beta\colon F_2\Rightarrow G_2 \), allora posso sì dire che \( \alpha\times\beta \) (definita in modo ovvio) è una naturale tra \( F_1\times F_2 \) e \( G_1\times G_2 \); ma i funtori precedenti in un certo senso "collassano il dominio di arrivo" in \( \Set \).
[1] E. Riehl, Category theory in context, paragrafo 2.2.
Risposte
Non è che hai risolto in privato, e a noi dici niente, eh...
Comunque sì: appiccicare insieme i pezzi è una parte essenziale, se non il sugo del lavoro per la dimostrazione del Lemma. È questo che stai chiedendo, no? Come cucire le parti?

Comunque sì: appiccicare insieme i pezzi è una parte essenziale, se non il sugo del lavoro per la dimostrazione del Lemma. È questo che stai chiedendo, no? Come cucire le parti?
\( \newcommand{\cat}[1]{\mathbf{#1}} \)\( \newcommand{\op}{\mathrm{op}} \)\( \newcommand{\Set}{\cat{Set}} \)Ho risolto! Nella naturalità della biiezione
\[
\eta_{c,F}\colon \Set^{\cat C}(\cat C(c,{-}),F) \xrightarrow{{\cong}} F(c)
\] in \( c\in\cat C \) e in \( F\colon \cat C\to \Set \) entrano in gioco rispettivamente la
\[
\eta_{{-},F}\colon \Set^{\cat C}(y({-}),F)\Rightarrow F
\] tra i due funtori \( \cat C\to \Set \), e la
\[
\eta_{c,{-}}\colon \Set^{\cat C}(y(c),{-})\Rightarrow \mathrm{ev}_c
\] tra i funtori \( \Set^{\cat C}\to \Set \). Ora, si vede che i due LHS sono rispettivamente le immagini di un \( F\colon \cat C\to \Set \) e di un \( c\in\cat C \) nei curried de
\[
\Set(y({-}),{-})\colon \cat C\times \Set^{\cat C}\to \Set
\] rispettivamente nelle biiezioni
\[
\cat{Cat}(\cat C\times \Set^{\cat C},\Set)\cong \cat{Cat}(\cat C,\Set^{\Set^{\cat C}})\qquad \cat{Cat}(\cat C\times \Set^{\cat C},\Set)\cong \cat{Cat}(\cat \Set^{\cat C},\Set)
\] E i due RHS sono la stessa cosa, però per il bifuntore di valutazione. E -che è quello che mi mancava- anche le naturali curriano, quindi \( \eta_{{-},F} \) e l'altra vengono da \( \eta_{{-},{-}} \). Modulo problemi di stazza.
\[
\eta_{c,F}\colon \Set^{\cat C}(\cat C(c,{-}),F) \xrightarrow{{\cong}} F(c)
\] in \( c\in\cat C \) e in \( F\colon \cat C\to \Set \) entrano in gioco rispettivamente la
\[
\eta_{{-},F}\colon \Set^{\cat C}(y({-}),F)\Rightarrow F
\] tra i due funtori \( \cat C\to \Set \), e la
\[
\eta_{c,{-}}\colon \Set^{\cat C}(y(c),{-})\Rightarrow \mathrm{ev}_c
\] tra i funtori \( \Set^{\cat C}\to \Set \). Ora, si vede che i due LHS sono rispettivamente le immagini di un \( F\colon \cat C\to \Set \) e di un \( c\in\cat C \) nei curried de
\[
\Set(y({-}),{-})\colon \cat C\times \Set^{\cat C}\to \Set
\] rispettivamente nelle biiezioni
\[
\cat{Cat}(\cat C\times \Set^{\cat C},\Set)\cong \cat{Cat}(\cat C,\Set^{\Set^{\cat C}})\qquad \cat{Cat}(\cat C\times \Set^{\cat C},\Set)\cong \cat{Cat}(\cat \Set^{\cat C},\Set)
\] E i due RHS sono la stessa cosa, però per il bifuntore di valutazione. E -che è quello che mi mancava- anche le naturali curriano, quindi \( \eta_{{-},F} \) e l'altra vengono da \( \eta_{{-},{-}} \). Modulo problemi di stazza.