プロダクトマップ（写像）たちのコンポジション（合成）はコンポーネントマップ（写像）たちのコンポジション（合成）たちのプロダクトであることの記述/証明
話題
About: セット（集合）
この記事の目次
開始コンテキスト
- 読者は、プロダクトマップ（写像）の定義を知っている。
ターゲットコンテキスト
- 読者は、任意のプロダクトマップ（写像）たちのコンポジション（合成）は当該コンポーネントマップ（写像）たちのコンポジション（合成）たちのプロダクトであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述1
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(A\): \(\in \{\text{ 全てのアンカウンタブル（不可算）かもしれないインデックスセット（集合）たち }\}\)
\(\{S_\alpha \vert \alpha \in A\}\): \(S_\alpha \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S'_\alpha \vert \alpha \in A\}\): \(S'_\alpha \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S''_\alpha \vert \alpha \in A\}\): \(S''_\alpha \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{f_\alpha \vert \alpha \in A\}\): \(f_\alpha: S_\alpha \to S'_\alpha\)
\(\{f'_\alpha \vert \alpha \in A\}\): \(f'_\alpha: S'_\alpha \to S''_\alpha\)
\(\times_{\alpha \in A} f_\alpha\): \(: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S'_\alpha, (\alpha \mapsto f (\alpha)) \mapsto (\alpha \mapsto f_\alpha (f (\alpha)))\)
\(\times_{\alpha \in A} f'_\alpha\): \(: \times_{\alpha \in A} S'_\alpha \to \times_{\alpha \in A} S''_\alpha, (\alpha \mapsto f (\alpha)) \mapsto (\alpha \mapsto f'_\alpha (f (\alpha)))\)
//
ステートメント（言明）たち:
\(\times_{\alpha \in A} f'_\alpha \circ \times_{\alpha \in A} f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha = \times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\)
//
2: 自然言語記述1
アンカウンタブル（不可算）かもしれない任意のインデックスセット（集合）\(A\)、セット（集合）たちの任意のセット（集合）\(\{S_\alpha \vert \alpha \in A\}\)、セット（集合）たちの任意のセット（集合）\(\{S'_\alpha \vert \alpha \in A\}\)、セット（集合）たちの任意のセット（集合）\(\{S''_\alpha \vert \alpha \in A\}\)、以下を満たすマップ（写像）たちの任意のセット（集合）\(\{f_\alpha \vert \alpha \in A\}\)、つまり、\(f_\alpha: S_\alpha \to S'_\alpha\)、以下を満たすマップ（写像）たちの任意のセット（集合）\(\{f'_\alpha \vert \alpha \in A\}\)、つまり、\(f'_\alpha: S'_\alpha \to S''_\alpha\)、\(\times_{\alpha \in A} f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S'_\alpha, (\alpha \mapsto f (\alpha)) \mapsto (\alpha \mapsto f_\alpha (f (\alpha)))\)、\(\times_{\alpha \in A} f'_\alpha: \times_{\alpha \in A} S'_\alpha \to \times_{\alpha \in A} S''_\alpha, (\alpha \mapsto f (\alpha)) \mapsto (\alpha \mapsto f'_\alpha (f (\alpha)))\)に対して、\(\times_{\alpha \in A} f'_\alpha \circ \times_{\alpha \in A} f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha = \times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\)。
3: 証明1
全体戦略: ステップ1: \(\times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\)は本当に意味をなしていることをみる; ステップ2: \(\times_{\alpha \in A} f'_\alpha \circ \times_{\alpha \in A} f_\alpha\)は\(p = (\alpha \mapsto f (\alpha))\)を何へマップするかを見る; ステップ3: \(\times_{\alpha \in A} f'_\alpha \circ f_\alpha\)は\(p = (\alpha \mapsto f (\alpha))\)を何へマップするかを見る; ステップ4: 本命題を結論する。
ステップ1:
\(\times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\)は本当に意味をなしていることをみよう。
\(f'_\alpha \circ f_\alpha: S_\alpha \to S''_\alpha\)。
したがって、\(\times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\)は意味をなしている、プロジェクトマップ（写像）の定義に基づいて。それは、\(: (\alpha \mapsto f (\alpha)) \mapsto (\alpha \mapsto f'_\alpha \circ f_\alpha (f (\alpha)))\)である。
ステップ2:
\(p = (\alpha \mapsto f (\alpha)) \in \times_{\alpha \in A} S_\alpha\)は任意のものであるとしよう。
\(\times_{\alpha \in A} f'_\alpha \circ \times_{\alpha \in A} f_\alpha\)は\(p\)を何にマップするかを見よう。
\(p \mapsto (\alpha \mapsto f_\alpha (f (\alpha))) \mapsto (\alpha \mapsto f'_\alpha \circ f_\alpha (f (\alpha)))\)。
ステップ3:
\(p = (\alpha \mapsto f (\alpha)) \in \times_{\alpha \in A} S_\alpha\)は任意のものとしよう。
\(\times_{\alpha \in A} f'_\alpha \circ f_\alpha\)は\(p\)を何にマップするかを見よう。
\(p \mapsto (\alpha \mapsto f'_\alpha \circ f_\alpha (f (\alpha)))\)。
ステップ4:
ステップ2およびステップ3は、当該2マップ（写像）たちは\(p\)を同一ポイントへマップすることを示した、したがって、当該2マップ（写像）たちは同一である。
4: 構造化された記述2
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(J\): \(= \{1, ..., n\}\)
\(\{S_j \vert j \in J\}\): \(S_j \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S'_j \vert j \in J\}\): \(S'_j \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{S''_j \vert j \in J\}\): \(S''_j \in \{\text{ 全てのセット（集合）たち }\}\)
\(\{f_j \vert j \in J\}\): \(f_j: S_j \to S'_j\)
\(\{f'_j \vert j \in J\}\): \(f'_j: S'_j \to S''_j\)
\(f_1 \times ... \times f_n\): \(: S_1 \times ... \times S_n \to S'_1 \times ... \times S'_n, (p_1, ..., p_n) \mapsto (f_1 (p_1), , ..., f_n (p_n))\)
\(f'_1 \times ... \times f'_n\): \(: S'_1 \times ... \times S'_n \to S''_1 \times ... \times S''_n, (p_1, ..., p_n) \mapsto (f'_1 (p_1), , ..., f'_n (p_n))\)
//
ステートメント（言明）たち:
\(f'_1 \times ... \times f'_n \circ f_1 \times ... \times f_n: S_1 \times ... \times S_n \to S''_1 \times ... \times S''_n = f'_1 \circ f_1 \times ... \times f'_n \circ f_n: S_1 \times ... \times S_n \to S''_1 \times ... \times S''_n\)
//
5: 自然言語記述2
ファイナイト（有限）インデックスセット（集合）\(J = \{1, ..., n\}\)、セット（集合）たちの任意のセット（集合）\(\{S_j \vert j \in J\}\)、セット（集合）たちの任意のセット（集合）\(\{S'_j \vert j \in J\}\)、セット（集合）たちの任意のセット（集合）\(\{S''_j \vert j \in J\}\)、以下を満たすマップ（写像）たちの任意のセット（集合）\(\{f_j \vert j \in J\}\)、つまり、\(f_j: S_j \to S'_j\)、以下を満たすマップ（写像）たちの任意のセット（集合）\(\{f'_j \vert j \in J\}\) 、つまり、\(f'_j: S'_j \to S''_j\)、\(f_1 \times ... \times f_n: S_1 \times ... \times S_n \to S'_1 \times ... \times S'_n, (p_1, ..., p_n) \mapsto (f_1 (p_1), , ..., f_n (p_n))\)、\(f'_1 \times ... \times f'_n: S'_1 \times ... \times S'_n \to S''_1 \times ... \times S''_n, (p_1, ..., p_n) \mapsto (f'_1 (p_1), , ..., f'_n (p_n))\)に対して、\(f'_1 \times ... \times f'_n \circ f_1 \times ... \times f_n: S_1 \times ... \times S_n \to S''_1 \times ... \times S''_n = f'_1 \circ f_1 \times ... \times f'_n \circ f_n: S_1 \times ... \times S_n \to S''_1 \times ... \times S''_n\)。
6: 証明2
全体戦略: ステップ1: \(f'_1 \circ f_1 \times ... \times f'_n \circ f_n: S_1 \times ... \times S_n \to S''_1 \times ... \times S''_n\)は本当に意味をなしていることをみる; ステップ2: \(f'_1 \times ... \times f'_n \circ f_1 \times ... \times f_n\)は\(p = (p_1, ..., p_n)\)を何へマップするかを見る; ステップ3: \(f'_1 \circ f_1 \times ... \times f'_n \circ f_n\)は\(p = (p_1, ..., p_n)\)を何へマップするかを見る; ステップ4: 本命題を結論する。
ステップ1:
\(f'_1 \circ f_1 \times ... \times f'_n \circ f_n: S_1 \times ... \times S_n \to S''_1 \times ... \times S''_n\)は本当に意味をなしていることをみよう。
\(f'_j \circ f_j: S_j \to S''_j\)。
したがって、\(f'_1 \circ f_1 \times ... \times f'_n \circ f_n: S_1 \times ... \times S_n \to S''_1 \times ... \times S''_n\)は意味をなしている、プロジェクトマップ（写像）の定義に基づいて。それは、\(: (p_1, ..., p_n) \mapsto (f'_1 \circ f_1 (p_1), ..., f'_n \circ f_n (p_n))\)である。
ステップ2:
\(p = (p_1, ..., p_n) \in S_1 \times ... \times S_n\)は任意のものであるとしよう。
\(f'_1 \times ... \times f'_n \circ f_1 \times ... \times f_n\)は\(p\)を何にマップするかを見よう。
\(p \mapsto (f_1 (p_1), , ..., f_n (p_n)) \mapsto (f'_1 \circ f_1 (p_1), , ..., f'_n \circ f_n (p_n))\)。
ステップ3:
\(p = (p_1, ..., p_n) \in S_1 \times ... \times S_n\)は任意のものとしよう。
\(f'_1 \circ f_1 \times ... \times f'_n \circ f_n\)は\(p\)を何にマップするかを見よう。
\(p \mapsto (f'_1 \circ f_1 (p_1), ..., f'_n \circ f_n (p_n))\)。
ステップ4:
ステップ2およびステップ3は、当該2マップ（写像）たちは\(p\)を同一ポイントへマップすることを示した、したがって、当該2マップ（写像）たちは同一である。
