PS

Inverse image adjunctions

圏論 Adjunction 命題

(･･･とでも呼ぶことにする)

Posetal powerset

任意の集合 $A$ について、objectを $A$ の部分集合、morphismを $\subseteq$ とするposetal category*1:

$\mathcal{P}(A)$

を定義できる。

以下、任意の関数:

$f : A \to B$

について･･･

Direct(existential) image

$f _ \exists : \mathcal{P}(A) \to \mathcal{P}(B)$
$f _ \exists (A _ 0) := \lbrace b \in B \mid f({} ^ \exists a \in A) = b, a \in A _ 0 \rbrace$

Inverse image

$f ^ {-1} : \mathcal{P}(B) \to \mathcal{P}(A)$
$f ^ {-1}(B _ 0) := \lbrace a \in A \mid f(a) \in B _ 0 \rbrace$

Dual(universal) image

$f _ \forall : \mathcal{P}(A) \to \mathcal{P}(B)$
$f _ \forall (A _ 0) := \lbrace b \in B \mid f({} ^ \forall a \in A) = b, a \in A _ 0 \rbrace$

とすると、これらは確かにfunctorial(この場合特にmonotonic)、つまり

$X \subseteq Y \Rightarrow g(X) \subseteq g(Y)$

を満たしている。

命題

$f _ \exists \dashv f ^ {-1} \dashv f _ \forall$

証明

$A _ 0 \subseteq f ^ {-1} ( f _ \exists (A _ 0) )$
$f _ \exists (f ^ {-1} (B _ 0) ) \subseteq B _ 0$

と、

$B _ 0 \subseteq f _ \forall ( f ^ {-1} (B _ 0) )$
$f ^ {-1} (f _ \forall (A _ 0) ) \subseteq A _ 0$

による。これらがそれぞれunitとcounitになっている。

RAPL

RAPL*2とそのdual*3により、命題:

$f ^ {-1} ( B _ 1 \cap B _ 2) = f ^ {-1} (B _ 1) \cap f ^ {-1} (B _ 2)$
$f ^ {-1} ( B _ 1 \cup B _ 2) = f ^ {-1} (B _ 1) \cup f ^ {-1} (B _ 2)$
$f _ \exists ( A _ 1 \cup A _ 2) = f _ \exists (A _ 1) \cup f _ \exists (A _ 2)$

を大げさに証明できる。

参考文献

*1:特にcomplete Heyting algebra

*2:Right Adjoints Preserve Limits

*3:left adjoints preserve colimits