763: Composition of Product Maps Is Product of Compositions of Component Maps

<The previous article in this series | The table of contents of this series | The next article in this series>

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 }|\alpha \in A\}$: $S_{\alpha }\in \{\text{ the sets }\}$
$\{S_{\alpha }^{\prime }|\alpha \in A\}$: $S_{\alpha }^{\prime }\in \{\text{ the sets }\}$
$\{S_{\alpha }^{″}|\alpha \in A\}$: $S_{\alpha }^{″}\in \{\text{ the sets }\}$
$\{f_{\alpha }|\alpha \in A\}$: $f_{\alpha }:S_{\alpha }\to S_{\alpha }^{\prime }$
$\{f_{\alpha }^{\prime }|\alpha \in A\}$: $f_{\alpha }^{\prime }:S_{\alpha }^{\prime }\to S_{\alpha }^{″}$
${\times }_{\alpha \in A}{f}_{\alpha }$: $:{\times }_{\alpha \in A}{S}_{\alpha }\to {\times }_{\alpha \in A}{S}_{\alpha }^{\prime },(\alpha \mapsto f(\alpha ))\mapsto (\alpha \mapsto f_{\alpha }(f(\alpha )))$
${\times }_{\alpha \in A}{f}_{\alpha }^{\prime }$: $:{\times }_{\alpha \in A}{S}_{\alpha }^{\prime }\to {\times }_{\alpha \in A}{S}_{\alpha }^{″},(\alpha \mapsto f(\alpha ))\mapsto (\alpha \mapsto f_{\alpha }^{\prime }(f(\alpha )))$
//

Statements:
${\times }_{\alpha \in A}{f}_{\alpha }^{\prime }\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 }^{\prime }\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 }|\alpha \in A\}$, any set of sets, $\{S_{\alpha }^{\prime }|\alpha \in A\}$, any set of sets, $\{S_{\alpha }^{″}|\alpha \in A\}$, any set of maps, $\{f_{\alpha }|\alpha \in A\}$, such that $f_{\alpha }:S_{\alpha }\to S_{\alpha }^{\prime }$, any set of maps, $\{f_{\alpha }^{\prime }|\alpha \in A\}$, such that $f_{\alpha }^{\prime }:S_{\alpha }^{\prime }\to S_{\alpha }^{″}$, ${\times }_{\alpha \in A}{f}_{\alpha }:{\times }_{\alpha \in A}{S}_{\alpha }\to {\times }_{\alpha \in A}{S}_{\alpha }^{\prime },(\alpha \mapsto f(\alpha ))\mapsto (\alpha \mapsto f_{\alpha }(f(\alpha )))$, and ${\times }_{\alpha \in A}{f}_{\alpha }^{\prime }:{\times }_{\alpha \in A}{S}_{\alpha }^{\prime }\to {\times }_{\alpha \in A}{S}_{\alpha }^{″},(\alpha \mapsto f(\alpha ))\mapsto (\alpha \mapsto f_{\alpha }^{\prime }(f(\alpha )))$, ${\times }_{\alpha \in A}{f}_{\alpha }^{\prime }\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 }^{\prime }\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 }^{\prime }\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 }^{\prime }\circ {\times }_{\alpha \in A}{f}_{\alpha }$ maps $p=(\alpha \mapsto f(\alpha ))$ to; Step 3: see what ${\times }_{\alpha \in A}{f}_{\alpha }^{\prime }\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 }^{\prime }\circ f_{\alpha }:{\times }_{\alpha \in A}{S}_{\alpha }\to {\times }_{\alpha \in A}{S}_{\alpha }^{″}$ indeed makes sense.

$f_{\alpha }^{\prime }\circ f_{\alpha }:S_{\alpha }\to S_{\alpha }^{″}$.

So, ${\times }_{\alpha \in A}{f}_{\alpha }^{\prime }\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 }^{\prime }\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 }^{\prime }\circ {\times }_{\alpha \in A}{f}_{\alpha }$ maps $p$ to.

$p\mapsto (\alpha \mapsto f_{\alpha }(f(\alpha )))\mapsto (\alpha \mapsto f_{\alpha }^{\prime }\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 }^{\prime }\circ f_{\alpha }$ maps $p$ to.

$p\mapsto (\alpha \mapsto f_{\alpha }^{\prime }\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|j\in J\}$: $S_j\in \{\text{ the sets }\}$
$\{S_j^{\prime }|j\in J\}$: $S_j^{\prime }\in \{\text{ the sets }\}$
$\{S_j^{″}|j\in J\}$: $S_j^{″}\in \{\text{ the sets }\}$
$\{f_j|j\in J\}$: $f_j:S_j\to S_j^{\prime }$
$\{f_j^{\prime }|j\in J\}$: $f_j^{\prime }:S_j^{\prime }\to S_j^{″}$
$f_1\times ...\times f_n$: $:S_1\times ...\times S_n\to S_1^{\prime }\times ...\times S_n^{\prime },(p_1,...,p_n)\mapsto (f_1(p_1),,...,f_n(p_n))$
$f_1^{\prime }\times ...\times f_n^{\prime }$: $:S_1^{\prime }\times ...\times S_n^{\prime }\to S_1^{″}\times ...\times S_n^{″},(p_1,...,p_n)\mapsto (f_1^{\prime }(p_1),,...,f_n^{\prime }(p_n))$
//

Statements:
$f_1^{\prime }\times ...\times f_n^{\prime }\circ f_1\times ...\times f_n:S_1\times ...\times S_n\to S_1^{″}\times ...\times S_n^{″}=f_1^{\prime }\circ f_1\times ...\times f_n^{\prime }\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|j\in J\}$, any set of sets, $\{S_j^{\prime }|j\in J\}$, any set of sets, $\{S_j^{″}|j\in J\}$, any set of maps, $\{f_j|j\in J\}$, such that $f_j:S_j\to S_j^{\prime }$, any set of maps, $\{f_j^{\prime }|j\in J\}$, such that $f_j^{\prime }:S_j^{\prime }\to S_j^{″}$, $f_1\times ...\times f_n:S_1\times ...\times S_n\to S_1^{\prime }\times ...\times S_n^{\prime },(p_1,...,p_n)\mapsto (f_1(p_1),,...,f_n(p_n))$, and $f_1^{\prime }\times ...\times f_n^{\prime }:S_1^{\prime }\times ...\times S_n^{\prime }\to S_1^{″}\times ...\times S_n^{″},(p_1,...,p_n)\mapsto (f_1^{\prime }(p_1),,...,f_n^{\prime }(p_n))$, $f_1^{\prime }\times ...\times f_n^{\prime }\circ f_1\times ...\times f_n:S_1\times ...\times S_n\to S_1^{″}\times ...\times S_n^{″}=f_1^{\prime }\circ f_1\times ...\times f_n^{\prime }\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^{\prime }\circ f_1\times ...\times f_n^{\prime }\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^{\prime }\times ...\times f_n^{\prime }\circ f_1\times ...\times f_n$ maps $p=(p_1,...,p_n)$ to; Step 3: see what $f_1^{\prime }\circ f_1\times ...\times f_n^{\prime }\circ f_n$ maps $p=(p_1,...,p_n)$ to; Step 4: conclude the proposition.

Step 1:

Let us see that $f_1^{\prime }\circ f_1\times ...\times f_n^{\prime }\circ f_n:S_1\times ...\times S_n\to S_1^{″}\times ...\times S_n^{″}$ indeed makes sense.

$f_j^{\prime }\circ f_j:S_j\to S_j^{″}$.

So, $f_1^{\prime }\circ f_1\times ...\times f_n^{\prime }\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^{\prime }\circ f_1(p_1),...,f_n^{\prime }\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^{\prime }\times ...\times f_n^{\prime }\circ f_1\times ...\times f_n$ maps $p$ to.

$p\mapsto (f_1(p_1),,...,f_n(p_n))\mapsto (f_1^{\prime }\circ f_1(p_1),,...,f_n^{\prime }\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^{\prime }\circ f_1\times ...\times f_n^{\prime }\circ f_n$ maps $p$ to.

$p\mapsto (f_1^{\prime }\circ f_1(p_1),...,f_n^{\prime }\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.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>