QuantumInfo.Finite.CPTPMap.Dual
32 declarations
The dual of a matrix map
#dualLet be a semiring. For a matrix map , its dual map is the unique linear map defined such that for all matrices and , the trace identity 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 .
for dual matrix maps
#trace_eqLet be a semiring. For any matrix map and any matrices and , the trace of the product of and is equal to the trace of the product of and the dual map applied to . That is, .
The dual of a Hermitian-preserving matrix map is Hermitian-preserving
#dualLet be a matrix map. If is Hermitian-preserving, then its dual map is also Hermitian-preserving.
The trace of the product of two positive semidefinite matrices is non-negative
#trace_mul_nonnegLet be a finite type with decidable equality, and let and be matrices over a field (typically or ). If both and are positive semidefinite, then the trace of their product is non-negative, i.e., .
The dual of a positive matrix map is positive
#dualLet be a matrix map between matrices over a semiring . If is a positive map (meaning it maps positive semidefinite matrices to positive semidefinite matrices), then its dual map is also a positive map.
The dual of a trace-preserving matrix map is unital
#dual_UnitalLet be a matrix map. If is trace-preserving, then its dual map is unital, meaning where is the identity matrix.
Uniqueness of Matrix Map Dual via Trace Duality Property
#dual_uniqueLet be a field. For any two matrix maps and , if for all matrices and , the trace equality holds, then is equal to the dual map .
The Choi matrix of the dual map is the reindexed transpose of the Choi matrix of .
#dual_choi_matrixLet be a matrix map from matrices over to matrices over with coefficients in a field . The Choi matrix of the dual map , denoted , is equal to the transpose of the Choi matrix of the original map , , after reindexing the row and column indices using the product commutation equivalence . Specifically, where the reindexing swaps the input and output components of the index pairs.
If is positive semidefinite, then is positive semidefinite
#dual_choi_matrix_posSemidef_of_posSemidefLet be a matrix map between matrix spaces over and with coefficients in a field . If the Choi matrix of , denoted , is positive semidefinite, then the Choi matrix of its dual map , denoted , is also positive semidefinite.
The dual of the identity matrix map is the identity map
#dual_idFor any finite type and any field , the dual of the identity matrix map is the identity matrix map itself. That is, .
Let be a field, and let be finite types with decidable equality. For any matrix maps and , the dual of their Kronecker product is equal to the Kronecker product of their dual maps, . That is, .
The Dual of a Completely Positive Matrix Map is Completely Positive
#dualLet be a matrix map between finite-dimensional spaces. If is completely positive, then its dual map (or in some contexts) is also completely positive.
Let be a commutative ring and a reflexive -module with a basis indexed by a finite set . Let be the dual basis isomorphism induced by . Then the composition of the dual of the inverse isomorphism, , with the isomorphism satisfies , where is the canonical evaluation map into the double dual.
for a reflexive module basis
#toDualEquiv_symm_comp_dualMap_toDualEquivLet be a commutative ring and be a reflexive module over with a finite basis indexed by . Let denote the isomorphisms to the dual space induced by the basis , and its inverse. Let 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., where is the dual map of .
The operation of taking the dual of a `MatrixMap` is an involution, i.e., .
#dual_dualFor a matrix map acting between types and over a semiring , the dual of its dual is equal to itself, i.e., .
The dual of a CPTP map is a CPU map
#dualLet be a completely positive and trace-preserving (CPTP) map from the space of matrices of dimension to the space of matrices of dimension over . The dual is defined as the adjoint (dual) linear map . This map is a completely positive and unital (CPU) map from the space of matrices of dimension to the space of matrices of dimension .
The dual of a CPTP map is positivity-preserving
#dual_posLet be a completely positive trace-preserving (CPTP) map from the space of complex Hermitian matrices to the space of complex Hermitian matrices. Let (denoted as `M.dual`) be the dual map of , which is a completely positive unital (CPU) map. For any Hermitian matrix , if is positive semi-definite (), then its image under the dual map is also positive semi-definite ().
The dual of a CPTP map preserves two-element POVMs ()
#PTP_POVMLet be a completely positive and trace-preserving (CPTP) map from the space of complex Hermitian matrices of dimension to those of dimension . Let (denoted as `M.dual`) be its dual map. For any complex Hermitian matrix of dimension that represents a two-element POVM effect (i.e., ), its image under the dual map also satisfies , where denotes the identity matrix.
Expectation Value Adjoint Property for maps:
#exp_val_DualLet be a completely positive trace-preserving (CPTP) map from the space of complex matrices of dimension to those of dimension . For any quantum mixed state with dimension and any Hermitian operator of dimension , the expectation value of with respect to the evolved state is equal to the expectation value of the evolved operator with respect to the initial state . That is, \[ \text{Tr}(\mathcal{E}(\rho) T) = \text{Tr}(\rho \mathcal{E}^\dagger(T)) \] where is the dual (completely positive unital) map of .
HPMap from an -linear map on Hermitian matrices
#ofHermitianMatLet be an -linear map between spaces of Hermitian matrices. The definition constructs a Hermiticity-Preserving Map (HPMap) from to by extending to all complex matrices via the decomposition into Hermitian and anti-Hermitian parts. Specifically, for any matrix , the map is defined as: where and are the Hermitian components of .
The linear map of `HPMap.ofHermitianMat f` equals
#linearMap_ofHermitianMatLet be an -linear map between spaces of Hermitian matrices. Let be the hermiticity-preserving map obtained by extending to all complex matrices. Then, the -linear map on Hermitian matrices associated with is equal to the original map .
`HPMap.ofHermitianMat` is Inverse to the Restriction of `HPMap` to Hermitian Matrices
#ofHermitianMat_linearMapLet be a Hermitian-preserving map. If we take its restriction to the space of Hermitian matrices as an -linear map, denoted by , and then reconstruct a Hermitian-preserving map from this linear map using the `ofHermitianMat` construction, the resulting map is equal to the original map .
The Hermitian dual of a Hermitian-preserving map
#hermDualGiven a Hermitian-preserving map , its Hermitian dual (or `hermDual`) is the Hermitian-preserving map from to defined as the adjoint of the linear map with respect to the Hilbert-Schmidt inner product. It satisfies the adjoint property for all Hermitian matrices and .
for Hermitian-preserving maps
#hermDual_hermDualFor any Hermitian-preserving map , the Hermitian dual of its Hermitian dual is equal to the original map, i.e., . Here, the Hermitian dual is defined as the adjoint of with respect to the Hilbert-Schmidt inner product.
for Hermitian-preserving maps
#inner_hermDualLet be a Hermitian-preserving map (an element of `HPMap`) from the space of Hermitian matrices of dimension to over . For any Hermitian matrices and , the Hilbert-Schmidt inner product satisfies: where (denoted as `f.hermDual`) is the Hermitian dual map of .
Adjoint property of the Hermitian dual map with respect to the inner product
#inner_hermDual'Let be a Hermitian-preserving map and denote its Hermitian dual. For any Hermitian matrices and , the Hilbert-Schmidt inner product satisfies .
If is a positive map, then is a positive map
#hermDualLet be a Hermitian-preserving matrix map (of type `HPMap`) from complex matrices of dimension to . If the underlying linear 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, , is also positive.
If is trace-preserving, then its Hermitian dual is unital
#hermDual_UnitalLet be a Hermitian-preserving map between complex Hermitian matrices of dimensions and . If the underlying linear map is trace-preserving, then the underlying linear map of its Hermitian dual is unital, meaning it maps the identity matrix to the identity matrix ().
The Hermitian dual of a is a
#hermDualGiven a positive trace-preserving map (PTPMap) from complex matrices to complex matrices, its Hermitian dual is a positive unital map (PUMap) from matrices to 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 .
The Hermitian Dual of a Preserves Positivity
#hermDual_posLet be a positive trace-preserving map () from the space of complex Hermitian matrices to complex Hermitian matrices. For any Hermitian matrix of size such that is positive semidefinite (), its image under the Hermitian dual map (or ) is also positive semidefinite ().
The Dual of a PTP Map Preserves POVM Effects
#PTP_POVMLet be a point-trace-preserving (PTP) map from the space of complex matrices of dimension to . Let be a Hermitian matrix of dimension such that , representing a two-element Positive Operator-Valued Measure (POVM) effect. Then its image under the Hermitian dual map, , is a Hermitian matrix of dimension that also satisfies .
Expectation value of a PTPMap equals the expectation value of its dual map:
#exp_val_hermDualLet be a positive trace-preserving map (PTPMap) from to . For any quantum mixed state of dimension and any Hermitian operator of dimension , the expectation value of in the state is equal to the expectation value of the dual map applied to in the original state : \[ \text{Tr}(\mathcal{E}(\rho) T) = \text{Tr}(\rho \mathcal{E}^*(T)) \] where (denoted as `hermDual`) is the adjoint positive unital map (PUMap) of with respect to the Frobenius inner product.
