写像
word(ss,s) … \(\to\)\({\to}.\)【\(X \to Y = \{ f \subset X \times Y \mid X \subset \text{dom!} ( f ) \}\)】
word(s,c)F … \(\text{Mapon}\)
def …【\(\text{Mapon} ( {\sf X} )\)】≃【\(\{ {\sf f} \mid \exists {\sf y} \, {\sf f} \in {\sf X} \to {\sf y} \} \)】
\(\text{Mapon}\emptyset\)【\(\text{Mapon} ( \emptyset ) = \{ \emptyset \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\text{map1}\)【\(X \neq \emptyset \Longrightarrow X \to \emptyset = \emptyset\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}{\to}\)【\(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(|{\to}\)【\(f \in X \to Y , A \subset X \Longrightarrow f | _{ A } \in A \to Y\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
mapはoldではtoだった。チェック 'X to Y = X map Y' / d. ＜ %0
単射、全射
word(ss,s) … \(\stackrel{\rm I}\to\) \(\stackrel{\rm S}\to\) \(\stackrel{\rm IS}\to\)\({\stackrel{\rm I}\to}.\)【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid \forall y \, ! x \, \langle x , y \rangle \in f \}\)】
\({\stackrel{\rm S}\to}.\)【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \text{im} ( f ) = Y \}\)】
\({\stackrel{\rm IS}\to}.\)【\(X \stackrel{\rm IS}\to Y = ( X \stackrel{\rm I}\to Y ) \cap ( X \stackrel{\rm S}\to Y )\)】
\({\stackrel{\rm IS}\to}{.}{.}\)【\(X \stackrel{\rm IS}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \in Y \to X \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\text{Mapon1}\)【\(f \in \text{mapon} ( X ) \Longrightarrow f \in X \stackrel{\rm S}\to \text{im} ( f )\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}{\stackrel{\rm I}\to}\)【\(f \in X \stackrel{\rm I}\to Y , g \in Y \stackrel{\rm I}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm I}\to Z\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}{\stackrel{\rm S}\to}\)【\(f \in X \stackrel{\rm S}\to Y , g \in Y \stackrel{\rm S}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm S}\to Z\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}{\stackrel{\rm IS}\to}\)【\(f \in X \stackrel{\rm IS}\to Y , g \in Y \stackrel{\rm IS}\to Z \Longrightarrow g \circ f \in X \stackrel{\rm IS}\to Z\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
最初の写像
具体的な写像を作るときには\(\lambda\)計算の記号が便利ですが、クラスであることに注意です。abbr …【\([ {\sf x} \mid {\sf X} ]\)】≈【\(\{ {\sf z} \mid \exists {\sf x} \, {\sf z} = \langle {\sf x} , {\sf X} \rangle \} \)】
abbr …【\([ {\sf x} {\sf A} \mid {\sf X} ]\)】≈【\(\{ \langle {\sf x} , {\sf X} \rangle \mid {\sf x} {\sf A} \}\)】
\(\text{Mapon0}\)【\(f \in \text{Mapon} ( X ) \Longrightarrow f = [ x \in X \mid f ( x ) ]\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
一点集合への写像
word(ss,s)! …【\({\sf Y} _{ \mid {\sf X} }\)】
\(\text{on.}\)【\(y _{ \mid X } = X \times \{ y \}\)】
\(\text{on0}\)【\(y _{ \mid X } = [ x \in X \mid y ]\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\text{on1}\)【\(X \to \{ y \} = \{ y _{ \mid X } \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
互換
word(ss,s) … \(\leftrightharpoons\)
\({\leftrightharpoons}.\)【\(x \leftrightharpoons y = \{ \langle x , y \rangle , \langle y , x \rangle \}\)】
入力補助を？
恒等写像
word(s,s)! …【\(\text{id} _{ {\sf X} }\)】\(\text{id}.\)【\(\text{id} _{ X } = [ x \in X \mid x ]\)】
\(\text{id0}\)【\(\text{id} _{ X } \in X \stackrel{\rm IS}\to X\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}単\)【\(R \subset X \times Y \Longrightarrow \text{id} _{ Y } \circ R = R = R \circ \text{id} _{ X }\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(|\text{id}\)【\(R \in \text{Rel} \Longrightarrow R | _{ X } = R \circ \text{id} _{ X }\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\stackrel{\rm I}\to}{.}{.}\)【\(X \stackrel{\rm I}\to Y = \{ f \in X \to Y \mid f ^\leftrightarrow \circ f = \text{id} _{ X } \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\stackrel{\rm S}\to}{.}{.}\)【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid f \circ f ^\leftrightarrow = \text{id} _{ Y } \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
to:I.. / d. ＜ %0 ， sw. と to