nLab FinDimVect

Idea

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

A compact closed monoidal category

Properties

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 \,\colon\, D \to C$ is equivalent to

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

where

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

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

of $f$.

Fiber (co)products

The cartesian product in $FinDimVect$ 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_{/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 $B$ of the two subspaces:

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

Related concepts

• Vect

• sFinVect

• quantum information theory$\;$in terms of dagger-compact categories

• linear logic

References

Discussion of linear algebra in $FinDimVect$ as categorical semantics for linear logic:

• Daniel Murfet, Logic and linear algebra: an introduction [arXiv:1407.2650]