Dopo averci sbattuto un poco la testa mi è uscito un diagrammino quasi carino, ma ho paura di non aver checkato qualcosa.
Riassumendo, ho considerato tre frecce $h: A \to B$, $f: C \to D$ e $g: C' \to D'$, e i due quadrati commutativi:
\[
\begin{array}[c]{ccc}
C&\stackrel{a_0}{\longrightarrow}&A\\
\big\downarrow\scriptstyle{f}&&\big\downarrow\scriptstyle{h}\\
D&\stackrel{a_1}{\longrightarrow}&B
\end{array}
\]
e
\[
\begin{array}[c]{ccc}
C'&\stackrel{b_0}{\longrightarrow}&A\\
\big\downarrow\scriptstyle{g}&&\big\downarrow\scriptstyle{h}\\
D'&\stackrel{b_1}{\longrightarrow}&B
\end{array}
\]
sono andatx allora a costruire i pullback in Set di $a_0$ e $b_0$ e di $a_1$ e $b_1$, ottenendo quindi
\( P_0=\{ (c, c') \in C \times C' : a_0 (c) = b_0(c') \} \)
\( P_1 = \{ (d, d') \in D \times D' : a_1 (d) = b_1(d') \} \)
A questo punto concludo che la freccia $p: P_0 \to P_1$ tale che $a_1 @ p = g @ b'_1 $ e $b'_1 @ p = f @ b'_0$ (e rispettivi quadrati commutativi, mi danno il pullback che cercavo.
(che per ogni altra freccia $x:X_0 \to X_1$ esista unico eccetera, segue dal fatto che ho considerato dei pullback. nel diagramma* sta cosa mj pare chiara)
Se qualcuno ha voglia di controllare che io non abbia scritto cose troppo demenziali, vi ringrazio!
* il diagramma:
- Codice:
\begin{tikzcd}[row sep=scriptsize, column sep=scriptsize]
& & & C \ar[d, blue, "f"] \ar[drr, blue] & & \\
X_0 \ar[urrr, bend left, dotted] \ar[drrr, bend right, dotted] \ar[d, "x"] \ar[r, dashed] & P_0 \ar[rrrr, phantom, ">", very near start] \ar[d, "p"] \ar[urr] & & D \ar[drr, blue] & & A \ar[d, blue, "h"] \\
X_1 \ar[urrr, bend left, dotted] \ar[drrr, bend right, dotted] \ar[r, dashed] & P_1 \ar[rrrr, phantom, ">", very near start] \ar[urr] \ar[drr] & & C' \ar[from=ull, crossing over] \ar[urr, blue, crossing over] \ar[d, blue, "g"] & & B \\
& & & D' \ar[urr, blue] & &
\end{tikzcd}
