What would synthetic linear algebra look like?

Question

I'm aware of synthetic mathematical fields like synthetic differential geometry and synthetic topology where the area is developed axiomatically rather than deriving everything analytically from a foundation of sets.

So I'm wondering if a synthetic linear algebra would make sense or if that's trivial. Is linear type theory essentially the same thing?

Answer 1

J.N. Oliveira and friends have a number of papers that give an axiomatisation of linear algebra.

The important observation is that matrices cannot be arbitrarily multiplied and as such do not form monoids, so the traditional mathematical approach of using monoids, groups, rings, fields does not easily apply here.

Matrices have types, or dimensions, that specify when they can be multiplied.

Slogan: Categories are Typed Monoids!

One rather accessible paper might well be Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra, or see http://www4.di.uminho.pt/~jno/html/jnopub.html for more similar such papers.

The abstract of the mentioned paper includes:

Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective [...]

From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.

Answer 2

It would look like something out of principia. Instead of vectors being coordinated, one would have to define linear operators in terms of basic "geometric algebra".