Choi correspondence

Turn a quantum channel into a state and vice-versa.

import Quantum_channel

def |Γ⟩ := ∑ i, |i⟩R ⊗ |i⟩A -- unnormalized maximally entangled vector

def Γ := |Γ⟩⟨Γ|

def Choi [linear_map 𝒩] : linear_operator :=
IR⊗𝒩A ΓRA

-- 1R⊗𝒩 ΓRA = ∑ i j, |i⟩⟨j|R ⊗ 𝒩(|i⟩⟨j|A)

If operator is LOCC then Choi state is separable accross an appropriate cut.

Positive partial transpose of separable state.

theorem quantum_channels_eq_iff_Choi_states_equals [quantum_channel 𝒩 ℳ] :
𝒩 = ℳ ↔ Choi 𝒩 = Choi ℳ := sorry

/-- "linear map completely positive iff 
Choi operator ΓNRD is positive semi-definite." -/
theorem Choi_of_completely_positive :
  completely_positive 𝒩 ↔ positive_semidefinite Choi 𝒩 :=
sorry

/-- "trace preserving iff pTr_D(ΓRD) = 1R." -/
theorem Choi_of_trace_preserving_map :
  trace_preserving 𝒩 ↔ pTrD(Choi 𝒩) = 1R :=
sorry

---

import Entanglement_breaking

theorem Choi_Jam_of_entanglement_breaking [quantum_channel 𝒩] :
  entanglement_breaking 𝒩
  → ∀ [trace_class_op A] [bounded_op B], 
      ∃ [Ω : quantum_channel → separable_bounded_op], 
        pTr_B(Ω(𝒩)) = 1_A 
        ∧ Tr(B 𝒩(A)) = Tr(Ω(𝒩)A ⊗ B) :=
begin
  sorry,
end

References

• Wilde2011;

• Wilde2020;

• Plenio2008;