読者です 読者をやめる 読者になる 読者になる

北海道苫小牧市出身の壮年PGが書くブログ

永遠のプログラマを夢見る、苫小牧市出身のおじさんのちらしの裏

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

math

前回の続き。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:上の三角形が可換かは確かめる必要がありますが、定義通り計算すれば自明です。