description/proof of that composition of product maps is product of compositions of component maps
Topics
About: set
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description 1
- 2: Natural Language Description 1
- 3: Proof 1
- 4: Structured Description 2
- 5: Natural Language Description 2
- 6: Proof 2
Starting Context
- The reader knows a definition of product map.
Target Context
- The reader will have a description and a proof of the proposition that the composition of any product maps is the product of the compositions of the component maps.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description 1
Here is the rules of Structured Description.
Entities:
\(A\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(\{S_\alpha \vert \alpha \in A\}\): \(S_\alpha \in \{\text{ the sets }\}\)
\(\{S'_\alpha \vert \alpha \in A\}\): \(S'_\alpha \in \{\text{ the sets }\}\)
\(\{S''_\alpha \vert \alpha \in A\}\): \(S''_\alpha \in \{\text{ the sets }\}\)
\(\{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)))\)
//
Statements:
\(\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: Natural Language Description 1
For any possibly uncountable index set, \(A\), any set of sets, \(\{S_\alpha \vert \alpha \in A\}\), any set of sets, \(\{S'_\alpha \vert \alpha \in A\}\), any set of sets, \(\{S''_\alpha \vert \alpha \in A\}\), any set of maps, \(\{f_\alpha \vert \alpha \in A\}\), such that \(f_\alpha: S_\alpha \to S'_\alpha\), any set of maps, \(\{f'_\alpha \vert \alpha \in A\}\), such that \(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)))\), and \(\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: Proof 1
Whole Strategy: Step 1: see that \(\times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\) indeed makes sense; Step 2: see what \(\times_{\alpha \in A} f'_\alpha \circ \times_{\alpha \in A} f_\alpha\) maps \(p = (\alpha \mapsto f (\alpha))\) to; Step 3: see what \(\times_{\alpha \in A} f'_\alpha \circ f_\alpha\) maps \(p = (\alpha \mapsto f (\alpha))\) to; Step 4: conclude the proposition.
Step 1:
Let us see that \(\times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\) indeed makes sense.
\(f'_\alpha \circ f_\alpha: S_\alpha \to S''_\alpha\).
So, \(\times_{\alpha \in A} f'_\alpha \circ f_\alpha: \times_{\alpha \in A} S_\alpha \to \times_{\alpha \in A} S''_\alpha\) makes sense, according to the definition of project map. It is \(: (\alpha \mapsto f (\alpha)) \mapsto (\alpha \mapsto f'_\alpha \circ f_\alpha (f (\alpha)))\).
Step 2:
Let \(p = (\alpha \mapsto f (\alpha)) \in \times_{\alpha \in A} S_\alpha\) be any.
Let us see what \(\times_{\alpha \in A} f'_\alpha \circ \times_{\alpha \in A} f_\alpha\) maps \(p\) to.
\(p \mapsto (\alpha \mapsto f_\alpha (f (\alpha))) \mapsto (\alpha \mapsto f'_\alpha \circ f_\alpha (f (\alpha)))\).
Step 3:
Let \(p = (\alpha \mapsto f (\alpha)) \in \times_{\alpha \in A} S_\alpha\) be any.
Let us see what \(\times_{\alpha \in A} f'_\alpha \circ f_\alpha\) maps \(p\) to.
\(p \mapsto (\alpha \mapsto f'_\alpha \circ f_\alpha (f (\alpha)))\).
Step 4:
Step 2 and Step 3 have shown that the 2 maps map \(p\) to the same point, so, the 2 maps are the same.
4: Structured Description 2
Here is the rules of Structured Description.
Entities:
\(J\): \(= \{1, ..., n\}\)
\(\{S_j \vert j \in J\}\): \(S_j \in \{\text{ the sets }\}\)
\(\{S'_j \vert j \in J\}\): \(S'_j \in \{\text{ the sets }\}\)
\(\{S''_j \vert j \in J\}\): \(S''_j \in \{\text{ the sets }\}\)
\(\{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))\)
//
Statements:
\(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: Natural Language Description 2
For the finite index set, \(J = \{1, ..., n\}\), any set of sets, \(\{S_j \vert j \in J\}\), any set of sets, \(\{S'_j \vert j \in J\}\), any set of sets, \(\{S''_j \vert j \in J\}\), any set of maps, \(\{f_j \vert j \in J\}\), such that \(f_j: S_j \to S'_j\), any set of maps, \(\{f'_j \vert j \in J\}\), such that \(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))\), and \(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: Proof 2
Whole Strategy: Step 1: see that \(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\) indeed makes sense; Step 2: see what \(f'_1 \times ... \times f'_n \circ f_1 \times ... \times f_n\) maps \(p = (p_1, ..., p_n)\) to; Step 3: see what \(f'_1 \circ f_1 \times ... \times f'_n \circ f_n\) maps \(p = (p_1, ..., p_n)\) to; Step 4: conclude the proposition.
Step 1:
Let us see that \(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\) indeed makes sense.
\(f'_j \circ f_j: S_j \to S''_j\).
So, \(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\) makes sense, according to the definition of project map. It is \(: (p_1, ..., p_n) \mapsto (f'_1 \circ f_1 (p_1), ..., f'_n \circ f_n (p_n))\).
Step 2:
Let \(p = (p_1, ..., p_n) \in S_1 \times ... \times S_n\) be any.
Let us see what \(f'_1 \times ... \times f'_n \circ f_1 \times ... \times f_n\) maps \(p\) to.
\(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))\).
Step 3:
Let \(p = (p_1, ..., p_n) \in S_1 \times ... \times S_n\) be any.
Let us see what \(f'_1 \circ f_1 \times ... \times f'_n \circ f_n\) maps \(p\) to.
\(p \mapsto (f'_1 \circ f_1 (p_1), ..., f'_n \circ f_n (p_n))\).
Step 4:
Step 2 and Step 3 have shown that the 2 maps map \(p\) to the same point, so, the 2 maps are the same.
