ファンクター（関手）はアイソモーフィズム（同形写像）をアイソモーフィズム（同形写像）へマップすることの記述/証明
話題
About: カテゴリー（圏）
この記事の目次
開始コンテキスト
- 読者は、コバリアント（共変）ファンクター（関手）の定義を知っている。
- 読者は、コントラバリアント（反変）ファンクター（関手）の定義を知っている。
- 読者は、%カテゴリー名%アイソモーフィズム（同形写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のファンクター（関手）は任意のアイソモーフィズム（同形写像）をあるアイソモーフィズム（同形写像）へマップするという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(C_1\): \(\in \{\text{ 全てのカテゴリー（圏）たち }\}\)
\(C_2\): \(\in \{\text{ 全てのカテゴリー（圏）たち }\}\)
\(F\): \(\in \{C_1 \text{ から } C_2 \text{ への全てのファンクター（関手）たち }\}\)
\(O_1\): \(\in Obj (C_1)\)
\(O_2\): \(\in Obj (C_1)\)
\(f\): \(\in Mor (O_1, O_2)\)
//
ステートメント（言明）たち:
\(f \in \{\text{ 全ての } C_1 \text{ アイソモーフィズム（同形写像）たち }\}\)
\(\implies\)
\(F (f) \in \{\text{ 全ての } C_2 \text{ アイソモーフィズム（同形写像）たち }\}\)
//
2: 自然言語記述
任意のカテゴリー（圏）たち\(C_1, C_2\)、\(C_1\)から\(C_2\)への任意のファンクター（関手）\(F\)、任意のオブジェクトたち\(O_1, O_2 \in Obj (C_1)\)、任意のモーフィズム（射）\(f \in Mor (O_1, O_2)\)に対して、もしも、\(f\)が\(C_1\)アイソモーフィズム（同形写像）である場合、\(F (f) \in Mor (F (O_1), F (O_2))\)は\(C_2\)アイソモーフィズム（同形写像）である。
3: 証明
以下を満たすあるモーフィズム（射）\(f^{-1} \in Mor (O_2, O_1)\)、つまり、\(f^{-1} \circ f = id_{O_1} \land f \circ f^{-1} = id_{O_2}\)、がある。
\(F\)はコバリアント（共変）ファンクター（関手）であると仮定しよう。
コバリアント（共変）ファンクター（関手）の定義によって、\(F (f^{-1}) \circ F (f) = F (f^{-1} \circ f) = F (id_{O_1}) = id_{F (O_1)}\); \(F (f) \circ F (f^{-1}) = F (f \circ f^{-1}) = F (id_{O_2}) = id_{F (O_2)}\)、それが意味するのは、\(F (f)\)は\(C_2\)アイソモーフィズム（同形写像）であるということ。
\(F\)はコントラバリアント（反変）ファンクター（関手）であると仮定しよう。
コントラバリアント（反変）ファンクター（関手）によって、\(F (f) \circ F (f^{-1}) = F (f^{-1} \circ f) = F (id_{O_1}) = id_{F (O_1)}\); \(F (f^{-1}) \circ F (f) = F (f \circ f^{-1}) = F (id_{O_2}) = id_{F (O_2)}\)、それが意味するのは、\(F (f)\)は\(C_2\)アイソモーフィズム（同形写像）であるということ。
