Signs in objective linear algebra

Standard objective linear algebra works with slice categories instead of
vector spaces and with colimit- preserving functors instead of linear maps.
(Such functors are represented by spans, so that matrix multiplication
becomes pullback composition of spans.) This is useful in algebraic
combinatorics, although the amount of linear algebra that can be carried
out in this setting is quite limited. One serious limitation is the absence
of negatives. In this talk, I will explain how this can be overcome,
outlining an objective theory of signs in linear algebra. It turns out one
can maintain a nice topos flavour by not having the signs directly on the
objects but rather on 'states' (for a monoidal structure which is not the
cartesian product). By using groupoid coefficients instead of set
coefficients, the signs can be encoded as homotopies, and some of the sign
rules can be derived rather than stipulated. I will illustrate some of the
features of the theory with an objective treatment of exterior powers.

Joint work with Jesper Møller