description/proof of that for finite indexed set of finite sets, disjointed union of indexed set, and commutative ring, product by disjointed union is product by index after products by elements of indexed set
Topics
About: ring
The table of contents of this article
Starting Context
- The reader knows a definition of disjointed union of indexed set of sets.
- The reader knows a definition of ring.
Target Context
- The reader will have a description and a proof of the proposition that for any finite indexed set of finite sets, the disjointed union of the indexed set, and any commutative ring, the product by the disjointed union is the product by the index after the products by the elements of the indexed set.
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
Here is the rules of Structured Description.
Entities:
\(J\): \(\in \{\text{ the finite index sets }\}\)
\(\{L_j \in \{\text{ the finite index sets }\}\}_{j \in J}\): \(\in \{\text{ the indexed sets }\}\)
\(R\): \(\in \{\text{ the commutative rings }\}\)
\(\{r_{j, l_j} \in R\}_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j}\):
//
Statements:
\(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j} = \prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\)
//
2: Note
\(R\) needs to be commutative, because otherwise, \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j}\) or \(\prod_{j \in J} \prod_{l_j \in L_j}\) would not be well-defined, because \(\cup_{j \in J} \{j\} \times L_j\), \(J\), or \(L_j\) was not particularly ordered.
\(J\) and each \(L_j\) needs to be finite, because otherwise, \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j}\) or \(\prod_{j \in J} \prod_{l_j \in L_j}\) would not be well-defined, because product of infinite number of factors is not defined.
3: Proof
Whole Strategy: Step 1: see that each of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) and \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) has only \(1\) term with \(r_{j, l_j}\) s as the factors; Step 2: see that each factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) appears as a factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) only once; Step 3: see that each factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) appears as a factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) only once; Step 4: conclude the proposition.
Step 1:
\(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) has only \(1\) term with \(r_{j, l_j}\) s as the factors.
\(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) has only \(1\) term with \(r_{j, l_j}\) s as the factors.
As \(R\) is commutative, the orders of the factors do not matter.
Note that we are going to distinguish the factors by the indexes, \((j, l_j)\) s: when \(r_{j, l_j} = r_{j', l'_{j'}}\), they cannot be distinguished by the values but we distinguish them by the indexes.
So, \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j} = \prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) if and only if each factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) appears as a factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) only once and each factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) appears as a factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) only once.
Step 2:
Let \(r_{j, l_j}\) be any factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\).
\((j, l_j) \in \cup_{j \in J} \{j\} \times L_j\).
\((j, l_j) \in \{j\} \times L_j\) for a \(j \in J\), so, \(l_j \in L_j\).
So, \(r_{j, l_j}\) appears as a factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\) only once.
Step 3:
Let \(r_{j, l_j}\) be any factor of \(\prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\).
\(r_{j, l_j}\) is a factor of \(\prod_{l_j \in L_j} r_{j, l_j}\).
So, \(r_{j, l_j}\) appears as a factor of \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j}\) only once.
Step 4:
So, \(\prod_{(j, l_j) \in \cup_{j \in J} \{j\} \times L_j} r_{j, l_j} = \prod_{j \in J} \prod_{l_j \in L_j} r_{j, l_j}\).
