Fibrazioni discrete su \({\cal B}\)
Un funtore \(G : {\cal E} \to {\cal B}\) è una fibrazione discreta se per ogni $f : B\to GE$ in \(\cal B\) esiste un'unica freccia $v : E'\to E$ tale che $Gv=f$.
Un morfismo di fibrazioni discrete tra \(G : {\cal E}\to {\cal B}\) e \(G' : {\cal E}'\to {\cal B}\) è un funtore \(H : {\cal E}\to {\cal E}'\) tale che $G'\circ H =G$.
Mostrare che questo definisce una categoria \(\text{Fib}({\cal B})\) delle fibrazioni discrete su \(\mathcal B\).
Mostrare che il funtore \(\text{src} : {\cal B}/B\to{\cal B}\), che manda una freccia $f : X\to B$ nel suo dominio $X$, è una fibrazione discreta. (definizione di \({\cal B}/B\))
Mostrare che la categoria \(\text{Fib}({\cal B})\) così definita è equivalente alla categoria dei funtori \(F : {\cal B}^\text{op}\to Set\), ovvero che:
Un morfismo di fibrazioni discrete tra \(G : {\cal E}\to {\cal B}\) e \(G' : {\cal E}'\to {\cal B}\) è un funtore \(H : {\cal E}\to {\cal E}'\) tale che $G'\circ H =G$.
Mostrare che questo definisce una categoria \(\text{Fib}({\cal B})\) delle fibrazioni discrete su \(\mathcal B\).
Mostrare che il funtore \(\text{src} : {\cal B}/B\to{\cal B}\), che manda una freccia $f : X\to B$ nel suo dominio $X$, è una fibrazione discreta. (definizione di \({\cal B}/B\))
Mostrare che la categoria \(\text{Fib}({\cal B})\) così definita è equivalente alla categoria dei funtori \(F : {\cal B}^\text{op}\to Set\), ovvero che:
[*:31bupqkh] esiste un funtore \(\int : [{\cal B}^\text{op}, Set]\to \text{Fib}({\cal B})\) [/*:m:31bupqkh]
[*:31bupqkh] esiste un funtore \(\chi : \text{Fib}({\cal B})\to [{\cal B}^\text{op}, Set]\)[/*:m:31bupqkh]
[*:31bupqkh] esistono degli isomorfismi \(\int\circ\chi\cong \text{id}_{\text{Fib}({\cal B})}\) e \(\chi\circ\int \cong \text{id}_{[{\cal B}^\text{op}, Set]}\)[/*:m:31bupqkh][/list:u:31bupqkh]
Mostrare che dato \(F : {\cal B}^\text{op}\to Set\) c'è una biiezione tra l'insieme $FB$ e l'insieme di tutte le mappe di fibrazioni discrete tra la fibrazione discreta \(\text{src} : {\cal B}/B\to {\cal B}\) e \(\chi(F)\).
Risposte
Sono un po' arrugginito. Solo per essere sicuro se ho capito bene: \(E, E'\in \mathrm{ob}(\mathcal{E})\), \(B\in \mathrm{ob}(\mathcal{B})\) e \(f\in \hom(\mathcal{B})\). Inoltre il nome dell'unica freccia su \(\mathcal{E}\) è \(v\) (hai usato la lettera senza definirla). Giusto?
Ora non ho tempo di mettermici, magari provo a risolverlo stasera.
Ora non ho tempo di mettermici, magari provo a risolverlo stasera.
Ho corretto; sì, esatto.
[tex]\xymatrix{
\mathcal E \ar[dr]_G & & \mathcal E^\prime \ar[dl]^{G^\prime} \\
& \mathcal B &
}[/tex]
\mathcal E \ar[dr]_G & & \mathcal E^\prime \ar[dl]^{G^\prime} \\
& \mathcal B &
}[/tex]
Forse intendevi \(H \colon \mathcal E \mapsto \mathcal E'\) se vuoi che sia \(G' \circ H = G\). Oppure è \(G \circ H = G'\)?
Sì, non rende falso il risultato (viene solo controvariante l'equivalenza), ma non era voluto quindi correggo.
Bozza, quindi forse con molte sviste o peggio per la velocità con cui tutto è stato scritto... Nella versione definitiva sarà tutto visibile direttamente.
[ot]Per ora faccio vedere la definizione di \(\operatorname{Fib}(\cal B)\). Gli oggetti sono le fibrazioni discrete di codominio \(\cal B\) e i morfismi i funtori tra queste. Faccio vedere ora che ci sono delle composizioni, ovvero delle funzioni che mandano una coppia di funtori tra fibrazioni discrete su \(\cal B\) in uno e un solo funtore tra fibrazioni discrete su \(\cal B\) (con i funtori scelti in modo da poterli comporre, ovviamente). Se \(H\) è un morfismo da \(G \colon \cal E \mapsto \cal B\) a \(G' \colon \cal E' \mapsto \cal B\) e \(H'\) è un morfismo da \(G' \colon \cal E' \mapsto \cal B\) a \(G \colon \cal E'' \mapsto \cal B\), allora pure \(H' \circ H\) lo è: infatti \(G = G' \circ H = G'' \circ (H' \circ H)\).
E \(H' \circ H\) è anche l'unico a far commutare questo diagramma, perchè, date due fibrazioni discrete, il funtore tra di loro è unico per la definizione stessa di fibrazione discreta (dimostrazione in spoiler, a breve..., sempre se non ho preso un abbaglio
). La proprietà associativa è quella dei funtori in generale, le identità pure.[/ot]
[ot]Per ora faccio vedere la definizione di \(\operatorname{Fib}(\cal B)\). Gli oggetti sono le fibrazioni discrete di codominio \(\cal B\) e i morfismi i funtori tra queste. Faccio vedere ora che ci sono delle composizioni, ovvero delle funzioni che mandano una coppia di funtori tra fibrazioni discrete su \(\cal B\) in uno e un solo funtore tra fibrazioni discrete su \(\cal B\) (con i funtori scelti in modo da poterli comporre, ovviamente). Se \(H\) è un morfismo da \(G \colon \cal E \mapsto \cal B\) a \(G' \colon \cal E' \mapsto \cal B\) e \(H'\) è un morfismo da \(G' \colon \cal E' \mapsto \cal B\) a \(G \colon \cal E'' \mapsto \cal B\), allora pure \(H' \circ H\) lo è: infatti \(G = G' \circ H = G'' \circ (H' \circ H)\).
[tex]\xymatrix{
\cal E \ar[dr]_G \ar[rr]^H & & \cal E^\prime \ar[dl]^{G^\prime} \ar[dd]^{H^\prime} \\
& \cal B & \\
& & \cal E^\prime^\prime \ar[ul]^{G^\prime^\prime}
}[/tex]
\cal E \ar[dr]_G \ar[rr]^H & & \cal E^\prime \ar[dl]^{G^\prime} \ar[dd]^{H^\prime} \\
& \cal B & \\
& & \cal E^\prime^\prime \ar[ul]^{G^\prime^\prime}
}[/tex]
E \(H' \circ H\) è anche l'unico a far commutare questo diagramma, perchè, date due fibrazioni discrete, il funtore tra di loro è unico per la definizione stessa di fibrazione discreta (dimostrazione in spoiler, a breve..., sempre se non ho preso un abbaglio

Affinché \(\text{Fib}(\mathcal B)\) sia una categoria, non è necessario che tra ogni coppia di oggetti ci sia un solo morfismo.
Non solo queste sono categorie molto particolari (si chiamano "gruppoidi massimalmente connessi"), e perciò questa richiesta non rientra tra gli assiomi di categoria, ma è anche falso che \(\text{Fib}(\mathcal B)\) sia un tale gruppoide: in base all'ultimo teorema che vi chiedo di dimostrare, se scegli un funtore \(F : \mathcal B \to Set\) tale che \(\text{card } FX > 1\) (come puoi immaginare, ce ne sono a bizzeffe), allora ci sono esattamente \(\text{card } FX\) morfismi tra la fibrazione discreta \(\text{src} : \mathcal B/X \to \mathcal B\) e la fibrazione discreta \(\chi(F) \to \mathcal B\).
Puoi per esempio prendere come $F$ il funtore costante sull'insieme \(\{g,t,e\}\) (gatto, topo, elefante: non manca più nessuno), e divertirti a trovare esattamente tre morfismi di fibrazione discreta tra src e $\chi(F)$ (e già che ci sei... chi è $\chi(F)$ quando $F$ è un funtore costante?).
C'è poi una nota terminologica: tu scrivi $f : A \mapsto B$; questo è sintatticamente sbagliato, perché l'uso che è comune praticamente a tutti è di usare, invece, $\to$; il simbolo infisso \(\mapsto\), invece, è riservato ad indicare la regola che, fissato $f : A \to B$, manda $a : A$ in $fa : B$.
Non solo queste sono categorie molto particolari (si chiamano "gruppoidi massimalmente connessi"), e perciò questa richiesta non rientra tra gli assiomi di categoria, ma è anche falso che \(\text{Fib}(\mathcal B)\) sia un tale gruppoide: in base all'ultimo teorema che vi chiedo di dimostrare, se scegli un funtore \(F : \mathcal B \to Set\) tale che \(\text{card } FX > 1\) (come puoi immaginare, ce ne sono a bizzeffe), allora ci sono esattamente \(\text{card } FX\) morfismi tra la fibrazione discreta \(\text{src} : \mathcal B/X \to \mathcal B\) e la fibrazione discreta \(\chi(F) \to \mathcal B\).
Puoi per esempio prendere come $F$ il funtore costante sull'insieme \(\{g,t,e\}\) (gatto, topo, elefante: non manca più nessuno), e divertirti a trovare esattamente tre morfismi di fibrazione discreta tra src e $\chi(F)$ (e già che ci sei... chi è $\chi(F)$ quando $F$ è un funtore costante?).
C'è poi una nota terminologica: tu scrivi $f : A \mapsto B$; questo è sintatticamente sbagliato, perché l'uso che è comune praticamente a tutti è di usare, invece, $\to$; il simbolo infisso \(\mapsto\), invece, è riservato ad indicare la regola che, fissato $f : A \to B$, manda $a : A$ in $fa : B$.
Pensavo di far vedere che ci sono delle composizioni, che sono delle funzioni, quindi una coppia di morfismi viene mandata in uno e un solo morfismo. Mmmmh... a me sembrava che in questo caso specifico il morfismo tra due oggetti è unico. Dopo controllo... (Dove sono ora non riesco a trovare mezzo foglio, come è possibile?)
Il resto appena posso lo risolvo con calma.
La nota terminologica non l'ho capita. Il codice LaTeX che sta sotto è \mapsto, per questo uso quel simbolo.
Il resto appena posso lo risolvo con calma.
La nota terminologica non l'ho capita. Il codice LaTeX che sta sotto è \mapsto, per questo uso quel simbolo.
date due fibrazioni discrete, il funtore tra di loro è unico per la definizione stessa di fibrazione discreta
Questo è falso e ti ho spiegato perché (sebbene con un argomento ex post, ma certamente saprai trovare i tre morfismi che intendo). Da ciò è naturale dedurre che c'è un solo morfismo in ogni hom-set tra due fibrazioni.
La nota terminologica è questa: $f : A \to B$ significa "c'è un morfismo tra $A$ e $B$" (formalmente: $\to$ è il costruttore del tipo "morfismo" [inline]mor : obj -> obj -> Type[/inline]; $a \mapsto fa$ significa "$a$ viene mandato in $fa$ da $f$" (formalmente... è difficile scriverlo). Sono segnature diverse, significati diversi.
Beh?

\(\newcommand\B{\mathcal B} \newcommand\src{\text{src}}\)
Mmmmh... diciamo che la difficoltà qua sta nella lettura e nella comprensione di quello che sta scritto e dei ruoli. Allora, diciamo inanzitutto che gli oggetti di \(\B/B\) sono morfismi di \(\B\) con codominio \(B\) e che un morfismo da \(s \colon X \to B\) a \(t \colon Y \to B\) è un morfismo \(u \colon X \to Y\) in \(\B\) per cui \(s=tu\).
Il funtore \(\src \colon \B/B \to \B\) agisce così:
"caulacau":
Mostrare che il funtore \(\src : \B/B\to\B\), che manda una freccia $f : X\to B$ nel suo dominio $X$, è una fibrazione discreta.
Mmmmh... diciamo che la difficoltà qua sta nella lettura e nella comprensione di quello che sta scritto e dei ruoli. Allora, diciamo inanzitutto che gli oggetti di \(\B/B\) sono morfismi di \(\B\) con codominio \(B\) e che un morfismo da \(s \colon X \to B\) a \(t \colon Y \to B\) è un morfismo \(u \colon X \to Y\) in \(\B\) per cui \(s=tu\).
Il funtore \(\src \colon \B/B \to \B\) agisce così:
[*:1yr9ycez] manda \(X \to B\) in \(X\)[/*:m:1yr9ycez]
[*:1yr9ycez] manda un morfismo \((X \to B) \to (Y \to B)\) in \(X \to Y\) dimenticando che \[(X \to B)=(Y \to B)\circ(X \to Y)\][/*:m:1yr9ycez][/list:u:1yr9ycez]
in effetti \(\src\) è amnestico.
Veniamo al dunque. \(\src\) è una fibrazione discreta perché per ogni morfismo \[f \colon Q \to \src(P \to B)\,,\] (vale a dire \(f \colon Q \to P\)), esiste una e una sola freccia \(u \colon R \to (P \to B)\) in \(\B/B\): preso \(R\) come morfismo \(Q \to B\), il morfismo \(v\) è praticamente \(f\) con la proprietà che \(\src\) dimentica.
[ot]Avete mai provato a fare una cosa del genere?
\( \newcommand\B{\mathcal B} \)[/ot]
Bene,e il resto?

Fra un po' arriva...

\(
\newcommand\fib{\operatorname{Fib}}
\newcommand\B{\mathcal{B}}
\newcommand\E{\mathcal{E}}
\newcommand\Set{\mathbf{Set}}
\newcommand\op[1]{#1^\text{op}}
\newcommand\id[1]{\text{id}_#1}
\newcommand\obj{\operatorname{obj}}
\newcommand\el{\operatorname{el}}
\)Piccolo disclaimer. L'esercizio ha richiesto tanto lavoro, in questo periodo particolare della mia vita incompatibile con il tempo rimasto. Quando posso (e non potrei), nelle dimostrazioni e nelle sottigliezze compio delle ellissi abbastanza vistose, se non delle omissioni: questo perché, nolente, questo aspetto tecnico è passato in secondo piano rispetto all'idea generale e alle costruzioni. Ciò non toglie che io possa aver perso il controllo delle mie costruzioni: in tal caso mi scuso, ma è positivo per voi (non mi riferisco a caulacau, che ovviamente mastica queste cose) se siete stati in grado di indivduare errori, bravi
; a testimoniare anche che c'è un po' di vita qui dentro, oltre ai soliti quattro gatti.
Non credo neppure di ritornare a dedicarmi a questo mega-esercizio prima di tanto tempo, per problemi, impegni e... incominciano i corsi all'università per me a breve.
... allora, dividiamo in tre parti l'esercizio:
Costruzione del funtore \(\chi \colon \fib(\B) \to [\op\B,\Set]\). Data una fibrazione discreta in \(F \colon \E \to \B\) in \(\fib(\B)\), costruisco il funtore \(\chi(F) \colon \op\B \to \Set\) in questo modo:
\newcommand\fib{\operatorname{Fib}}
\newcommand\B{\mathcal{B}}
\newcommand\E{\mathcal{E}}
\newcommand\Set{\mathbf{Set}}
\newcommand\op[1]{#1^\text{op}}
\newcommand\id[1]{\text{id}_#1}
\newcommand\obj{\operatorname{obj}}
\newcommand\el{\operatorname{el}}
\)Piccolo disclaimer. L'esercizio ha richiesto tanto lavoro, in questo periodo particolare della mia vita incompatibile con il tempo rimasto. Quando posso (e non potrei), nelle dimostrazioni e nelle sottigliezze compio delle ellissi abbastanza vistose, se non delle omissioni: questo perché, nolente, questo aspetto tecnico è passato in secondo piano rispetto all'idea generale e alle costruzioni. Ciò non toglie che io possa aver perso il controllo delle mie costruzioni: in tal caso mi scuso, ma è positivo per voi (non mi riferisco a caulacau, che ovviamente mastica queste cose) se siete stati in grado di indivduare errori, bravi

Non credo neppure di ritornare a dedicarmi a questo mega-esercizio prima di tanto tempo, per problemi, impegni e... incominciano i corsi all'università per me a breve.
... allora, dividiamo in tre parti l'esercizio:
"caulacau":
Mostrare che la categoria \(\text{Fib}({\cal B})\) così definita è equivalente alla categoria dei funtori \(F : {\cal B}^\text{op}\to Set\), ovvero che:
[*:1onaicav] esiste un funtore \(\int : [{\cal B}^\text{op}, Set]\to \text{Fib}({\cal B})\) [/*:m:1onaicav]
[*:1onaicav] esiste un funtore \(\chi : \text{Fib}({\cal B})\to [{\cal B}^\text{op}, Set]\)[/*:m:1onaicav]
[*:1onaicav] esistono degli isomorfismi \(\int\circ\chi\cong \text{id}_{\text{Fib}({\cal B})}\) e \(\chi\circ\int \cong \text{id}_{[{\cal B}^\text{op}, Set]}\)[/*:m:1onaicav][/list:u:1onaicav]
Costruzione del funtore \(\chi \colon \fib(\B) \to [\op\B,\Set]\). Data una fibrazione discreta in \(F \colon \E \to \B\) in \(\fib(\B)\), costruisco il funtore \(\chi(F) \colon \op\B \to \Set\) in questo modo:
[*:1onaicav] ogni oggetto \(x\) di \(\B\) viene mandato in \((\chi(F))(x):=\{u \in \obj(\E) \mid F(u)=x\}\), oggetto di \(\Set\)[/*:m:1onaicav]
[*:1onaicav] ogni morfismo \(\op f \colon b \to a\) di \(\op\B\) viene spedito nel morfismo \((\chi(F))(f) \colon (\chi(F))(a) \to (\chi(F))(b)\), determinabile univocamente dal fatto che \(F \colon \E \to \B\) sia una fibrazione discreta (come? spoiler che segue.)[/*:m:1onaicav][/list:u:1onaicav]
Abbiamo appena visto come \(\chi\) agisce sugli oggetti, adesso vediamo cosa fa coi morfismi: ad ogni morfismo di funtori \(H \colon (\E' \overset{G}{\to} \B) \to (\E \overset{F}{\to} \B)\) si fa corrispondere la trasformazione naturale \(\alpha \colon \chi(F) \to \chi(G)\) per cui il seguente diagramma commuta
[tex]\xymatrix{
(\chi(F))(x) \ar[r]^{\alpha_x} & (\chi(G))(x) \\
(\chi(F))(y) \ar[r]_{\alpha_y} \ar^{(\chi(F))(f)} & (\chi(G))(y) \ar_{(\chi(G))(f)}
}[/tex]
(\chi(F))(x) \ar[r]^{\alpha_x} & (\chi(G))(x) \\
(\chi(F))(y) \ar[r]_{\alpha_y} \ar^{(\chi(F))(f)} & (\chi(G))(y) \ar_{(\chi(G))(f)}
}[/tex]
per ogni \(f \colon x \to y\) di \(\op\B\). Abbiamo già visto \((\chi(-))(f)\), con \(f\) morfismo, e \(\alpha\) è fornito da \(H\).
Parte I finita! Anzi no! La costruzione fatta qui ovviamente funziona quando \(\B\) è piccola. E qualora non lo sia?
Costruzione del funtore \(\int \colon [\op\B,\Set] \to \fib(\B)\). Facciamo che questa è abbastanza ardua per arrivarci da solo


Come pima su un funtore \(G \colon \op\B \to \Set\), oggetto di \([\op\B,\Set]\), costruiamo una fibrazione discreta, oggetto di \(\fib(\B)\); in particolare \(G\) viene mandato nel funtore sbadato \(\int G \colon \el_G (\B) \to \B\) così fatto:
[*:1onaicav] manda \((x,a)\) in \(x\)[/*:m:1onaicav]
[*:1onaicav] manda \((x,a) \to (y,b)\) in \(x \to y\)[/*:m:1onaicav][/list:u:1onaicav]Si può provare che \(\int G\) è una fibrazione discreta su \(\B\).
Vediamo che fa \(\int G\) coi morfismi. Va da trasformazioni naturali
[tex]\xymatrix{
\mathcal{B}^\text{op} \ar@/^1pc/[r]^G="g1" \ar@/_1pc/[r]_{G^\prime}="g2" & \mathbf{Set}
\ar@{=>}"g1";"g2" ^\alpha
}[/tex]
a funtori di fibrazioni discrete \(H \colon \int G \to \int G'\): il tutto sta nel capire quanto è contorta la situzione, facile, no? \mathcal{B}^\text{op} \ar@/^1pc/[r]^G="g1" \ar@/_1pc/[r]_{G^\prime}="g2" & \mathbf{Set}
\ar@{=>}"g1";"g2" ^\alpha
}[/tex]

La quiete dopo la tempesta. Se siete arrivati qui, avrete bestemmiato e imprecato moltissimo. Comunque è semplice (a patto di calarsi nei menadri delle costruzioni e capire i ruoli degli oggetti in gioco) constatare i due isomorfismi.
Fiù... A pensare che manca il gran finale
"caulacau":
Mostrare che dato \(F : {\cal B}^\text{op}\to Set\) c'è una biiezione tra l'insieme $FB$ e l'insieme di tutte le mappe di fibrazioni discrete tra la fibrazione discreta \(\text{src} : {\cal B}/B\to {\cal B}\) e \(\chi(F)\).

"Indrjo Dedej":
\(
\newcommand\fib{\operatorname{Fib}}
\newcommand\B{\mathcal{B}}
\newcommand\E{\mathcal{E}}
\newcommand\Set{\mathbf{Set}}
\newcommand\op[1]{#1^\text{op}}
\newcommand\id[1]{\text{id}_#1}
\newcommand\obj{\operatorname{obj}}
\newcommand\el{\operatorname{el}}
\)[*:32253r89] ogni oggetto \(x\) di \(\B\) viene mandato in \((\chi(F))(x):=\{u \in \obj(\E) \mid F(u)=x\}\), oggetto di \(\Set\)[/*:m:32253r89][/list:u:32253r89]
La fibra di \(x\) mediante \(F\) sarà, in generale, una categoria; ma è la proprietà di fibrazione discreta ad assicurare che sia una categoria discreta; riempi(te) i dettagli di questa affermazione. (Giustificando la nomenclatura "fibrazione discreta", da un lato; e dall'altro, constatando che la definizione di \(\chi(F)\) è proprio \(x\mapsto F^\leftarrow(x)\), se con tale simbolo si intende l'insieme degli oggetti che $F$ manda in \(x\), e l'insieme dei morfismi che $F$ manda in \(\text{id}_x\)).
[*:32253r89] ogni morfismo \(\op f \colon b \to a\) di \(\op\B\) viene spedito nel morfismo \((\chi(F))(f) \colon (\chi(F))(a) \to (\chi(F))(b)\), determinabile univocamente dal fatto che \(F \colon \E \to \B\) sia una fibrazione discreta (come? spoiler che segue.)[/*:m:32253r89][/list:u:32253r89]
C'è un ingarbugliamento; \(\chi(F)(f)\) è una funzione tra due insiemi, precisamente le fibre sopra dominio e codominio di \(f\); dovresti scrivere meglio dove un elemento di \(F^\leftarrow a\) viene mappato da \(\chi(F)(f)\) in un elemento di \(F^\leftarrow b\).
Abbiamo appena visto come \(\chi\) agisce sugli oggetti, adesso vediamo cosa fa coi morfismi: ad ogni morfismo di funtori \(H \colon (\E' \overset{G}{\to} \B) \to (\E \overset{F}{\to} \B)\) si fa corrispondere la trasformazione naturale \(\alpha \colon \chi(F) \to \chi(G)\) per cui il seguente diagramma commuta
[tex]\xymatrix{
(\chi(F))(x) \ar[r]^{\alpha_x} & (\chi(G))(x) \\
(\chi(F))(y) \ar[r]_{\alpha_y} \ar^{(\chi(F))(f)} & (\chi(G))(y) \ar_{(\chi(G))(f)}
}[/tex]
per ogni \(f \colon x \to y\) di \(\op\B\). Abbiamo già visto \((\chi(-))(f)\), con \(f\) morfismo, e \(\alpha\) è fornito da \(H\).
C'è certamente modo di scriverlo meglio. Per esempio, potresti dire che se \(E\in G^\leftarrow X\) allora \(HE\in F^\leftarrow X\)... e poi, la naturalità va dimostrata, non solo scritta

Parte I finita! Anzi no! La costruzione fatta qui ovviamente funziona quando \(\B\) è piccola. E qualora non lo sia?Si può trasportare tutto a un universo più grande, dove la categoria \([{\cal B}^\text{op}, \Set]\) è legittima, e dove lo è anche \(\el\).
Costruzione del funtore \(\int \colon [\op\B,\Set] \to \fib(\B)\). Facciamo che questa è abbastanza ardua per arrivarci da solo: studiando altre cose mi sono imbattuto in questa pagina [nota]Come non averci pensato prima? Pensavo di fare in un altro modo, ma solo vivoli cechi...[/nota]. Cerco di riorganizzare un po' le cose e completare (non che ci sia tanto da raccontare ancora...), anche per altri che leggono, ignorano[nota]Ignorante non è un'offesa, eh...[/nota], ma cercano di capire un minimo, altrimenti sono discorsi tra i soliti quattro gatti e non è divertente...
Come pima su un funtore \(G \colon \op\B \to \Set\), oggetto di \([\op\B,\Set]\), costruiamo una fibrazione discreta, oggetto di \(\fib(\B)\); in particolare \(G\) viene mandato nel funtore sbadato \(\int G \colon \el_G (\B) \to \B\) così fatto:
[*:32253r89] manda \((x,a)\) in \(x\)[/*:m:32253r89]
[*:32253r89] manda \((x,a) \to (y,b)\) in \(x \to y\)[/*:m:32253r89][/list:u:32253r89]Si può provare che \(\int G\) è una fibrazione discreta su \(\B\).
Certo, si può. Quindi fallo

Bravo, comunque. Meno male che qualcuno c'è.