Theorem KNSI and Theorem RCSI have two of the most subtle proofs we have seen so far. The conclusion that two vector spaces are isomorphic is established by actually constructing an isomorphism between the vector spaces. To build the isomorphism, we begin with a familar object, a vector representation linear transformation, but the hard work is showing that we can “restrict” the domain and codomain of this function and still arrive at a legitimate (invertible) linear transformation. In an effort to make the proofs more concrete, we will walk through a nontrivial example for Theorem KNSI, and you might try to do the same for Theorem RCSI. (An understanding of this subsection is not needed for the remainder — its second purpose is to demonstrate some of the powerful tools Sage provides.)
Here are the pieces. We build a linear transformation with two different representations, one with respect to standard bases, the other with respect to less-obvious bases.
Now we compute the kernel of the linear transformation using the “plain” version, and the null space of a matrix representation coming from the “fancy” version.
So quite obviously, the kernel of the linear transformation is quite different looking from the null space of the matrix representation. Though it is no accident that they have the same dimension. Now we build the necessary vector representation, and use two Sage commands to “restrict” the function to a smaller domain (the kernel of the linear transformation) and a smaller codomain (the null space of the matrix representation relative to nonstandard bases).
The first success is that the restriction was even created. Sage would recognize if the original linear transformation ever carried an input from the restricted domain to an output that was not contained in the proposed codomain, and would have raised an error in that event. Phew! Guaranteeing this success was the first big step in the proof of Theorem KNSI. Notice that the matrix representation of the restriction is a $3\times 3$ matrix, since the restriction runs between a domain and codomain that each have dimension 3. These two vector spaces (the domain and codomain of the restriction) have dimension 3 but still contain vectors with 5 entries in their un-coordinatized versions.
The next two steps of the proof show that the restriction is injective (easy in the proof) and surjective (hard in the proof). In Sage, here is the second success,
Verified as invertible, rho_restrict qualifies as an isomorphism between the linear transformation kernel, K, and the matrix representation null space, MK. Only an example, but still very nice. Your turn — can you create a verfication of Theorem RCSI (for this example, or some other nontrivial example you might create yourself)?