写像
word(,c) … \(\text{Map}\)def …【\(\text{Map}\)】≃【\(\{ f \in \text{Rel} \mid \forall x \, ! y \, \langle x , y \rangle \in 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{mapon0}\)【\(\text{mapon} ( \emptyset ) = \{ \emptyset \}\)】\({\bf /}\text{set}_1.{\bf /}\emptyset{.}{.}{\bf /}\text{dom.}\) ◀ O
word(ss,s) … \(\to\)
\({\to}.\)【\(X \to Y = \{ f \in \text{mapon} ( X ) \mid \text{rng} ( f ) \subset Y \}\)】
\(\text{Map0}\)【\(f \in \text{Map} \Longrightarrow f \in \text{dom} ( f ) \to \text{rng} ( f )\)】\({\bf /}{\to}.{\bf /}{\subset.}\) ◀ O
\({\circ}\text{Map}\)【\(f \in X \to Y , g \in Y \to Z \Longrightarrow g \circ f \in X \to Z\)】\({\bf /}{\to}.{\bf /}^{1112}{=.}{\bf /}^{1212}{=.}{\bf /}^{212}{=.}{\bf /}{\subset.}{\bf /}\mathbb{S}.\) ◀ \(\text{%0}\)
写像への代入、\(\lambda\)記法
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\)】
\(\text{ap1}\)【\(f \in X \to Y , x \in X \Longrightarrow f ( x ) \in Y\)】\({\bf /}{\to}.{\bf /}{\subset.}{\bf /}\text{rng.}\) ◀ \(\text{ap0}\)
\({\circ}\text{ap}\)【\(f \in X \to Y , g \in Y \to Z , x \in X \Longrightarrow ( g \circ f ) ( x ) = g ( f ( x ) )\)】\(\) ◀ \({\circ}\text{Map}\,{\bf ,}\,{\to}.\,{\bf ,}\,\text{ap0}\,{\bf ,}\,!{\circ}\text{ap}\)
\(!{\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\)】\({\bf /}{\to}.{\bf /}^{11112}{=.}{\bf /}^{11212}{=.}{\bf /}{\subset.}{\bf /}\mathbb{S}.\) ◀ \(\text{ap0}{\bf /}^{112}{=.}{\bf /}\text{dom.}\)
写像を作るときには\(\lambda\)計算の記法が便利です。ただしクラスであることに注意。
abbr …【\([ {\sf x} {\sf A} \mid {\sf X} ]\)】≈【\(\{ \langle {\sf x} , {\sf X} \rangle \mid {\sf x} {\sf A} \}\)】
\(\text{Map1}\)【\(f \in \text{mapon} ( X ) \Longrightarrow f = [ x \in X \mid f ( x ) ]\)】\({\bf /}^{12}{=.}{\bf /}\text{dom.}\) ◀ \(\text{ap0}{\bf /}^{112}{=.}{\bf /}\text{dom.}\)
一点集合への写像
word(ss,s)! …【\({\sf Y} _{ \mid {\sf X} }\)】def …【\({\sf Y} _{ \mid {\sf X} }\)】≃【\({\sf X} \times \{ {\sf Y} \}\)】
\(\text{on0}\)【\(y _{ \mid X } = [ x \in X \mid y ]\)】\({\bf /}\mathbb{S}.\) ◀ O
\(\text{on1}\)【\(X \to \{ y \} = \{ y _{ \mid X } \}\)】\({\bf /}{=.}{\bf /}\mathbb{S}.{\bf /}^{2112}{=.}{\bf /}^{22}{=.}{\bf /}{\subset.}{\bf /}\mathbb{S}.\) ◀ \(\text{%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 x , y \in X . ( f ( x ) = f ( y ) \Rightarrow x = y ) \}\)】
\({\stackrel{\rm S}\to}.\)【\(X \stackrel{\rm S}\to Y = \{ f \in X \to Y \mid \text{rng} ( 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 )\)】
\({\circ}\text{MapI}\)【\(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\)】\({\bf /}{\stackrel{\rm I}\to}.\rfloor\) ◀ \({\circ}\text{Map}\)
\({\circ}\text{MapS}\)【\(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\)】
compMapI / to.I. Rr < compMap , ap1 , compap
恒等写像
恒等写像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\)】
\(|\text{id}\)【\(\text{Rel} ( R ) \Longrightarrow R | _{ X } = R \circ \text{id} _{ X }\)】
/ to.IS. は未実装