PhyslibSearch

QuantumInfo.Finite.CPTPMap.Dual

32 declarations

definition

The dual MM^* of a matrix map MM

#dual

Let RR be a semiring. For a matrix map M:MatdIn×dIn(R)MatdOut×dOut(R)M: \text{Mat}_{d_{In} \times d_{In}}(R) \to \text{Mat}_{d_{Out} \times d_{Out}}(R), its dual map M:MatdOut×dOut(R)MatdIn×dIn(R)M^* : \text{Mat}_{d_{Out} \times d_{Out}}(R) \to \text{Mat}_{d_{In} \times d_{In}}(R) is the unique linear map defined such that for all matrices AA and BB, the trace identity tr(M(A)B)=tr(AM(B))\text{tr}(M(A) B) = \text{tr}(A M^*(B)) holds. Formally, this is constructed by identifying the space of matrices with its dual space using the trace form and taking the algebraic dual of the linear map MM.

theorem

tr(M(A)B)=tr(AM(B))\text{tr}(M(A)B) = \text{tr}(A M^*(B)) for dual matrix maps

#trace_eq

Let RR be a semiring. For any matrix map M:MatdIn×dIn(R)MatdOut×dOut(R)M: \text{Mat}_{d_{In} \times d_{In}}(R) \to \text{Mat}_{d_{Out} \times d_{Out}}(R) and any matrices AMatdIn×dIn(R)A \in \text{Mat}_{d_{In} \times d_{In}}(R) and BMatdOut×dOut(R)B \in \text{Mat}_{d_{Out} \times d_{Out}}(R), the trace of the product of M(A)M(A) and BB is equal to the trace of the product of AA and the dual map MM^* applied to BB. That is, tr(M(A)B)=tr(AM(B))\text{tr}(M(A)B) = \text{tr}(A M^*(B)).

theorem

The dual of a Hermitian-preserving matrix map is Hermitian-preserving

#dual

Let MM be a matrix map. If MM is Hermitian-preserving, then its dual map MM^* is also Hermitian-preserving.

theorem

The trace of the product of two positive semidefinite matrices is non-negative

#trace_mul_nonneg

Let nn be a finite type with decidable equality, and let AA and BB be n×nn \times n matrices over a field k\mathbb{k} (typically R\mathbb{R} or C\mathbb{C}). If both AA and BB are positive semidefinite, then the trace of their product is non-negative, i.e., 0tr(AB)0 \le \text{tr}(AB).

theorem

The dual of a positive matrix map is positive

#dual

Let M:MatdIn×dIn(R)MatdOut×dOut(R)M: \text{Mat}_{d_{In} \times d_{In}}(R) \to \text{Mat}_{d_{Out} \times d_{Out}}(R) be a matrix map between matrices over a semiring RR. If MM is a positive map (meaning it maps positive semidefinite matrices to positive semidefinite matrices), then its dual map MM^* is also a positive map.

theorem

The dual of a trace-preserving matrix map is unital

#dual_Unital

Let MM be a matrix map. If MM is trace-preserving, then its dual map MM^* is unital, meaning M(I)=IM^*(I) = I where II is the identity matrix.

theorem

Uniqueness of Matrix Map Dual via Trace Duality Property

#dual_unique

Let k\mathbb{k} be a field. For any two matrix maps M:Matdin×din(k)Matdout×dout(k)M: \text{Mat}_{d_{in} \times d_{in}}(\mathbb{k}) \to \text{Mat}_{d_{out} \times d_{out}}(\mathbb{k}) and M:Matdout×dout(k)Matdin×din(k)M': \text{Mat}_{d_{out} \times d_{out}}(\mathbb{k}) \to \text{Mat}_{d_{in} \times d_{in}}(\mathbb{k}), if for all matrices AA and BB, the trace equality tr(M(A)B)=tr(AM(B))\text{tr}(M(A)B) = \text{tr}(A M'(B)) holds, then MM' is equal to the dual map MM^*.

theorem

The Choi matrix of the dual map MM^* is the reindexed transpose of the Choi matrix of MM.

#dual_choi_matrix

Let MM be a matrix map from matrices over dind_{in} to matrices over doutd_{out} with coefficients in a field k\mathbb{k}. The Choi matrix of the dual map MM^*, denoted C(M)\mathcal{C}(M^*), is equal to the transpose of the Choi matrix of the original map MM, C(M)T\mathcal{C}(M)^T, after reindexing the row and column indices using the product commutation equivalence (dout×din)(din×dout)(d_{out} \times d_{in}) \cong (d_{in} \times d_{out}). Specifically, C(M)=reindex(C(M)T)\mathcal{C}(M^*) = \text{reindex}(\mathcal{C}(M)^T) where the reindexing swaps the input and output components of the index pairs.

theorem

If C(M)\mathcal{C}(M) is positive semidefinite, then C(M)\mathcal{C}(M^*) is positive semidefinite

#dual_choi_matrix_posSemidef_of_posSemidef

Let MM be a matrix map between matrix spaces over dind_{in} and doutd_{out} with coefficients in a field k\mathbb{k}. If the Choi matrix of MM, denoted C(M)\mathcal{C}(M), is positive semidefinite, then the Choi matrix of its dual map MM^*, denoted C(M)\mathcal{C}(M^*), is also positive semidefinite.

theorem

The dual of the identity matrix map is the identity map

#dual_id

For any finite type dind_{in} and any field k\mathbb{k}, the dual of the identity matrix map id:Matdin(k)Matdin(k)\text{id} : \text{Mat}_{d_{in}}(\mathbb{k}) \to \text{Mat}_{d_{in}}(\mathbb{k}) is the identity matrix map itself. That is, (id)=id(\text{id})^* = \text{id}.

theorem

(MkmN)=MkmN(M \otimes_{km} N)^* = M^* \otimes_{km} N^*

#dual_kron

Let k\mathbb{k} be a field, and let A,B,C,DA, B, C, D be finite types with decidable equality. For any matrix maps M:MatA×A(k)MatB×B(k)M: \text{Mat}_{A \times A}(\mathbb{k}) \to \text{Mat}_{B \times B}(\mathbb{k}) and N:MatC×C(k)MatD×D(k)N: \text{Mat}_{C \times C}(\mathbb{k}) \to \text{Mat}_{D \times D}(\mathbb{k}), the dual of their Kronecker product MkmNM \otimes_{km} N is equal to the Kronecker product of their dual maps, MkmNM^* \otimes_{km} N^*. That is, (MkmN)=MkmN(M \otimes_{km} N)^* = M^* \otimes_{km} N^*.

theorem

The Dual of a Completely Positive Matrix Map is Completely Positive

#dual

Let MM be a matrix map between finite-dimensional spaces. If MM is completely positive, then its dual map MM^\dagger (or MM^* in some contexts) is also completely positive.

theorem

(ϕb1)ϕb=ev(\phi_b^{-1})^* \circ \phi_b = \text{ev}

#dualMap_toDualEquiv_symm_comp_toDualEquiv

Let RR be a commutative ring and MM a reflexive RR-module with a basis bb indexed by a finite set ι\iota. Let ϕb:MM\phi_b : M \cong M^* be the dual basis isomorphism induced by bb. Then the composition of the dual of the inverse isomorphism, (ϕb1):MM(\phi_b^{-1})^* : M^{**} \to M^*, with the isomorphism ϕb:MM\phi_b : M \to M^* satisfies (ϕb1)ϕb=ev(\phi_b^{-1})^* \circ \phi_b = \text{ev}, where ev:MM\text{ev} : M \to M^{**} is the canonical evaluation map into the double dual.

theorem

Φb1Φb=eval1\Phi_b^{-1} \circ \Phi_b^* = \text{eval}^{-1} for a reflexive module basis bb

#toDualEquiv_symm_comp_dualMap_toDualEquiv

Let RR be a commutative ring and MM be a reflexive module over RR with a finite basis bb indexed by ι\iota. Let Φb:MM\Phi_b: M \to M^\vee denote the isomorphisms to the dual space induced by the basis bb, and Φb1:MM\Phi_b^{-1}: M^\vee \to M its inverse. Let eval:MM\text{eval}: M \xrightarrow{\cong} M^{\vee\vee} be the natural evaluation isomorphism to the double dual. Then the composition of the inverse dual basis isomorphism with the dual of the dual basis isomorphism is the inverse of the evaluation map, i.e., Φb1Φb=eval1\Phi_b^{-1} \circ \Phi_b^* = \text{eval}^{-1} where Φb:MM\Phi_b^*: M^{\vee\vee} \to M^\vee is the dual map of Φb\Phi_b.

theorem

The operation of taking the dual of a `MatrixMap` is an involution, i.e., M=MM^{**} = M.

#dual_dual

For a matrix map MM acting between types dInd_{In} and dOutd_{Out} over a semiring RR, the dual of its dual is equal to MM itself, i.e., (M)=M(M^*)^* = M.

definition

The dual of a CPTP map is a CPU map MM^\dagger

#dual

Let MM be a completely positive and trace-preserving (CPTP) map from the space of matrices of dimension dind_{in} to the space of matrices of dimension doutd_{out} over C\mathbb{C}. The dual dual(M)\text{dual}(M) is defined as the adjoint (dual) linear map MM^\dagger. This map is a completely positive and unital (CPU) map from the space of matrices of dimension doutd_{out} to the space of matrices of dimension dind_{in}.

theorem

The dual of a CPTP map is positivity-preserving

#dual_pos

Let MM be a completely positive trace-preserving (CPTP) map from the space of din×dind_{in} \times d_{in} complex Hermitian matrices to the space of dout×doutd_{out} \times d_{out} complex Hermitian matrices. Let MM^\dagger (denoted as `M.dual`) be the dual map of MM, which is a completely positive unital (CPU) map. For any dout×doutd_{out} \times d_{out} Hermitian matrix TT, if TT is positive semi-definite (0T0 \le T), then its image under the dual map M(T)M^\dagger(T) is also positive semi-definite (0M(T)0 \le M^\dagger(T)).

theorem

The dual of a CPTP map preserves two-element POVMs (0T1    0M(T)10 \le T \le 1 \implies 0 \le M^\dagger(T) \le 1)

#PTP_POVM

Let MM be a completely positive and trace-preserving (CPTP) map from the space of complex Hermitian matrices of dimension dind_{in} to those of dimension doutd_{out}. Let MM^\dagger (denoted as `M.dual`) be its dual map. For any complex Hermitian matrix TT of dimension doutd_{out} that represents a two-element POVM effect (i.e., 0TI0 \le T \le \mathbb{I}), its image under the dual map also satisfies 0M(T)I0 \le M^\dagger(T) \le \mathbb{I}, where I\mathbb{I} denotes the identity matrix.

theorem

Expectation Value Adjoint Property for CPTP\text{CPTP} maps: Tr(E(ρ)T)=Tr(ρE(T))\text{Tr}(\mathcal{E}(\rho)T) = \text{Tr}(\rho \mathcal{E}^\dagger(T))

#exp_val_Dual

Let E\mathcal{E} be a completely positive trace-preserving (CPTP) map from the space of complex matrices of dimension dind_{in} to those of dimension doutd_{out}. For any quantum mixed state ρ\rho with dimension dind_{in} and any Hermitian operator TT of dimension doutd_{out}, the expectation value of TT with respect to the evolved state E(ρ)\mathcal{E}(\rho) is equal to the expectation value of the evolved operator E(T)\mathcal{E}^\dagger(T) with respect to the initial state ρ\rho. That is, \[ \text{Tr}(\mathcal{E}(\rho) T) = \text{Tr}(\rho \mathcal{E}^\dagger(T)) \] where E\mathcal{E}^\dagger is the dual (completely positive unital) map of E\mathcal{E}.

definition

HPMap from an R\mathbb{R}-linear map ff on Hermitian matrices

#ofHermitianMat

Let f:HermitianMatdin(C)RHermitianMatdout(C)f: \text{HermitianMat}_{d_{in}}(\mathbb{C}) \to_{\mathbb{R}} \text{HermitianMat}_{d_{out}}(\mathbb{C}) be an R\mathbb{R}-linear map between spaces of Hermitian matrices. The definition constructs a Hermiticity-Preserving Map (HPMap) E\mathcal{E} from dind_{in} to doutd_{out} by extending ff to all complex matrices via the decomposition into Hermitian and anti-Hermitian parts. Specifically, for any matrix xx, the map is defined as: E(x)=f(Re(x))+if(Im(x))\mathcal{E}(x) = f(\text{Re}(x)) + i \cdot f(\text{Im}(x)) where Re(x)=x+x2\text{Re}(x) = \frac{x + x^*}{2} and Im(x)=xx2i\text{Im}(x) = \frac{x - x^*}{2i} are the Hermitian components of xx.

theorem

The linear map of `HPMap.ofHermitianMat f` equals ff

#linearMap_ofHermitianMat

Let f:HermitianMatdin(C)RHermitianMatdout(C)f: \text{HermitianMat}_{d_{in}}(\mathbb{C}) \to_{\mathbb{R}} \text{HermitianMat}_{d_{out}}(\mathbb{C}) be an R\mathbb{R}-linear map between spaces of Hermitian matrices. Let HPMap.ofHermitianMat(f)\text{HPMap.ofHermitianMat}(f) be the hermiticity-preserving map E\mathcal{E} obtained by extending ff to all complex matrices. Then, the R\mathbb{R}-linear map on Hermitian matrices associated with E\mathcal{E} is equal to the original map ff.

theorem

`HPMap.ofHermitianMat` is Inverse to the Restriction of `HPMap` to Hermitian Matrices

#ofHermitianMat_linearMap

Let fHPMap(dIn,dOut,C)f \in \text{HPMap}(d_{In}, d_{Out}, \mathbb{C}) be a Hermitian-preserving map. If we take its restriction to the space of Hermitian matrices as an R\mathbb{R}-linear map, denoted by LinearMapClass.linearMap(f)\text{LinearMapClass.linearMap}(f), and then reconstruct a Hermitian-preserving map from this linear map using the `ofHermitianMat` construction, the resulting map is equal to the original map ff.

definition

The Hermitian dual of a Hermitian-preserving map ff

#hermDual

Given a Hermitian-preserving map f:HermitianMatdIn(C)HermitianMatdOut(C)f : \text{HermitianMat}_{d_{In}}(\mathbb{C}) \to \text{HermitianMat}_{d_{Out}}(\mathbb{C}), its Hermitian dual ff^\dagger (or `hermDual`) is the Hermitian-preserving map from HermitianMatdOut(C)\text{HermitianMat}_{d_{Out}}(\mathbb{C}) to HermitianMatdIn(C)\text{HermitianMat}_{d_{In}}(\mathbb{C}) defined as the adjoint of the linear map ff with respect to the Hilbert-Schmidt inner product. It satisfies the adjoint property f(A),B=A,f(B)\langle f(A), B \rangle = \langle A, f^\dagger(B) \rangle for all Hermitian matrices AA and BB.

theorem

(f)=f(f^\dagger)^\dagger = f for Hermitian-preserving maps

#hermDual_hermDual

For any Hermitian-preserving map f:HermitianMatdIn(C)HermitianMatdOut(C)f : \text{HermitianMat}_{d_{In}}(\mathbb{C}) \to \text{HermitianMat}_{d_{Out}}(\mathbb{C}), the Hermitian dual of its Hermitian dual is equal to the original map, i.e., (f)=f(f^\dagger)^\dagger = f. Here, the Hermitian dual ff^\dagger is defined as the adjoint of ff with respect to the Hilbert-Schmidt inner product.

theorem

f(A),B=A,f(B)\langle f(A), B \rangle = \langle A, f^\dagger(B) \rangle for Hermitian-preserving maps

#inner_hermDual

Let ff be a Hermitian-preserving map (an element of `HPMap`) from the space of Hermitian matrices of dimension dInd_{In} to dOutd_{Out} over C\mathbb{C}. For any Hermitian matrices AHermitianMatdIn(C)A \in \text{HermitianMat}_{d_{In}}(\mathbb{C}) and BHermitianMatdOut(C)B \in \text{HermitianMat}_{d_{Out}}(\mathbb{C}), the Hilbert-Schmidt inner product satisfies: f(A),B=A,f(B)\langle f(A), B \rangle = \langle A, f^\dagger(B) \rangle where ff^\dagger (denoted as `f.hermDual`) is the Hermitian dual map of ff.

theorem

Adjoint property of the Hermitian dual map ff^\dagger with respect to the inner product

#inner_hermDual'

Let f:HermitianMatdIn(C)HermitianMatdOut(C)f: \text{HermitianMat}_{d_{In}}(\mathbb{C}) \to \text{HermitianMat}_{d_{Out}}(\mathbb{C}) be a Hermitian-preserving map and ff^\dagger denote its Hermitian dual. For any Hermitian matrices AHermitianMatdIn(C)A \in \text{HermitianMat}_{d_{In}}(\mathbb{C}) and BHermitianMatdOut(C)B \in \text{HermitianMat}_{d_{Out}}(\mathbb{C}), the Hilbert-Schmidt inner product satisfies f(A),B=A,f(B)\langle f(A), B \rangle = \langle A, f^\dagger(B) \rangle.

theorem

If ff is a positive map, then ff^\dagger is a positive map

#hermDual

Let ff be a Hermitian-preserving matrix map (of type `HPMap`) from complex matrices of dimension dInd_{In} to dOutd_{Out}. If the underlying linear map f.mapf.\text{map} is positive (i.e., it maps positive semi-definite matrices to positive semi-definite matrices), then the underlying linear map of its Hermitian dual, f.hermDual.mapf.\text{hermDual}.\text{map}, is also positive.

theorem

If ff is trace-preserving, then its Hermitian dual ff^\dagger is unital

#hermDual_Unital

Let ff be a Hermitian-preserving map between complex Hermitian matrices of dimensions dInd_{In} and dOutd_{Out}. If the underlying linear map f.mapf.\text{map} is trace-preserving, then the underlying linear map of its Hermitian dual f.mapf^\dagger.\text{map} is unital, meaning it maps the identity matrix to the identity matrix (f(I)=If^\dagger(I) = I).

definition

The Hermitian dual of a PTPMap\text{PTPMap} is a PUMap\text{PUMap}

#hermDual

Given a positive trace-preserving map (PTPMap) MM from dIn×dInd_{In} \times d_{In} complex matrices to dOut×dOutd_{Out} \times d_{Out} complex matrices, its Hermitian dual MM^\dagger is a positive unital map (PUMap) from dOut×dOutd_{Out} \times d_{Out} matrices to dIn×dInd_{In} \times d_{In} matrices. This dual map is constructed by taking the adjoint of the underlying Hermitian-preserving map and inherits the property of being unital from the trace-preserving property of MM.

theorem

The Hermitian Dual of a PTPMap\text{PTPMap} Preserves Positivity

#hermDual_pos

Let MM be a positive trace-preserving map (PTPMap\text{PTPMap}) from the space of dIn×dInd_{In} \times d_{In} complex Hermitian matrices to dOut×dOutd_{Out} \times d_{Out} complex Hermitian matrices. For any Hermitian matrix TT of size dOutd_{Out} such that TT is positive semidefinite (0T0 \le T), its image under the Hermitian dual map MTM^\dagger T (or M.hermDualTM.hermDual T) is also positive semidefinite (0MT0 \le M^\dagger T).

theorem

The Dual of a PTP Map Preserves POVM Effects 0TI0 \le T \le I

#PTP_POVM

Let MM be a point-trace-preserving (PTP) map from the space of complex matrices of dimension dInd_{In} to dOutd_{Out}. Let TT be a Hermitian matrix of dimension dOutd_{Out} such that 0TI0 \le T \le I, representing a two-element Positive Operator-Valued Measure (POVM) effect. Then its image under the Hermitian dual map, M(T)M^\dagger(T), is a Hermitian matrix of dimension dInd_{In} that also satisfies 0M(T)I0 \le M^\dagger(T) \le I.

theorem

Expectation value of a PTPMap equals the expectation value of its dual map: E(ρ),T=ρ,E(T)\langle \mathcal{E}(\rho), T \rangle = \langle \rho, \mathcal{E}^*(T) \rangle

#exp_val_hermDual

Let E\mathcal{E} be a positive trace-preserving map (PTPMap) from dInd_{In} to dOutd_{Out}. For any quantum mixed state ρ\rho of dimension dInd_{In} and any Hermitian operator TT of dimension dOutd_{Out}, the expectation value of TT in the state E(ρ)\mathcal{E}(\rho) is equal to the expectation value of the dual map E\mathcal{E}^* applied to TT in the original state ρ\rho: \[ \text{Tr}(\mathcal{E}(\rho) T) = \text{Tr}(\rho \mathcal{E}^*(T)) \] where E\mathcal{E}^* (denoted as `hermDual`) is the adjoint positive unital map (PUMap) of E\mathcal{E} with respect to the Frobenius inner product.