Arveson-type extension of a unital completely positive map on an operator system
ProvedOAI.BoundedHochschild.KadisonRingrose.exists_unital_completelyPositive_extensionLet be a unital C*-algebra with star-ordered partial order and a nontrivial complex Hilbert space. Let be a linear subspace containing and closed under , and a linear map with such that every amplification sends positive matrices over to positive matrices: if and in , then . Then there is a completely positive map (CompletelyPositiveMap) with , and .
Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.
import Mathlib
import Definitions.Def_KadisonRingroseSupport2
namespace OAI
noncomputable section
open Filter Topology
open scoped ComplexOrder InnerProductSpace
namespace BoundedHochschild.KadisonRingrose
variable {A H : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H]
theorem exists_unital_completelyPositive_extension
(S : Submodule ℂ A) (h1 : (1 : A) ∈ S) (hstar : ∀ a ∈ S, star a ∈ S)
(φ : S →ₗ[ℂ] (H →L[ℂ] H)) (hφ1 : φ ⟨1, h1⟩ = 1)
(hφ : ∀ n (X : operatorSystemMatrices S n),
0 ≤ (X : CStarMatrix (Fin n) (Fin n) A) →
0 ≤ operatorSystemAmplification S φ n X) :
∃ Φ : CompletelyPositiveMap A (H →L[ℂ] H),
Φ 1 = 1 ∧ (∀ a, ‖Φ a‖ ≤ ‖a‖) ∧ ∀ a : S, Φ (a : A) = φ a := by
sorry
end BoundedHochschild.KadisonRingrose
end
end OAI