Buona definizione della categoria comma

marco2132k
\( \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
[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
solaàl
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.

kaspar1
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". :roll: Va come traduzione?[/ot]

marco2132k
Sì, ok, a livello colloquiale la cosa non mi infastidisce.

"solaàl":
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' $
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 [...]).

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ì".

marco2132k
@kaspar Guarda CWM, capitolo 1, paragrafi 2 e 8.

kaspar1
Categories for the Working Mathematician? Se intendi questo, non ho questo testo.

solaàl
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.

marco2132k
"kaspar":
Categories for the Working Mathematician? Se intendi questo, non ho questo testo.
C'è una preview su gbooks. Ho anche sentito dire che ci sia in giro un pdf.
[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 :D

kaspar1
[ot]
"solaàl":
[...] Questa cosa però "non type-checka", nel senso che \(f=g\), sia in ZF che in TT [...]
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]

solaàl
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).

kaspar1
Ho inziato un post ieri sera, ma alla fine mi sono stancato e ho cancellato tutto. (E volevo evitare i gremlins :roll:)

"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 :lol:[/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?

solaàl
Poi ti rispondo, ma prima dimmi se di questa cosa ti interessa andare a fondo per perfezionismo o se hai una motivazione altra.

solaàl
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.

kaspar1
"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?

solaàl
Ho capito, volevo solo sapere se la risposta "sì, puoi sempre rendere disgiunta una famiglia di insiemi che non lo erano" è sufficiente.

marco2132k
Io? Sì, certo, ho capito.

Grazie a entrambi ancora!

solaàl
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.

marco2132k
So dove andarmelo a leggere, ma se lo faccio è inutile.

Aiutino?

solaàl
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à?

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

solaàl
Ah, no, quello che dico non c'è nel Mac Lane

Rispondi
Per rispondere a questa discussione devi prima effettuare il login.