Now you are in the subtree of Container for Linear Algebra project. 

The dimension of the domain of an injective linear transformation is at most the dimension of the codomain.