写像
word(,c) … \(\text{Map}\)def …【\(\text{Map}\)】≃【\(\{ {\sf f} \in \text{Rel} \mid \forall {\sf x} \, ! {\sf y} \, \langle {\sf x} , {\sf y} \rangle \in {\sf f} \}\)】
word(s,c)F … \(\text{mapon} \)
def …【\(\text{mapon} ( {\sf X} )\)】≃【\(\{ {\sf f} \in \text{Map} \mid \text{dom} ( {\sf f} ) = {\sf X} \}\)】
\(\text{mapon}\emptyset\)【\(\text{mapon} ( \emptyset ) = \{ \emptyset \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
word(ss,s) … \(\to\)
\({\to}.\)【\(X \to Y = \{ f \in \text{mapon} ( X ) \mid \text{im} ( f ) \subset Y \}\)】
\({\to}{.}{.}\)【\(X \to Y = \{ f \subset X \times Y \mid \forall x \in X . \exists! y \, \langle x , y \rangle \in f \}\)】\(\,{\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}.\)
写像の和
単射、全射
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{Map}0\)【\(f \in \text{Map} \Longrightarrow f \in \text{dom} ( f ) \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}.\)
写像への代入
word(ss,s)! …【\({\sf F} ( {\sf X} )\)】\(\text{ap0}\)【\(f \in \text{mapon} ( X ) , x \in X \Longrightarrow \langle x , f ( x ) \rangle \in f\)】
代入はなるべく使用しない方が良いです。【\(y = f ( x )\)】は【\(\langle x , y \rangle \in f\)】としましょう。
\(\text{ap1}\)【\(f \in X \to Y , x \in X \Longrightarrow f ( x ) \in Y\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\text{Pap0}\)【\(f \in \text{mapon} ( X ) , A \subset X \Longrightarrow f ( A ) = \{ f ( a ) \mid a \in A \}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\circ}\text{ap}\)【\(f \in X \to Y , g \in Y \to Z , x \in X \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(!{\circ}\text{ap}\)【\(f \in X \to Y , g \in Y \to Z , x \in X \Longrightarrow \langle x , g ( f ( x ) ) \rangle \in g \circ f\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
写像の例
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} \}\)】
\({\to}1\)【\(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}.\)
射影？