かじもとにっき

自分用メモ

Galois connectionのいくつかの同値な定義

数学

以下、(A,\leqA)と(B,\leqB)を共にposetとする。

定義 (Galois connection)

(F,G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB)
  \equivDef F \in A \leftarrow B \wedge G \in B \leftarrow A \wedge \langle \forall x \in B, y \in A :: F.x \leqA y \equiv x \leqB G.y \rangle

定理 (Cancellation)

(F, G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB) \Rightarrow F \bullet G \dleqA I_A \wedge I_B \dleqB G \bullet F

証明

定義内のxとyとしてそれぞれG.yとF.xを取れば直ちに導かれる。∎

定義 (Poset of monotonic functions)

(A,\leqA) \funcM (B,\leqB) \overset{\text{def}}{=} (\{ f \in A \leftarrow B : \langle \forall x,y \in B : x \leqB y : f.x \leqA f.y \rangle : f \}, \dleqA)

定理 (Galois connectionの別の定義)

(F, G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB)
  \equiv F \in (A,\leqA) \funcM (B,\leqB) \wedge G \in (B,\leqB) \funcM (A,\leqA) \wedge F \bullet G \leqA I_A \wedge I_B \leqB G \bullet F

証明

(\Rightarrow):

CancellationによりF \bullet G \dleqA I_AとI_B \dleqB G \bullet Fが成り立つので、後はFとGが共にmonotonicであることを言えば良い。
任意のx,y \in Bに対し:

  F.x \leqA F.y
\Leftrightarrow  { (F, G) \text{ is a Galois connection } }
  x \leqB G(F.y)
\Leftarrow  { cancellation: I_B \dleqB G \bullet F + \leqB-transitivity }
  x \leqB y

同様に、任意のx,y \in Aに対し:

  G.x \leqB G.y
\Leftrightarrow  { (F, G) \text{ is a Galois connection } }
  F(G.x) \leqA y
\Leftarrow  { cancellation: F \bullet G \dleqA I_A + \leqA-transitivity }
  x \leqA y

(\Leftarrow):

任意のx \in Bとy \in Aに対し:

  F.x \leqA y
\Rightarrow  { G \text{ is monotonic} }
  G(F.x) \leqB G.y
\Rightarrow  { cancellation + \leqB-transitivity }
  x \leqB G.y
\Rightarrow  { F \text{ is monotonic} }
  F.x \leqA F(G.y)
\Rightarrow  { cancellation + \leqA-transitivity }
  F.x \leqA y

∎

定理 (Galois connectionの別の定義)

(F, G) \text{ is a Galois connection between } (A,\sqsubseteq) \text{ and } (B,\preceq)
  \equiv F \in (A,\leqA) \funcM (B,\leqB) \wedge G \in B \leftarrow A \wedge F \bullet G \dleqA I_A \wedge \langle \forall x \in B, y \in A : F.x \leqA y : x \leqB G.y \rangle

証明

\text{LHS} \equiv \text{RHS} \wedge \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y \rangleなので、
\text{RHS} \Rightarrow \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y \rangleを示せば良い。

任意のx \in Bとy \in Aに対し:

  x \leqB G.y
\Rightarrow  { assumption: F \text{ is monotonic } }
  F.x \leqA F(G.y)
\Rightarrow  { assumption: F \bullet G \dleqA I_A + \leqA-transitivity }
  F.x \leqA y

∎

補足

RHS*1において、

  F \bullet G \dleqA I_A \wedge \langle \forall x \in B, y \in A : F.x \leqA y : x \leqB G.y \rangle
\Leftrightarrow  { lifting }
  \langle \forall y \in A :: F(G.y) \leqA y \rangle \wedge \langle \forall x \in B, y \in A : F.x \leqA y : x \leqB G.y \rangle
\Leftrightarrow  { (\forall/\wedge)-distributivity }
  \langle \forall y \in A :: F(G.y) \leqA y \wedge \langle \forall x \in B : F.x \leqA y : x \leqB G.y \rangle
\Leftrightarrow  { informally }
  \langle \forall y \in A :: G.y \text{ is the greatest } x \in B \text{ s.t. } F.x \leqA y \rangle

定理 (Galois connectionの別の定義)

(F, G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB)
  \equiv F \in A \leftarrow B \wedge G \in (B,\leqB) \funcM (A,\leqA) \wedge I_B \dleqB G \bullet F \wedge \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y \rangle

証明

先の定理と同様。∎

補足

RHSにおいて、

  I_B \dleqB G \bullet F \wedge \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y  \rangle
\Leftrightarrow  { informally }
  \langle \forall x \in B :: F.x \text{ is the least } y \in A \text{ s.t }  x \leqB G.y \rangle

参考文献

  • R.C. Backhouse. Mathematics of Program Construction, Unpublished.
  • R. Bird and O. de Moor. Algebra of Programming. Series in Computer Science. Prentice-Hall, 1997.
  • B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.
  • D. Gries and F.B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
  • S. Rudeanu. Sets and Ordered Structures. Bentham Science Publishers, 2012.

*1:right hand side