Physlib

QuantumInfo.Channels.CPTP

Completely Positive Trace Preserving maps

A `CPTPMap` is a `ℂ`-linear map between matrices (`MatrixMap` is an alias), bundled with the facts that it `IsCompletelyPositive` and `IsTracePreserving`. CPTP maps are typically regarded as the "most general quantum operation", as they map density matrices (`MState`s) to density matrices. The type `PTPMap`, for maps that are positive (but not necessarily completely positive) is also declared.

A large portion of the theory is in terms of the Choi matrix (`MatrixMap.choi_matrix`), as the positive-definiteness of this matrix corresponds to being a CP map. This is [Choi's theorem on CP maps](https://en.wikipedia.org/wiki/Choi%27s_theorem_on_completely_positive_maps).

This file also defines several important examples of, classes of, and operations on, CPTPMaps: * `compose`: Composition of maps * `id`: The identity map * `replacement`: The replacement channel that always outputs the same state * `prod`: Tensor product of two CPTP maps, with notation M₁ ⊗ M₂ * `piProd`: Tensor product of finitely many CPTP maps (Pi-type product) * `of_unitary`: The CPTP map corresponding to a unitary operation `U` * `IsUnitary`: Predicate whether the map corresponds to any unitary * `purify`: Purifying a channel into a unitary on a larger Hilbert space * `complementary`: The complementary channel to its purification * `IsEntanglementBreaking`, `IsDegradable`, `IsAntidegradable`: Entanglement breaking, degradable and antidegradable channels. * `SWAP`, `assoc`, `assoc'`, `traceLeft`, `traceRight`: The CPTP maps corresponding to important operations on states. These correspond directly to `MState.SWAP`, `MState.assoc`, `MState.assoc'`, `MState.traceLeft`, and `MState.traceRight`.

4 declarations

theorem

(Λ1⊗Λ2)(ρ1⊗ρ2)=Λ1(ρ1)⊗Λ2(ρ2)(\Lambda_1 \otimes \Lambda_2)(\rho_1 \otimes \rho_2) = \Lambda_1(\rho_1) \otimes \Lambda_2(\rho_2)

Let Λ1\Lambda_1 and Λ2\Lambda_2 be completely positive trace-preserving (CPTP) maps acting on mixed states of dimensions dI1d_{I_1} and dI2d_{I_2} respectively. For any two mixed states (density matrices) ρ1\rho_1 and ρ2\rho_2, the application of the tensor product map Λ1⊗Λ2\Lambda_1 \otimes \Lambda_2 to the product state ρ1⊗ρ2\rho_1 \otimes \rho_2 is equal to the tensor product of the maps applied individually to each state: (Λ1⊗Λ2)(ρ1⊗ρ2)=Λ1(ρ1)⊗Λ2(ρ2)(\Lambda_1 \otimes \Lambda_2)(\rho_1 \otimes \rho_2) = \Lambda_1(\rho_1) \otimes \Lambda_2(\rho_2)

theorem

⨂i∈ιidi=id\bigotimes_{i \in \iota} \text{id}_i = \text{id}

Let ι\iota be an index set and {dIi}i∈ι\{dI_i\}_{i \in \iota} be a family of finite types representing dimensions of Hilbert spaces. For each i∈ιi \in \iota, let iddIi\text{id}_{dI_i} denote the identity CPTP map on the space of matrices over dIidI_i. Then the tensor product of these identity maps, ⨂i∈ιiddIi\bigotimes_{i \in \iota} \text{id}_{dI_i}, is equal to the identity CPTP map id∏i∈ιdIi\text{id}_{\prod_{i \in \iota} dI_i} on the space of matrices over the product type ∏i∈ιdIi\prod_{i \in \iota} dI_i.

theorem

Λ\Lambda is Unitary iff Λ(ρ)=UρU†\Lambda(\rho) = U \rho U^\dagger for some Unitary UU

A completely positive trace-preserving (CPTP) map Λ\Lambda on the space of density matrices of dimension dd is unitary if and only if there exists a unitary matrix UU such that for every density matrix ρ\rho, the action of the map is given by unitary conjugation, Λ(ρ)=UρU†\Lambda(\rho) = U \rho U^\dagger.

theorem

Matrix Entries of the Stinespring Preparation (id⊗Rτ)∘append(\text{id} \otimes \mathcal{R}_\tau) \circ \text{append}

Let dInd_{In} and dOutd_{Out} be finite types. Let X∈MatdIn(C)X \in \text{Mat}_{d_{In}}(\mathbb{C}) be a complex matrix. Let τ=∣default⟩⟨default∣\tau = |default\rangle\langle default| be the pure state density matrix on the space dOut×dOutd_{Out} \times d_{Out} corresponding to the default basis element. Let Λappend:MatdIn(C)→MatdIn×Unit(C)\Lambda_{append} : \text{Mat}_{d_{In}}(\mathbb{C}) \to \text{Mat}_{d_{In} \times \text{Unit}}(\mathbb{C}) be the CPTP map induced by the index equivalence dIn≃dIn×Unitd_{In} \simeq d_{In} \times \text{Unit}. Let Λprep=id⊗Rτ\Lambda_{prep} = \text{id} \otimes \mathcal{R}_\tau be the tensor product of the identity map on MatdIn(C)\text{Mat}_{d_{In}}(\mathbb{C}) and the replacement channel Rτ:MatUnit(C)→MatdOut×dOut(C)\mathcal{R}_\tau: \text{Mat}_{\text{Unit}}(\mathbb{C}) \to \text{Mat}_{d_{Out} \times d_{Out}}(\mathbb{C}) that always outputs τ\tau. Then the matrix entries of the composition (Λprep∘Λappend)(X)(\Lambda_{prep} \circ \Lambda_{append})(X) satisfy: ((Λprep∘Λappend)(X))(a1,v1),(a2,v2)=Xa1,a2⋅τv1,v2 ((\Lambda_{prep} \circ \Lambda_{append})(X))_{(a_1, v_1), (a_2, v_2)} = X_{a_1, a_2} \cdot \tau_{v_1, v_2} for all a1,a2∈dIna_1, a_2 \in d_{In} and v1,v2∈dOut×dOutv_1, v_2 \in d_{Out} \times d_{Out}.