Kripke semantics and exponentiations in functor category

昔から functor category の冪はなぜ pointwise じゃなくて複雑な形をしているのだろうかと不思議だったのですが、なんとなく答えが見えたような気がするので記念にまとめ。

pointwise に冪をとると何が困るかというと、対象をそうやって作ってしまうと射がうまく写せないのが問題なのでした。

つまり関手 F, G に対して

$F^G(X) = (FX)^{GX}$

としてしまうと $f : X \to Y$ に対して

$F^G(f) : (FX)^{GX} \to (FY)^{GY}$

が自然に定義できないということです。

正しくは、米田の補題と冪の adjoint による定義を使って

$F^G(X) = Nat(Hom(X, -), F^G)$
$\quad = Nat(Hom(X, -)\times G, F)$

とします。

なんかよくわかりませんが、要するに X だけじゃなくてそれより大きいところも面倒見ないといけないということです。

上に出てきた冪の定義ですが、荒っぽく読むと

$\forall Y.Hom(X, Y) \times GY \to FY$

みたいなものです。さらに、X から Y への射が存在するということはだいたい X が Y より小さいということだと考えられるので

$\forall Y. X \leq Y \wedge GY \Longrightarrow FY$

これをよく見てみましょう。見たことがありませんか？直観主義論理の Kripke semantics で「G ならば F」を解釈したものです。