Diagram of different types of Linear Maps in Mathlib

Stream: mathlib4

[Niels Voss]

I was having a bit of trouble wrapping my mind around the 18 different types of (semi)linear maps in mathlib, so I decided to make this diagram using Obsidian's Canvas. I can't guarantee that it's accurate, and it's not the most general it could be, but maybe it will be helpful to at least one person.

Linear Maps in Lean.png

(Here's the .json source in case anyone wants it:
Linear Maps in Lean.canvas

[Alex Meiburg]

Not sure if you want these, but there's also docs#PositiveLinearMap and docs#CompletelyPositiveMap !

[Niels Voss]

Do PositiveLinearMap and CompletelyPositiveMap have any relation whatsoever to LinearMap.IsPositive?

[Alex Meiburg]

Not much relation, since they require different data... PositiveLinearMaps require an ordering on the input and output vector spaces; LinearMap.IsPositive requires an inner product structure.

The most common instance of the ordering on the vector space would be looking at the vector space of R-valued matrices, and the Loewner order. Then the positive elements are the positive semidefinite matrices. Matrices also have the Frobenius inner product, and then the inner product of two positive semidefinite matrices is always positive. So, for this particular ordering and this particular inner product, every PositiveLinearMap also IsPositive. (You can also talk about this for linear operators, instead of just matrices, of course.)

The converse is not true: there are IsPositive linear maps between spaces of matrices that are not PositiveLinearMaps.

CompletelyPositiveMap is a strengthening of PositiveLinearMap that requires it stays a PositiveLinearMap under tensor products with the identity. It turns out that, if you write down the matrix elements of a CompletelyPositiveMap, they correspond directly to the matrix elements of IsPositive maps, and this is known as Choi's theorem. By 'correspond directly' I mean that it's a linear isometry to convert between these two sets.

But the funny thing is that it's not writing down "the matrix elements" in the same basis ... because as I said before, every CompletelyPositiveMap is a PositiveLinearMap, and there are IsPositive maps that aren't PositiveLinearMap, so it's not that CompletelyPositiveMap = IsPositive. Since we're talking about linear maps from matrices to matrices, the matrix elements are generally labelled by 4 indices, and there's sort of two different reasonable ways to organize it then. And, _in the correct two distinct organizations of this data_, CompletelyPositiveMap and IsPositive are the same.

[Alex Meiburg]

To make things worse, there is a notion of Completely Positive Matrix which as far as I know is not in Mathlib. It crops up in optimization theory and polyhedral complexity stuff. They're the dual cone to the Copositive Matrix.

Now, I mentioned how PositiveLinearMap requires an ordering on the input and output vector spaces. The notion of Completely Positive Matrix appears when you equip the vector space ℝ^n with the "component-wise ordering": like, (x1,y1,z1) ≤ (x2,y2,z2) ↔ (x1 ≤ x2) ∧ (y1 ≤ y2) ∧ (z1 ≤ z2). With that ordering, every completely positive matrix is also PositiveLinearMap, and every PositiveLinearMap is copositive. Both of these inclusions are strict. This also happens to be an ordering+inner product pair where every PositiveLinearMap also IsPositive, although again, this isn't always true.

[Alex Meiburg]

That might've been more than you wanted to know :)