Basis-Equipped FinVect as a Kleisli Category

The slogan “a matrix is a linear map once you fix bases” has a clean categorical form. Basis-equipped finite vector spaces are the Kleisli category of the free-vector-space monad. This note pins down the equivalence and uses it as the “sameness” backdrop against which product coproduct in FinVect is read.

The free-vector-space monad

Let be the free functor and the underlying-set functor. The adjunction has unit picking out the standard basis and counit summing a formal combination to a vector. It therefore induces the monad on , where is the set of finite formal -combinations of elements of .

The equivalence

Proposition. Basis-equipped FinVect is Kleisli

The Kleisli category is equivalent to the category of basis-equipped finite-dimensional vector spaces, equivalently to . Its objects are finite sets, and a morphism is a function , that is a matrix. The comparison is the free functor one way and coordinate reading the other. A Kleisli map is exactly a matrix, and Kleisli composition is matrix multiplication.

Why this is the “sameness” backdrop

Remark. A basis fixes what "the same" means

Choosing a basis is choosing the coordinate section . Two spaces are then “the same” iff they share a dimension, and every isomorphism is a change of basis. Against this backdrop the collapse of product and coproduct into a biproduct looks less like a coincidence of and more like a feature of the Kleisli presentation, since the free monad is additive and its Kleisli category inherits finite biproducts.