Semantics Club 23 02 2001

Two-dimensional linear algebra

John Power

(joint work with Martin Hyland)


We introduce two-dimensional linear algebra. For ordinary linear algebra, the fundamental object of study is the category Ab of Abelian groups, and the fundamental fact about Ab is that it is monadic over Set for a commutative monad. That implies that Ab is a symmetric monoidal closed category, with the forgetful functor to Set forming part of a symmetric monoidal closed adjunction. For two-dimensional linear algebra, the category SymMon of small symmetric monoidal categories plays the role of Ab, and Cat plays the role of Set. However, one does not have a commutative monad here, because a diagram that must commute does not in fact do so. So we need to develop a notion of pseudo-commutative 2-monad, then a notion of pseudo-closed 2-category, then prove that if T is a pseudo-commutative 2-monad on Cat, it follows that the 2-category of T-algebras is pseudo-closed. We also need to provide some independent indication that our definitions are robust. This work provides a unified framework for modelling various sorts of simply typed context such as linear contexts, ordinary contexts, and combinations of them, and provides a theoretical basis for some of the choices in axiomatic domain theory, action calculi, and the like.