description/proof of that for linear map between modules with bases, if its restriction on domain basis is bijection onto codomain basis, map is 'modules - linear morphisms' isomorphism
Topics
About: module
The table of contents of this article
Starting Context
- The reader knows a definition of basis of module.
- The reader knows a definition of linear map.
- The reader knows a definition of bijection.
- The reader knows a definition of %category name% isomorphism.
- The reader admits the proposition that for any module with any basis, the components set of any element with respect to the basis is unique.
- The reader admits the proposition that any bijective linear map between any modules is a 'modules - linear morphisms' isomorphism.
Target Context
- The reader will have a description and a proof of the proposition that for any linear map between any modules with bases, if its restriction on any domain basis is a bijection onto any codomain basis, the map is a 'modules - linear morphisms' isomorphism.
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:
\(R\): \(\in \{\text{ the rings }\}\)
\(M_1\): \(\in \{\text{ the } R \text{ modules }\}\)
\(M_2\): \(\in \{\text{ the } R \text{ modules }\}\)
\(J_1\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(J_2\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(B_1\): \(= \{b_{1, j} \vert j \in J_1\}\), \(\in \{\text{ the bases for } M_1\}\)
\(B_2\): \(= \{b_{2, j} \vert j \in J_2\}\), \(\in \{\text{ the bases for } M_2\}\)
\(f\): \(: M_1 \to M_2\)
//
Statements:
\(f (B_1) = B_2 \land f \vert_{B_1}: B_1 \to B_2 \in \{\text{ the bijections }\}\)
\(\implies\)
\(f \in \{\text{ the 'modules - linear morphisms' isomorphisms }\}\)
//
2: Proof
Whole Strategy: Step 1: see that \(f\) is injective; Step 2: see that \(f\) is surjective; Step 3: conclude the proposition.
Step 1:
Let us see that \(f\) is injective.
Let \(m, m' \in M_1\) be any such that \(m \neq m'\).
There are a finite \(S \subseteq J_1\) such that \(m = \sum_{j \in S} m^j b_{1, j}\) and a finite \(S' \subseteq J_1\) such that \(m' = \sum_{j \in S'} m'^j b_{1, j}\).
Let us take \(S \cup S'\) and for each \(j \in S \cup S'\), \(\widetilde{m}^j = m^j\) for \(j \in S\) and \(\widetilde{m}^j = 0\) for \(j \notin S\) and \(\widetilde{m'}^j = m'^j\) for \(j \in S'\) and \(\widetilde{m'}^j = 0\) for \(j \notin S'\).
\(m = \sum_{j \in S \cup S'} \widetilde{m}^j b_{1, j}\) and \(m' = \sum_{j \in S \cup S'} \widetilde{m'}^j b_{1, j}\).
As \(m \neq m'\), \(\widetilde{m}^l \neq \widetilde{m'}^l\) for a \(l \in S \cup S'\).
\(f (m) = f (\sum_{j \in S \cup S'} \widetilde{m}^j b_{1, j}) = \sum_{j \in S \cup S'} \widetilde{m}^j f (b_{1, j})\), because \(f\) is linear.
\(f (m') = f (\sum_{j \in S \cup S'} \widetilde{m'}^j b_{1, j}) = \sum_{j \in S \cup S'} \widetilde{m'}^j f (b_{1, j})\), because \(f\) is linear.
As \(f (B_1) = B_2\), each \(f (b_{1, j})\) is an element of \(B_2\), and as \(f \vert_{B_1}\) is bijective, \(\{f (b_{1, j}) \vert j \in S \cup S'\}\) is distinct.
As \(\widetilde{m}^l \neq \widetilde{m'}^l\), \(f (m) = \sum_{j \in S \cup S'} \widetilde{m}^j f (b_{1, j}) \neq \sum_{j \in S \cup S'} \widetilde{m'}^j f (b_{1, j}) = f (m')\), by the proposition that for any module with any basis, the components set of any element with respect to the basis is unique.
Step 2:
Let \(m \in M_2\) be any.
There is a finite \(S \subseteq J_2\) such that \(m = \sum_{j \in S} m^j b_{2, j}\).
As \(f \vert_{B_1}: B_1 \to B_2\) is bijective, there is the inverse, \({f \vert_{B_1}}^{-1}: B_2 \to B_1\). So, \({f \vert_{B_1}}^{-1} (b_{2, j}) \in B_1\).
Let us think of \(\sum_{j \in S} m^j {f \vert_{B_1}}^{-1} (b_{2, j}) \in M_1\).
\(f (\sum_{j \in S} m^j {f \vert_{B_1}}^{-1} (b_{2, j})) = \sum_{j \in S} m^j f ({f \vert_{B_1}}^{-1} (b_{2, j}))\), because \(f\) is linear, \(= \sum_{j \in S} m^j b_{2, j} = m\).
So, \(f\) is surjective.
Step 3:
By the proposition that any bijective linear map between any modules is a 'modules - linear morphisms' isomorphism, \(f\) is a 'modules - linear morphisms' isomorphism.
