これはトポスに関する備忘録である.
一般に, 射$A\to B$があるとグラフ$A\to A\times B$を作ることができる. これはモノ射なので, トポスにおいてはこれはある$A\times B\to \Omega$によって分類され, 随伴によって$A\to PB$が得られる. これを$A\to B$の持ち上げと呼ぶことにする.
このとき次が成り立つ.
トポス$C$において以下が成り立つ.
(1)の証明には次の補題を用いるとよい.
$f\colon A\to B$, $g\colon B\to C$を射とする. $g$のグラフ$B\to B\times C$の$f\times id\colon A\times C\to B\times C$による引き戻しは$g\circ f$のグラフ$A\to A\times C$である.
$$
A\times C = (A\times_B B)\times (1\times_1 C)
= (A\times 1)\times_{B\times 1} (B\times C)
= A\times_B (B\times C)
$$
なので
$$
B\times_{A\times B} (A\times C)
= B\times_{B\times C} (B\times C) \times_B A
= B\times_B A
= A
$$
である. (図式を書いて確かめよ)
$id\colon B\to B$の持ち上げ$B\to PB$はモノである.
命題1(1)より, $A\to B$の持ち上げは$A\to B$と$B\to PB$の合成に等しいことがわかる. したがって命題1(2)は$B\to PB$がモノであることを表していることになる.
有限完備な圏において, $A^X$, $B^X$, $C^X$がそれぞれ存在するならば$(A\times_B C)^X$も存在し, それは$A^X\times_{B^X} C^X$である.
右随伴が極限と交換することの証明をなぞるとわかる.
トポスはカルテシアン閉である.
$B\to PB$はモノ射なので, ある$PB\to \Omega$が存在して$B=PB\times_\Omega 1$とできる. しかし$(PB)^X=P(B\times X)$, $\Omega^X=PX$, $1^X=1$はそれぞれ存在するので, それらのpullbackが$B^X$となる. したがって任意の$B$, $X$について$B^X$が存在するのでカルテシアン閉である.