linear algebra, higher linear algebra
(…)
The category of finite dimensional vector spaces and linear functions between them.
A compact closed monoidal category
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
where
$ker(f) \xrightarrow{\iota_{ker(f)}} D$ is the kernel
$im(f) \xrightarrow{\iota_{im(f)}} C$ is the image
of $f$.
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.
Discussion of linear algebra in $FinDimVect$ as categorical semantics for linear logic:
Last revised on April 8, 2023 at 12:08:32. See the history of this page for a list of all contributions to it.