English
An instance of CompletelyPositiveMapClass for a given F, A1, A2 is itself a CompletelyPositiveMapClass.
Русский
Для заданного F, A1, A2 имеется инстанс CompletelyPositiveMapClass, образующий сам класс полностью положительных отображений.
LaTeX
$$instCompletelyPositiveMapClass F A₁ A₂$$
Lean4
/-- Linear maps which are completely positive are order homomorphisms (i.e., positive maps). -/
theorem _root_.OrderHomClass.of_map_cstarMatrix_nonneg
(h : ∀ (φ : F) (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map φ) : OrderHomClass F A₁ A₂ :=
.ofLinear <| by
intro φ a ha
let Ma := toOneByOne (Fin 1) ℂ A₁ a
have h₁ : 0 ≤ Ma := map_nonneg (toOneByOne (Fin 1) ℂ A₁) ha
have h₂ : 0 ≤ Ma.map φ := h φ 1 Ma h₁
have h₃ : φ a = (toOneByOne (Fin 1) ℂ A₂).symm (toOneByOne (Fin 1) ℂ A₂ (φ a)) := rfl
rw [h₃]
exact map_nonneg (toOneByOne (Fin 1) ℂ A₂).symm h₂
