Matematicamente.it

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:

• esiste un funtore \(\int : [{\cal B}^\text{op}, Set]\to \text{Fib}({\cal B})\)
• esiste un funtore \(\chi : \text{Fib}({\cal B})\to [{\cal B}^\text{op}, Set]\)
• 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]}\)

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)\).

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.

Ho corretto; sì, esatto.

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.

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

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.

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" mor : obj -> obj -> Type; $a \mapsto fa$ significa "$a$ viene mandato in $fa$ da $f$" (formalmente... è difficile scriverlo). Sono segnature diverse, significati diversi.

Beh?