The definition of matrix (“the basis maps to:”) ought to come after the “uniquely determines the linear map” that justifies it.
For interpreting v as a slim matrix, I would use bra-ket notation: |v> for the function of type V ← R, <v| for the function whose type is the dual R ← V. Then <v|v> has type R ← R (and corresponds to multiplication by a scalar) and |v><v| has type V ← V.
An inner product just maps |v> to <v|. (Though I don’t quite see what the symmetry is for.)
Mapping a point cloud through a linear map thins it by a factor of the determinant; this generalizes to smooth maps, since they are locally linear.
The definition of matrix (“the basis maps to:”) ought to come after the “uniquely determines the linear map” that justifies it.
For interpreting v as a slim matrix, I would use bra-ket notation: |v> for the function of type V ← R, <v| for the function whose type is the dual R ← V. Then <v|v> has type R ← R (and corresponds to multiplication by a scalar) and |v><v| has type V ← V.
An inner product just maps |v> to <v|. (Though I don’t quite see what the symmetry is for.)
Mapping a point cloud through a linear map thins it by a factor of the determinant; this generalizes to smooth maps, since they are locally linear.