description/proof of that 'vectors spaces - linear morphisms' isomorphism is map that maps basis onto basis bijectively and expands mapping linearly
Topics
About: vectors space
The table of contents of this article
Starting Context
- The reader knows a definition of %field name% vectors space.
- The reader knows a definition of %category name% isomorphism.
- The reader knows a definition of basis of module.
- The reader admits the proposition that for any 'vectors spaces - linear morphisms' isomorphism, the image of any linearly independent subset or any basis of the domain is linearly independent or a basis on the codomain.
Target Context
- The reader will have a description and a proof of the proposition that any 'vectors spaces - linear morphisms' isomorphism is a map that maps any basis onto a basis bijectively and expands the mapping linearly.
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:
\(F\): \(\in \{\text{ the fields }\}\)
\(V_1\): \(\in \{\text{ the } F \text{ vectors spaces }\}\)
\(V_2\): \(\in \{\text{ the } F \text{ vectors spaces }\}\)
\(f\): \(: V_1 \to V_2\), \(\in \{\text{ the 'vectors spaces - linear morphisms' isomorphisms }\}\)
\(J\): \(\in \{\text{ the possibly uncountable index sets }\}\)
\(B_1\): \(= \{{b_1}_j \vert j \in J\}\), \(\in \{\text{ the bases for } V_1\}\)
//
Statements:
\(B_2 := f (B_1) \in \{\text{ the bases for } V_2\}\)
\(\land\)
\(f \vert_{B_1}: B_1 \to B_2 \in \{\text{ the bijections }\}\)
\(\land\)
\(\forall v \in V_1 (\exists S \in \{\text{ the finite subsets of } J\} (v = \sum_{j \in S} v^j {b_1}_j) \land f (v) = \sum_{j \in S} v^j f ({b_1}_j))\)
//
2: Note
Each of \(V_1\) and \(V_2\) does not need to be finite-dimensional.
3: Proof
Whole Strategy: Step 1: see that \(f (B_1)\) is a basis for \(V_2\), by the proposition that for any 'vectors spaces - linear morphisms' isomorphism, the image of any linearly independent subset or any basis of the domain is linearly independent or a basis on the codomain; Step 2: see that \(f \vert_{B_1}: B_1 \to B_2\) is a bijection; Step 3: see that for each \(v \in V_1\), \(v = \sum_{j \in S} v^j {b_1}_j\) for a finite \(S \subseteq J\) and \(f (v) = \sum_{j \in S} v^j f ({b_1}_j)\).
Step 1:
\(B_2 := f (B_1)\) is a basis for \(V_2\), by the proposition that for any 'vectors spaces - linear morphisms' isomorphism, the image of any linearly independent subset or any basis of the domain is linearly independent or a basis on the codomain.
Step 2:
\(f \vert_{B_1}: B_1 \to B_2\) is an injection, because \(f\) is an injection.
\(f \vert_{B_1}: B_1 \to B_2\) is a surjection, because \(B_2 = f (B_1)\).
So, \(f \vert_{B_1}: B_1 \to B_2\) is a bijection.
Step 3:
Let \(v \in V_1\) be any.
\(v = \sum_{j \in S} v^j {b_1}_j\) for a finite \(S \subseteq J\), by the definition of basis of module.
\(f (v) = \sum_{j \in S} v^j f ({b_1}_j)\), because any 'vectors spaces - linear morphisms' isomorphism is linear.
