Buona definizione della categoria comma
\( \newcommand{\cat}[1]{\mathit{#1}} \)Siano \( \cat C \), \( \cat D \) ed \( E \) tre categorie [1], e si considerino due funtori \( F\colon\cat D\to\cat C \), \( G\colon\cat E\to\cat C \).
Definisco \( F\downarrow G \) come la categoria che ha per oggetti le triple \( (d,e,f) \), dove \( d \) ed \( e \) sono rispettivamente un oggetto di \( \cat D \) e un oggetto di \( \cat E \), ed \( f \) è un morfismo \( f\colon Fd\to Ge \) della categoria \( \cat C \); e per morfismi \( (d,e,f)\to(d^\prime,e^\prime,f) \) le coppie \( (h,k) \), dove \( h\colon d\to d^\prime \), e \( k\colon e\to e^\prime \) sono morfismi rispettivamente di \( \cat D \) e di \( \cat E \), tali che
Per me, una categoria è fatta di due collezioni. Affinché la precedente in linguaggio informale definisca una categoria, quindi, occorre che gli homsets \( \hom_{F\downarrow G}((d,e,f),(d^\prime,e^\prime,f^\prime)) \) siano tutti disgiunti.
Se un \( (h,k) \) appartiene a due homsets \( \hom_{F\downarrow G}((d,e,f),(d^\prime,e^\prime,f^\prime)) \) e \( \hom_{F\downarrow G}((p,q,r),(p^\prime,q^\prime,r^\prime)) \), devono valere \( d = p \), \( e = q \) e le rispettive uguaglianze con l'apice; inoltre, i due diagrammi
devono commutare. Perché, se lo è, è \( f = r \) e \( f^\prime = r^\prime\)?
Definisco \( F\downarrow G \) come la categoria che ha per oggetti le triple \( (d,e,f) \), dove \( d \) ed \( e \) sono rispettivamente un oggetto di \( \cat D \) e un oggetto di \( \cat E \), ed \( f \) è un morfismo \( f\colon Fd\to Ge \) della categoria \( \cat C \); e per morfismi \( (d,e,f)\to(d^\prime,e^\prime,f) \) le coppie \( (h,k) \), dove \( h\colon d\to d^\prime \), e \( k\colon e\to e^\prime \) sono morfismi rispettivamente di \( \cat D \) e di \( \cat E \), tali che
[tex]\xymatrix{Fd\ar[d]_{Fh}\ar[r]^f & Ge\ar[d]^{Gk}\\Fd^\prime\ar[r]_{f^\prime} & Ge^\prime}[/tex]
commuti.Per me, una categoria è fatta di due collezioni. Affinché la precedente in linguaggio informale definisca una categoria, quindi, occorre che gli homsets \( \hom_{F\downarrow G}((d,e,f),(d^\prime,e^\prime,f^\prime)) \) siano tutti disgiunti.
Se un \( (h,k) \) appartiene a due homsets \( \hom_{F\downarrow G}((d,e,f),(d^\prime,e^\prime,f^\prime)) \) e \( \hom_{F\downarrow G}((p,q,r),(p^\prime,q^\prime,r^\prime)) \), devono valere \( d = p \), \( e = q \) e le rispettive uguaglianze con l'apice; inoltre, i due diagrammi
[tex]\xymatrix{Fd\ar[d]_{Fh}\ar[r]^f & Ge\ar[d]^{Gk}\\Fd^\prime\ar[r]_{f^\prime} & Ge^\prime}\qquad\xymatrix{Fd\ar[d]_{Fh}\ar[r]^r & Ge\ar[d]^{Gk}\\Fd^\prime\ar[r]_{r^\prime} & Ge^\prime}[/tex]
devono commutare. Perché, se lo è, è \( f = r \) e \( f^\prime = r^\prime\)?
Risposte
Uso una notazione un po' diversa, cioè scrivo \((F/G)\) per quello che tu chiami \(F\downarrow G\)
Il primo \((h,k)\) è un morfismo \(f\to f'\) in \((F/G)\), e il secondo invece è un morfismo \(r \to r'\) (faccio un abuso di notazione che è innocuo, giusto per non scrivere troppo e farmi capire). Sono diversi, anche se li chiami entrambi \((h,k)\), per un semplice figmento notazionale: formalmente, un morfismo è una terna dominio, codominio, freccia, e quindi vedi che \((h,k) : f \to f'\) e \((h,k) : r \to r'\) sono uguali se e solo se $f=r, f'=r'$.
Quando tu scrivi \((h,k)\) quello che sta intendendo è l'immagine del morfismo dentro la categoria prodotto \(D\times E\): ovviamente esistono due funtori di proiezione sui due fattori della comma (che soddisfano una proprietà universale, ti invito a scoprire quale). Pedanteria vorrebbe che tu scrivessi ogni volta \((h,k) \in (F/G)(etc., \, etc.)\). Ma solitamente, non c'è ambiguità, o meglio: come vedi, un sufficiente grado di formalismo la evita.
Un esempio in cui accade una leggera imprecisione, che i più non notano: prendi un insieme non vuoto \(A\), e considera la funzione \(A \to \mathbb N\) che manda ogni elemento di \(\mathbb N\) in zero; ora considera la funzione \(A \to \mathbb Q\), definita allo stesso modo, costante in zero. Le due funzioni "fanno la stessa cosa", ma sono morfismi diversi, perché -di nuovo- un morfismo \(f : \mathcal C_1\) è una terna \((\text{dom } f, \text{cod } f, f)\).
Un esempio estremo (talmente estremo da non essere molto informativo, se avessi fatto solo questo e non anche quello precedente): se $A$ è vuoto, esiste un'unica funzione \(u : \varnothing \to \mathbb N\); ed esiste un'unica funzione \(v : \varnothing \to \mathbb Z\); ma $u\ne v$, perché sono diversi i loro codomini.
Il primo \((h,k)\) è un morfismo \(f\to f'\) in \((F/G)\), e il secondo invece è un morfismo \(r \to r'\) (faccio un abuso di notazione che è innocuo, giusto per non scrivere troppo e farmi capire). Sono diversi, anche se li chiami entrambi \((h,k)\), per un semplice figmento notazionale: formalmente, un morfismo è una terna dominio, codominio, freccia, e quindi vedi che \((h,k) : f \to f'\) e \((h,k) : r \to r'\) sono uguali se e solo se $f=r, f'=r'$.
Quando tu scrivi \((h,k)\) quello che sta intendendo è l'immagine del morfismo dentro la categoria prodotto \(D\times E\): ovviamente esistono due funtori di proiezione sui due fattori della comma (che soddisfano una proprietà universale, ti invito a scoprire quale). Pedanteria vorrebbe che tu scrivessi ogni volta \((h,k) \in (F/G)(etc., \, etc.)\). Ma solitamente, non c'è ambiguità, o meglio: come vedi, un sufficiente grado di formalismo la evita.
Un esempio in cui accade una leggera imprecisione, che i più non notano: prendi un insieme non vuoto \(A\), e considera la funzione \(A \to \mathbb N\) che manda ogni elemento di \(\mathbb N\) in zero; ora considera la funzione \(A \to \mathbb Q\), definita allo stesso modo, costante in zero. Le due funzioni "fanno la stessa cosa", ma sono morfismi diversi, perché -di nuovo- un morfismo \(f : \mathcal C_1\) è una terna \((\text{dom } f, \text{cod } f, f)\).
Un esempio estremo (talmente estremo da non essere molto informativo, se avessi fatto solo questo e non anche quello precedente): se $A$ è vuoto, esiste un'unica funzione \(u : \varnothing \to \mathbb N\); ed esiste un'unica funzione \(v : \varnothing \to \mathbb Z\); ma $u\ne v$, perché sono diversi i loro codomini.
Magari è una scemenza ma ho notato questa cosa: tra gli assiomi categoriali alcuni (tipo Manetti in Topologia) inseriscono esplicitamente l'assioma «dati degli oggetti \(a\), \(b\), \(c\) e \(d\) se \(a \ne c\) oppure \(b \ne d\), allora \(\hom(a, b) \cap \hom(c, d) = \varnothing\)», altri (ad esempio Leinster in Basic Category Theory) mettono un'osservazione in cui suggerisce che uno può voler assumere questo assioma, altri ancora (come Goldblatt in Topoi) non si preoccupano di questo. Penso, sì, come dice solaàl, che un buon formalismo e contesto evita ambiguità.
[ot]Ho notato anche che non esiste la pagina wiki in italiano corrispondente a "comma category"; in portoghese è "categoria virgula"; quindi penso la resa in italiano sia "categoria virgola".
Va come traduzione?[/ot]
[ot]Ho notato anche che non esiste la pagina wiki in italiano corrispondente a "comma category"; in portoghese è "categoria virgula"; quindi penso la resa in italiano sia "categoria virgola".

Sì, ok, a livello colloquiale la cosa non mi infastidisce.
Un esempio simile, ma meno incasinato, e quello delle categorie slice. Colloquialmente "se \( f\colon c\to x \) e \( g\colon c\to y\), un morfismo \( \kappa\colon f\to g \) è una freccia di \( \mathit C \) che fa commutare [...]"; "davvero", un morfismo \( f\to g \) di \( c/{\mathit C} \) è una tripla \( (f,g,\kappa) \), perché si pone che la collezione delle frecce sia l'unione disgiunta \( \coprod_{\substack{f\colon c\to X\\g\colon c\to Y}}\operatorname{Hom}_{c/\mathit C}(f,g) \).
Questo è lo sfondo di defs su cui ho fatto questa domanda. In altre parole, potevo anche scrivere: "devo prendere l'unione disgiunta delle \( (h,k) \) affinché io abbia una categoria \( F\downarrow G \)?" Mi pare che la risposta sia: "sì".
"solaàl":In CWM, se hai presente, non è richiesto che dominio e codominio facciano parte dei dati di un morfismo (questo mi sembra bello, perché permette definire economicamente una categoria come un grafo orientato equipaggiato con [...]).
formalmente, un morfismo è una terna dominio, codominio, freccia, e quindi vedi che \( (h,k) : f \to f' \) e \( (h,k) : r \to r' \) sono uguali se e solo se $ f=r, f'=r' $
Un esempio simile, ma meno incasinato, e quello delle categorie slice. Colloquialmente "se \( f\colon c\to x \) e \( g\colon c\to y\), un morfismo \( \kappa\colon f\to g \) è una freccia di \( \mathit C \) che fa commutare [...]"; "davvero", un morfismo \( f\to g \) di \( c/{\mathit C} \) è una tripla \( (f,g,\kappa) \), perché si pone che la collezione delle frecce sia l'unione disgiunta \( \coprod_{\substack{f\colon c\to X\\g\colon c\to Y}}\operatorname{Hom}_{c/\mathit C}(f,g) \).
Questo è lo sfondo di defs su cui ho fatto questa domanda. In altre parole, potevo anche scrivere: "devo prendere l'unione disgiunta delle \( (h,k) \) affinché io abbia una categoria \( F\downarrow G \)?" Mi pare che la risposta sia: "sì".
@kaspar Guarda CWM, capitolo 1, paragrafi 2 e 8.
Categories for the Working Mathematician? Se intendi questo, non ho questo testo.
Brevemente: sì, la risposta è che devi farlo, e quando sembra di no, in realtà lo hai fatto ma non ci hai pensato. Se per oggetti diversi i vari hom-set si intersecassero, avresti che \(f : X \to Y = g : A \to B\) sono lo stesso elemento. Questa cosa però "non type-checka", nel senso che \(f=g\), sia in ZF che in TT, presuppone che $f,g$ siano in particolare frecce parallele (e questo è vero anche nei grafi).
Quello che fa Mac Lane in effetti è solo evitare di dire che \(f\) è caratterizzato da source e target; questo semplicemente perché lo è come digrafo.
Tecnicamente, la teoria delle categorie è una teoria a due sorti ("oggetto" e "morfismo"), monadica sui digrafi (questa è una teoria ancor più generale, di nuovo a due sorti: "edge" e "vertex"). Ora, due teorie -essenzialmente- algebriche come queste devono avere lo stesso numero di sorti.
Quello che fa Mac Lane in effetti è solo evitare di dire che \(f\) è caratterizzato da source e target; questo semplicemente perché lo è come digrafo.
Tecnicamente, la teoria delle categorie è una teoria a due sorti ("oggetto" e "morfismo"), monadica sui digrafi (questa è una teoria ancor più generale, di nuovo a due sorti: "edge" e "vertex"). Ora, due teorie -essenzialmente- algebriche come queste devono avere lo stesso numero di sorti.
"kaspar":C'è una preview su gbooks. Ho anche sentito dire che ci sia in giro un pdf.
Categories for the Working Mathematician? Se intendi questo, non ho questo testo.
[ot]Ma non c'è scritto nulla di importante, solo che puoi definire una categoria (come faccio io qui) come un grafo orientato equipaggiato con le funzioni di composizione e identità per ogni oggetto. Spesso, nella pratica, non è "gli oggetti sono gli spazi topologici e i morfismi le continue", ma "un morfismo \( x\to y \) è ...": così stai dicendo, in altre parole, chi sono gli hom-sets della categoria che hai intenzione di definire. Ma per definirla è necessario, intanto, dare le funzioni \( \partial_0,\partial_1:\text{frecce}\to\text{oggetti} \) di dominio e codominio del grafo. Questo non puoi farlo se gli hom-sets non sono tutti disgiunti. Se decidi di dare la definizione di categoria "per homsets" quest'assioma è necessario, affinché la tua definizione sia equivalente alla precedente.[/ot]
Comunque grazie

[ot]
"solaàl":Ma, scusa, il typecheck non si limita a controllare il tipo d'input e il tipo d'output, mentre il predicato d'uguaglianza in ZF* dice anche che gli output sono i medesimi au un dato input? Voglio dire, due funzioni \(f, g : A \to B\) "typecheckano" anche se non è \(f x = g x\) per ogni \(x : A\), il che è invece col predicato d'uguaglianza di ZF*. O no? Questo mi viene in mente se penso alle piccole note teoriche date dal prof a programmazione 1. Poi in ZF* esiste un unico tipo: insieme. Se è troppo lunga come cosa apro un topic apposta casomai, oppure mi puoi indicare dei riferimenti.[/ot]
[...] Questa cosa però "non type-checka", nel senso che \(f=g\), sia in ZF che in TT [...]
Forse "type-checkare" era la parola sbagliata, stavo pensando a $f,g$ come due termini di tipo qualcosa \to qualcos'altro. Se penso in ZF dopo la mezzanotte mi trasformo come i Gremlin.
Cosa sai di teoria dei tipi? Se ricordi come è definito il tipo uguaglianza, esso ha senso per termini dello stesso tipo (e come potrebbe essere altrimenti?) e i due tipi \(A\to B\) e \(X \to Y\) sono uguali solo se \(A=X, B=Y\) (sta nelle formation rule del tipo "morfismo" in \(\lambda\)-calcolo).
Cosa sai di teoria dei tipi? Se ricordi come è definito il tipo uguaglianza, esso ha senso per termini dello stesso tipo (e come potrebbe essere altrimenti?) e i due tipi \(A\to B\) e \(X \to Y\) sono uguali solo se \(A=X, B=Y\) (sta nelle formation rule del tipo "morfismo" in \(\lambda\)-calcolo).
Ho inziato un post ieri sera, ma alla fine mi sono stancato e ho cancellato tutto. (E volevo evitare i gremlins
)
Sì, lo so. E capisco cosa intendi. Ma tieni conto che
Per fare un esempio: "fino a che punto" ha senso dire che sono disgiunti gli hom-sets della categoria \(\mathbf{Par}\) degli insiemi e delle funzioni parziali? Una funzione parziale \(f : A \to B\) è una \(\mathbf{Set}\)-freccia \(f : X \to B\), con \(X \subseteq A\) opportuno. Parlando terra-terra, quante funzioni parziali hanno la stessa "legge" ma non condividono lo stesso dominio, esaurendone solo un pezzo comune? Se vuoi proprio essere integro moralmente fino all'ultimo, potresti volere che le \(\mathbf{Par}\)-frecce siano delle coppie \((f, X)\) con \(X \subseteq \text{dom}f\), hai gli hom-sets disgiunti e sei contento. Ma questo è vendersi l'anima ad un diavolo in bottiglia, se permetti. La domanda che sorge spontanea è: la tua integrità morale è in grado di reggere a lungo? (D'altra chi lo è?)
Per di più si è anche sfigati:
L'idea delle protocategorie è interessante e la filosofia di fondo è conciliante per logici, teorici degli insiemi e categoristi[nota]Per esperienza so quanto possano essere "talebani" i primi due, non che esponenti dei terzi scherzino
[/nota]. Senza tenere conto che: dire che due hom-sets sono disgiunti vuol dire che per ogni coppia di frecce uno proveniente da uno e l'altro dall'altro, si ha che sono diversi. Il predicato di uguaglianza/disuguaglianza tra frecce che non "type-checkano" non ha senso, l'istanziazione della (dis)uguaglianza te la scordi. Tu ci credi che ha senso intersecare collezioni astratte?

"marco2132k":
Per me, una categoria è fatta di due collezioni. Affinché la precedente in linguaggio informale definisca una categoria, quindi, occorre che gli homsets \( \hom_{F\downarrow G}((d,e,f),(d^\prime,e^\prime,f^\prime)) \) siano tutti disgiunti. [...]
[... Un altro post ...]
[...] è necessario, intanto, dare le funzioni \(\partial_0, \partial_1 : \text{frecce} \to \text{oggetti}\) di dominio e codominio del grafo. Questo non puoi farlo se gli hom-sets non sono tutti disgiunti. Se decidi di dare la definizione di categoria "per hom-sets" quest'assioma è necessario, affinché la tua definizione sia equivalente alla precedente. [...]
Sì, lo so. E capisco cosa intendi. Ma tieni conto che
"https://ncatlab.org/nlab/show/category#equivalence_between_the_two_definitions":18oifwqq:
[...] In ordinary category theory [...] one rarely worries about whether the hom-sets are disjoint [...]
Per fare un esempio: "fino a che punto" ha senso dire che sono disgiunti gli hom-sets della categoria \(\mathbf{Par}\) degli insiemi e delle funzioni parziali? Una funzione parziale \(f : A \to B\) è una \(\mathbf{Set}\)-freccia \(f : X \to B\), con \(X \subseteq A\) opportuno. Parlando terra-terra, quante funzioni parziali hanno la stessa "legge" ma non condividono lo stesso dominio, esaurendone solo un pezzo comune? Se vuoi proprio essere integro moralmente fino all'ultimo, potresti volere che le \(\mathbf{Par}\)-frecce siano delle coppie \((f, X)\) con \(X \subseteq \text{dom}f\), hai gli hom-sets disgiunti e sei contento. Ma questo è vendersi l'anima ad un diavolo in bottiglia, se permetti. La domanda che sorge spontanea è: la tua integrità morale è in grado di reggere a lungo? (D'altra chi lo è?)
Per di più si è anche sfigati:
"sempre nella stessa sezione di prima":
[...] Moreover, categorical constructions do not "naturally" preserve disjointness of hom-sets [...]
L'idea delle protocategorie è interessante e la filosofia di fondo è conciliante per logici, teorici degli insiemi e categoristi[nota]Per esperienza so quanto possano essere "talebani" i primi due, non che esponenti dei terzi scherzino

Poi ti rispondo, ma prima dimmi se di questa cosa ti interessa andare a fondo per perfezionismo o se hai una motivazione altra.
Volevo dire solo una cosa, alla fine:
Formalmente \(\sf Par\) ha per oggetti gli span in \(\sf Set\)
\[
\begin{CD}
D @>f>> Y \\
@ViVV @.\\
X
\end{CD}
\] dove \(i : D\subseteq X\) è il dominio di $f$. Quindi non c'è rischio di confondere morfismi con "stesso" src e trg, che hanno domini diversi e sono funzioni diverse, perché rappresentati come span sono diversi.
Tanto più che esiste un'equivalenza di categorie \({\sf Par}\cong {\sf Set}_\bullet\), in cui a RHS c'è la categoria degli insiemi puntati e funzioni che preservano il punto. Puoi quindi rappresentare ogni funzione parziale \(f : X \to Y\) come una funzione tra insiemi puntati \(X\sqcup 1 \to Y\sqcup 1\), e queste ultime hanno un'ovvia nozione di "essere uguali" e "essere in hom-set disgiunti"
Ad ogni uso pratico, però, puoi sempre prendere una famiglia \(J\)-parametrica di insiemi e assicurare che questi siano disgiunti; perciò faccio fatica a vedere il problema.
Formalmente \(\sf Par\) ha per oggetti gli span in \(\sf Set\)
\[
\begin{CD}
D @>f>> Y \\
@ViVV @.\\
X
\end{CD}
\] dove \(i : D\subseteq X\) è il dominio di $f$. Quindi non c'è rischio di confondere morfismi con "stesso" src e trg, che hanno domini diversi e sono funzioni diverse, perché rappresentati come span sono diversi.
Tanto più che esiste un'equivalenza di categorie \({\sf Par}\cong {\sf Set}_\bullet\), in cui a RHS c'è la categoria degli insiemi puntati e funzioni che preservano il punto. Puoi quindi rappresentare ogni funzione parziale \(f : X \to Y\) come una funzione tra insiemi puntati \(X\sqcup 1 \to Y\sqcup 1\), e queste ultime hanno un'ovvia nozione di "essere uguali" e "essere in hom-set disgiunti"
Ad ogni uso pratico, però, puoi sempre prendere una famiglia \(J\)-parametrica di insiemi e assicurare che questi siano disgiunti; perciò faccio fatica a vedere il problema.
"solaàl":
[...] perciò faccio fatica a vedere il problema.
marco2132k ha iniziato una discussione intitolata "Buona definizione della categoria comma" in cui si premurava, forse eccessivamente, se o meno gli hom-sets fossero disgiunti. Keep calm, volevo comunicargli sostanzialmente, le cose interessanti da fare con le categorie sono certamente altre. E lo sai meglio di me. Se proprio ci tiene, comunque può ricorrere a vari trick formali per ottenere questo scopo, o no?
Ho capito, volevo solo sapere se la risposta "sì, puoi sempre rendere disgiunta una famiglia di insiemi che non lo erano" è sufficiente.
Io? Sì, certo, ho capito.
Grazie a entrambi ancora!
Grazie a entrambi ancora!
Potrebbe ora interessarti scoprire qual è la proprietà universale della categoria comma.
Ah già, per quanto riguarda la sua traduzione io preferisco pensare sia "comma" anche in italiano.
Ah già, per quanto riguarda la sua traduzione io preferisco pensare sia "comma" anche in italiano.
So dove andarmelo a leggere, ma se lo faccio è inutile.
Aiutino?
Aiutino?
La comma è terminale da qualche parte, ma la proprietà universale è 2-dimensionale (cioè coinvolge anche l'esistenza e unicità di trasformazioni naturali).
Dove lo saresti andato a leggere, per curiosità?
Dove lo saresti andato a leggere, per curiosità?
Ok, tra un po' ci provo.
Penso che la risposta sia l'esercizio 5 qui (secondo risultato; non riesco a linkarlo), ma devo ancora leggere quello che c'è intorno.
Penso che la risposta sia l'esercizio 5 qui (secondo risultato; non riesco a linkarlo), ma devo ancora leggere quello che c'è intorno.
Ah, no, quello che dico non c'è nel Mac Lane