Red cat の数学よもやま話・新装開店

はてなダイアリー「Red cat の数学よもやま話」から徐々にこちらに移行していきます。

直観主義論理の入り口~Heyting 代数~(その 8)

今回は Heyting 代数の性質についてもう少し詳し見ていきます. 以下 H は Heyting 代数とし, a, b, c, a', b' \in H とします.

1. b \le a \to b.
b \wedge a \le b より明らか.

2. a \le a', b' \le b ならば a' \to b' \le a \to b.
(a' \to b') \wedge a \le (a' \to b') \wedge a' \le b' \le b より.

3. a \to (b \wedge c) = (a \to b) \wedge (a \to c).
函手 a \to (-) : H \to H が極限を保つことから従う.

4. (a \vee b) \to c = (a \to c) \wedge (b \to c).
(a \vee b) \to c \le a \to c(a \vee b) \to c \le b \to c から (a \vee b) \to c \le (a \to c) \wedge (b \to c),
{\begin{align}
(a \to c) \wedge (b \to c) \wedge (a \vee b)
 &=   ( (a \to c) \wedge a \wedge (b \to c) ) \vee ( (a \to c) \wedge (b \to c) \wedge b ) \\
 &\le ( c \wedge (b \to c) ) \vee ( (a \to c) \wedge c ) \\
 &=    c \vee c = c
\end{align}}
により (a \to c) \wedge (b \to c) \le (a \vee b) \to c,
よって (a \vee b) \to c = (a \to c) \wedge (b \to c).
分配圏の性質としても導くことができる.
{\begin{align}
 \hom(x, (a \vee b) \to c)
  &\simeq \hom(x \wedge (a \vee b), c) \\
  &\simeq \hom( (x \wedge a) \vee (x \wedge b), c ) \\
  &\simeq \hom(x \wedge a, c) \times \hom(x \wedge b, c) \\
  &\simeq \hom(x, a \to c) \times \hom(x, b \to c) \\
  &\simeq \hom( x, (a \to c) \wedge (b \to c) ).
\end{align}}

5. (a \to c) \vee (b \to c) \le (a \wedge b) \to c.
a \to c \le (a \wedge b) \to cb \to c \le (a \wedge b) \to c から従う.

6. (a \to b) \vee (a \to c) \le a \to (b \vee c).
a \to b \le a \to (b \vee c)a \to c \le a \to (b \vee c) から従う.

7. a \to (b \to c) = (a \wedge b) \to c.
圏論の冪の性質から従う.
{\begin{align}
 \hom( x, a \to (b \to c) )
  &\simeq \hom(x \wedge a, b \to c) \\
  &\simeq \hom( (x \wedge a) \wedge b, c ) \\
  &\simeq \hom(x \wedge (a \wedge b), c) \\
  &\simeq \hom(x, (a \wedge b) \to c).
\end{align}}