かじもとにっき

自分用メモ

infとsup

数学

定義 (infimumとsupremum)

\mathcal Aと\mathcal Bを共にposetとする。
Binary relation \operatorname{\underline{=\sqcap}} \in \mathcal A \sim (\mathcal A \funcM \mathcal B)と\operatorname{\underline{=\sqcup}} \in \mathcal A \sim (\mathcal A \funcM \mathcal B)をそれぞれ

x \operatorname{\underline{=\sqcap}} f \equivDef \langle \forall a \in \mathcal A :: a \sqsubseteq x \equiv K.a \operatorname{\dot\sqsubseteq} f \rangle, 
x \operatorname{\underline{=\sqcup}} f \equivDef \langle \forall a \in \mathcal A :: x \sqsubseteq a \equiv f \operatorname{\dot\sqsubseteq} K.a \rangle
  where K = \langle a :: \langle b :: a \rangle \rangle \in (\mathcal A \leftarrow \mathcal B) \leftarrow \mathcal A

で定義し、x \operatorname{\underline{=\sqcap}} fをx \text{ is the infimum of } f、x \operatorname{\underline{=\sqcup}} fをx \text{ is the supremum of } fと読む。

定理 (infimumとsupremumの一意性)

\operatorname{\underline{=\sqcap}} \text{ and } \operatorname{\underline{=\sqcup}} \text{ are coinjective } .

証明

x \operatorname{\underline{=\sqcap}} f \wedge y \operatorname{\underline{=\sqcap}} fを仮定する。

任意のa \in \mathcal Aに対し:

   a \leqA x
\Leftrightarrow  { \operatorname{\underline{=\sqcap}}-definition }
   K.a \dleqA f
\Leftrightarrow  { \operatorname{\underline{=\sqcap}}-definition }
   a \leqA y .

よって、indirect equalityによりx=y。
supremumに関しても同様。

∎

定理 (infimumとsupremumの伝統的定義)

x \in \mathcal A、f \in \mathcal A \funcM \mathcal Bとすると、

x \operatorname{\underline{=\sqcap}} f \equiv K.x \operatorname{\dot\sqsubseteq} f \wedge \langle \forall a \in \mathcal A : K.a \operatorname{\dot\sqsubseteq} f : a \sqsubseteq x \rangle , 
x \operatorname{\underline{=\sqcup}} f \equiv f \operatorname{\dot\sqsubseteq} K.x \wedge \langle \forall a \in \mathcal A : f \operatorname{\dot\sqsubseteq} K.a : x \sqsubseteq a \rangle .

証明

(\Rightarrow):

infimumとsupremumの定義におけるaとしてxを取れば直ちに導かれる。

(\Leftarrow):

任意のa \in Aに対し:

  K.a \operatorname{\dot\sqsubseteq} f
\Leftarrow  { assumption:K.x \operatorname{\dot\sqsubseteq} f + \operatorname{\dot\sqsubseteq}-transitivity }
  K.a \operatorname{\dot\sqsubseteq} K.x
\Leftarrow  { K \text{ is monotonic } }
  a \sqsubseteq x .

supremumに関しても同様。

∎

定義 (completenessとcocompleteness)

\mathcal Aと\mathcal Bを共にposetとする。

\mathcal A \text{ is } \mathcal B \text{-complete } \equivDef \langle \forall f \in \mathcal A \underset{M}{\leftarrow} \mathcal B :: \langle \exists x \in \mathcal A :: x \operatorname{\underline{=\sqcap}} f \rangle \rangle  ,
\mathcal A \text{ is } \mathcal B \text{-cocomplete } \equivDef \langle \forall f \in \mathcal A \underset{M}{\leftarrow} \mathcal B :: \langle \exists x \in \mathcal A :: x \operatorname{\underline{=\sqcup}} f \rangle \rangle  ,
\mathcal A \text{ is complete } \equivDef \langle \forall \mathcal B : \mathcal B \text{ is a poset } : \mathcal A \text{ is } \mathcal B \text{-complete } \rangle  ,
\mathcal A \text{ is cocomplete } \equivDef \langle \forall \mathcal B : \mathcal B \text{ is a poset } : \mathcal A \text{ is } \mathcal B \text{-cocomplete } \rangle  .

定理 (completenessとcocompleteness)

\mathcal Aと\mathcal Bを共にposetとする。

\mathcal A \text{ is } \mathcal B \text{-complete} \equiv \langle \exists \sqcap :: (K, \sqcap) \text{ is a Galois connection between } \mathcal A \funcM \mathcal B \text{ and } \mathcal A \rangle,
\mathcal A \text{ is } \mathcal B \text{-cocomplete} \equiv \langle \exists \sqcup :: (\sqcup, K) \text{ is a Galois connection between } \mathcal A \text{ and } \mathcal A \funcM \mathcal B \rangle.

証明

  \mathcal A \text{ is } \mathcal B \text{-complete}
\Leftrightarrow  { definition }
  \langle \forall f \in \mathcal A \funcM \mathcal B :: \langle \exists x \in \mathcal A :: x \operatorname{\underline{=\sqcap}} f \rangle \rangle
\Leftrightarrow  { axiom of choice }
   \langle \exists \sqcap \in \mathcal A \leftarrow (\mathcal A \funcM \mathcal B) :: \langle \forall f \in \mathcal A \funcM \mathcal B :: \sqcap f \operatorname{\underline{=\sqcap}} f \rangle \rangle
\Leftrightarrow  { \operatorname{\underline{=\sqcap}}-definition }
   \langle \exists \sqcap \in \mathcal A \leftarrow (\mathcal A \funcM \mathcal B) :: \langle \forall f \in \mathcal A \funcM \mathcal B, a \in \mathcal A :: a \leqA \sqcap f \equiv K.a \dleqA f \rangle \rangle
\Leftrightarrow  { definition }
  \langle \exists \sqcap :: (K, \sqcap) \text{ is a Galois connection between } \mathcal A \funcM \mathcal B \text{ and } \mathcal A \rangle .

cocompletenessに関しても同様。

∎

参考文献

  • C.J. Aarts, R. C. Backhouse, P. Hoogendijk, T.S. Voermans, and J. van der Woude. A relational theory of datatypes. Unpublished.
  • 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. Foundations for Calculational Logic. In M. Broy, B. Schieder, eds., Mathematical Methods in Program Development. Springer, 1997.
  • 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.
  • G. Tourlakis. Lectures in Logic and Set Theory Vol. 1: Mathematical Logic. Cambridge University Press, 2003.
  • G. Tourlakis. Lectures in Logic and Set Theory Vol. 2: Set Theory. Cambridge University Press, 2003.