Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

CLTT p45 Exercises 1.3.1 (i) の証明の一部 (2)

前回の続き。only if を示します。

Categorical Logic and Type Theory, Volume 141 (Studies in Logic and the Foundations of Mathematics)
0444508538

まず、(u,f)がカルテシアンなので、(u,π'):(I,Y)→(J,Y)とIに関して、以下を可換にするようなj:I×Y→Xが存在します。

このjに対して、h^-1 = <π,j> と定義します。<π,j>は以下の図のようになります。この図は上の可換性を元の圏の射で表したものであり、これによってh^-1が求める射が満たすべき可換性を満たすことがわかります。

後は、このh^-1がisoになるかどうか。ここで h = <π,f>と定義すると、h;h^-1 = I×X かつ h^-1;h = I×Y となります。

まず、h^-1;h = I×Yは、以下の図で <π,π'> = I×Y、 <π,π'> = <π,j>;<π,f> であり、直積の一意性から言えます。

最後、h;h^-1 = I×Xですが、まずは以下の図を考えます。(u,f)とIについて、緑の射も青の射も図を可換にします*1が、(u,f)がカルテシアンなのでこの射は一意となります。つまり、(I,f);(I,j) = (I,π')です。

この等式を元の圏で考えると、以下の図になります。ここで、<π,π'> = I×X = <π,f>;<π,j> なので、h;h^-1 = I×Xが言えます。

*1:上の三角形が可換かは確かめる必要がありますが、定義通り計算すれば自明です。