PS

Creation

定義 関数

(一般化しても正しい用語なのか分からないが･･･)

  • 関数: f : X \rightarrow Y
  • 部分集合の族: (P _ A \subseteq A) _ A

について

Preservation

  • x \in P _ X \Rightarrow f(x) \in P _ Y

のとき、 f preserves P という。

このとき、関数:

  • P _ f : P _ X \rightarrow P _ Y

を作ることが出来る。

Reflection

  • f(x) \in P _ Y \Rightarrow x \in P _ X

のとき、 f reflects P という。

Lifting

  • y \in P _ Y \Rightarrow {} ^ \exists x \in P _ X, f(x) = y

のとき、 f lifts P という。

Unique lifting

  • y \in P _ Y \Rightarrow {} ^ \exists ! x \in P_X,\ f(x) = y

のとき、 f lifts P uniquely という。

これは、 ! を使わずに書くと、

  • y \in P _ Y \Rightarrow
    • {} ^ \exists x \in P _ X,
      • f(x) = y
      • {} ^ \forall x' \in P _ X, f(x') = y \Rightarrow x = x'

ということだが、少し要件を厳しくして･･･

Creation

  • y \in P _ Y \Rightarrow
    • {} ^ \exists x \in P_X,
      • f(x) = y
      • {} ^ \forall x' \in X, f(x') = y \Rightarrow x = x'

のとき、 f creates P という。 (最後の行の P_X のところが X に代わっている)

これは、 f(x) = y なる x \in X がただ一つ存在し、しかも x \in P_X ということ。

命題

  • f : \text{creates } P \Rightarrow f : \text{lifts } P \text{ uniquely} \Rightarrow f : \text{lifts } P
  • f : \text{creates } P \Leftrightarrow f : \text{reflects } P \text{ and lifts } P \text{ uniquely}

参考文献