description/proof of that for set of sequences for fixed domain and codomain, permutation bijectively maps set onto set
Topics
About: set
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Proof
- 4: Note
Starting Context
- The reader knows a definition of permutation of sequence.
Target Context
- The reader will have a description and a proof of the proposition that for the set of all the sequences for any fixed domain and any fixed codomain, any permutation bijectively maps the set onto the 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:
\(S\): \(\subseteq \mathbb{N}\), \(= \{l_1, ..., l_k\}\)
\(S'\): \(\in \{\text{ the sets }\}\)
\(S''\): \(= \{f \vert f: S \to S' \in \{\text{ the sequences over } S\}\}\)
\(\sigma\): \(\in \{\text{ the permutations of an } f_0 \in S''\}\), \(: S \to S\)
\(f_\sigma\): \(S'' \to S'', f \mapsto f \circ \sigma\)
//
Statements:
\(f_\sigma \in \{\text{ the bijections }\}\).
//
2: Natural Language Description
For any subset, \(S \subseteq \mathbb{N} = \{l_1, ..., l_k\}\), any set, \(S'\), the set of all the sequences, \(S'' = \{f \vert f: S \to S'\}\), and any permutation, \(\sigma: S \to S\) of any \(f_0 \in S''\), \(f_\sigma: S'' \to S'', f \mapsto f \circ \sigma\) is a bijection.
3: Proof
\(f_\sigma\) is well-defined, because \(f \circ \sigma: S \to S \to S' \in S''\).
Let us prove that \(f_\sigma\) is injective. For any \(f \neq f' \in S''\), \(f \circ \sigma \neq f' \circ \sigma\), because if \(f \circ \sigma = f' \circ \sigma\), \(f = f \circ \sigma \circ {\sigma}^{-1} = f' \circ \sigma \circ {\sigma}^{-1} = f'\), a contradiction.
Let us prove that \(f_\sigma\) is surjective. For any \(f' \in S''\), \(f' \circ {\sigma}^{-1} \in S''\) and \(f' \circ {\sigma}^{-1} \circ \sigma = f'\).
4: Note
Typically, \(S = \{1, ..., k\}\) and \(S' = \{1, ..., d\}\) and we think of \(\sum_{(j_1, ..., j_k) \in S''} N^{j_1, ..., j_k} M_{j_1, ..., j_k}\), which is nothing but \(N^{j_1, ..., j_k} M_{j_1, ..., j_k}\) with the Einstein convention. What this proposition implies is that \(\sum_{(j_1, ..., j_k) \in S''} N^{\sigma ((j_1, ..., j_k))_1, ..., \sigma ((j_1, ..., j_k))_k} M_{\sigma ((j_1, ..., j_k))_1, ..., \sigma ((j_1, ..., j_k))_k} = N^{j_1, ..., j_k} M_{j_1, ..., j_k}\). That fact is usually immediately accepted as obvious, but we have bothered to prove it rigorously.
