nLab FinDimVect




The category of finite dimensional vector spaces and linear functions between them.

A compact closed monoidal category


Splitting lemma

The splitting lemma says that ever short exact sequence of vector spaces splits so that (in categorification of the rank-nullity theorem) every linear map f:DCf \,\colon\, D \to C is equivalent to

f:ker(f)im(f)(0,ι im(f))C, f \;\colon\; ker(f) \oplus im(f) \xrightarrow{ (0 , \iota_{im(f)}) } C \,,


  • ker(f)ι ker(f)Dker(f) \xrightarrow{\iota_{ker(f)}} D is the kernel

  • im(f)ι im(f)Cim(f) \xrightarrow{\iota_{im(f)}} C is the image

of ff.

Fiber (co)products

The cartesian product in FinDimVectFinDimVect is a biproduct given by direct sum of vector spaces.

More generally, the fiber product of a pair of linear maps is given by the direct sum of their kernels and of the intersection of their images:

The coproduct in the slice category FinDimVect /BFinDimVect_{/B} is given (by general facts) as the coproducts, hence the direct sum, of the domains, equipped with the induced maps to the base.

Applying (-1)-truncation to this fiber-wise coproduct of a pair of linear monomorphisms yields the linear span in BB of the two subspaces:

In summary this means that the internal logic of slices of FinDimVectFinDimVect is a Birkhoff-vonNeumann quantum logic.


Discussion of linear algebra in FinDimVectFinDimVect as categorical semantics for linear logic:

Last revised on September 18, 2023 at 21:41:07. See the history of this page for a list of all contributions to it.