QuantumInfo.Channels.Bundled

Classes of Matrix Maps

The bundled `MatrixMap`s: `HPMap`, `UnitalMap`, `TPMap`, `PMap`, and `CPMap`. These are defined over the bare minimum rings (`Semiring` or `RCLike`, respectively).

The combinations `PTPMap` (positive trace-preserving), `CPTPMap`, and `CPUMap` (CP unital maps) take ℂ as the default class.

The majority of quantum theory revolves around `CPTPMap`s, so those are explored more thoroughly in their file CPTP.lean.

Hermitian-preserving maps

Positive-preserving maps

Positive trace-preserving maps

Completely positive trace-preserving linear maps

1 declaration

instance

Hermitian-preserving maps are continuous $\mathbb{R}$ -linear maps between Hermitian matrix spaces

#instContinuousLinearMapClassComplexRealHermitianMatOfFintype

Let $d_{In}$ be a finite index set and $d_{Out}$ be an index set. A Hermitian-preserving map $\Lambda$ between complex matrix spaces (of type `HPMap dIn dOut ℂ`) is a continuous $\mathbb{R}$ -linear map when viewed as a function from the space of $d_{In} \times d_{In}$ Hermitian matrices, $\text{HermitianMat}(d_{In}, \mathbb{C})$ , to the space of $d_{Out} \times d_{Out}$ Hermitian matrices, $\text{HermitianMat}(d_{Out}, \mathbb{C})$ .