Switch CPTPMap + more to "___Class"

[Timeroot]

There's the idea in Mathlib that you should have "XXXMap" and "XXXMapClass". For instance, a CPTPMap isn't itself literally a LinearMap (although it can be coerced to one), so some theorems won't apply; but if you instantiate it as a LinearMapClass then you get most of the benefit.

As it turns out, most of the properties we care about exist as Classes:

• LinearMap / LinearMapClass (on HermitianMat) are Hermitian-preserving maps
• OrderHom / OrderHomClass are positive maps
• OneHom / OneHomClass are unital maps
• the recent CompletelyPositiveMap / CompletelyPositiveMapClass are completely positive maps. They offer an OrderHomClass instance too.

The only feature missing, then, is trace-preserving maps, so that we need a TraceHom and TraceHomClass or similar. It would be great to redo ... well, pretty much the whole CPTPMap directory with this in mind. It will also break downstream stuff all over.

There's this unfortunate clash, though, where you can't have more than one DFunLike instance for a type, and so you can't have more than one LinearMapClass for a given type. So, if CPTPMap is a LinearMapClass on HermitianMat, then it can't also be one for Matrix.

I'm thinking about scrapping the "MatrixMap" (which is a LinearMap on Matrix) entirely, and just only ever using linear maps of HermitianMat. So that MatrixMap m n R -- maybe now better called HermMatMap m n R -- is defined as LinearMap R (HermitianMat m R) (HermitianMat n R). Then, we can have a coercion from HermMatMap to LinearMap, and some relevant extensionality lemmas. But this would advance the philosophy that most of quantum mechanics should be "type-safe" about Hermitian matrices wherever possible.

I have a branch for this called bundling but it's awful mess and it might be better just to start anew.