“魔法交换图”拉回性质的证明验证及相关疑问求助

各位代数几何/范畴论的大佬们好！之前看到不少关于这个“魔法图”的讨论，核心是要确认下面这个图是笛卡尔图（即拉回图）：

$$
\require{AMScd}
\begin{CD}
X_1\times_Y X_2 @>{p}>> X_1\times_Z X_2\
@V{h=f_1\circ y_1=f_2\circ y_2}V V @V{q}V V\
Y @>{d}>> Y \times_Z Y
\end{CD}
$$

我尝试写了一份验证证明，想请大家帮忙看看有没有哪里考虑不周或者遗漏的地方，证明过程如下：

1. 先证图的交换性：$d \circ h = q \circ p$

   • 先记 $h = f_1 \circ y_1 = f_2 \circ y_2$，利用乘积$Y\times_Z Y$的投影态射性质$s\circ d = 1_Y$ 和 $t \circ d = 1_Y$，可以得到：
     • $s \circ d \circ h = h = f_1 \circ y_1 = f_1 \circ z_1 \circ p = s \circ q \circ p$
     • $t \circ d \circ h = h = f_2 \circ y_2 = f_2 \circ z_2 \circ p = t \circ q \circ p$
   • 因为$s,t$是乘积$Y\times_Z Y$的投影，根据乘积的泛性质，就能推出$d \circ h = q \circ p$，也就是这个笛卡尔图是交换的。

2. 再证拉回的泛性质：任给态射$i: W \to Y$和$j: W \to X_1 \times_Z X_2$满足$d \circ i = q \circ j$，要证存在唯一的态射$l: W \to X_1 \times_Y X_2$使得$h \circ l = i$且$p \circ l = j$

   • 首先推导两个关键等式：
     • $f_1 \circ z_1 \circ j = s \circ q \circ j = s \circ d \circ i = i$
     • $f_2 \circ z_2 \circ j = t \circ q\circ j = t \circ d \circ i = i$
   • 根据$X_1 \times_Y X_2$的拉回泛性质，存在唯一的态射$l: W \to X_1 \times_Y X_2$，使得$y_1 \circ l = z_1 \circ j$且$y_2 \circ l = z_2 \circ j$。
   • 又因为$y_1 = z_1 \circ p$，$y_2 = z_2 \circ p$，代入得$z_1 \circ p \circ l = z_1 \circ j$和$z_2 \circ p \circ l = z_2 \circ j$，再根据$X_1 \times_Z X_2$的乘积泛性质，可得$j = p \circ l$。
   • 同时可以验证$i = h \circ l$：$i = s \circ d \circ i = s \circ q \circ j = s \circ q \circ p \circ l = f_1 \circ y_1 \circ l = h \circ l$。
   • 唯一性验证：如果存在另一个态射$l': W \to X_1 \times_Y X_2$满足$j = p \circ l'$（进而$i = h \circ l'$），那么$y_1 \circ l' = z_1 \circ p \circ l' = z_1 \circ j$，$y_2 \circ l' = z_2 \circ p \circ l' = z_2 \circ j$，根据之前$l$的唯一性，就能推出$l' = l$。$\square$

写完证明后，我还有几个拿不准的点想请教大家：

• 看起来要让态射能通过这个“魔法图”分解，好像只需要满足其中一半条件，另一半就能自动推导出来？这个结论是对的吗？
• 我证明里用到的图感觉有点别扭：比如$f_1 \circ y_1 = f_2 \circ y_2$这个条件在图里没体现出来，而且$d\circ s$、$d \circ t$并不是$Y \times_Z Y$上的恒等态射。我是不是在证明里用到了图里某些不交换的路径？有没有更清晰的图布局方式，能让起点和终点相同的路径都交换？

麻烦各位大佬帮忙看看我的证明是否正确，或者有没有哪里需要补充修正的，也希望能解答一下我的疑问，提前谢谢大家啦！

备注：内容来源于stack exchange，提问作者onRiv