Course related house keeping.

src/op/system/inj.tex

@@ -0,0 +1,24 @@
+\section{Injective Operator Systems}
+\label{section:injective-ops}
+
+
+By \hyperref[Arveson's Extension Theorem]{theorem:arveson-extension}, $B(H)$ is injective for any Hilbert space $H$. Further, the \hyperref[Choi-Effros Theorem]{choi-effros} implies that every operator system embeds into $B(H)$, for a suitable Hilbert space $H$. Therefore the category of operator systems, with unital complete order isomorphisms, has sufficiently many injectives. 
+
+\begin{theorem}
+\label{theorem:opsys-predual}
+    Let $S, T$ be operator systems. If $T$ admits a predual, then the space
+    \[
+    UCP(S; T) = \bracsn{\phi: S \to T| \phi \text{ unital, completely positive}}
+    \]
+
+    is compact in the point-weak* topology. 
+\end{theorem}
+
+
+\begin{definition}[Injective]
+\label{definition:injective-operator-system}
+    Let 
+\end{definition}
+
+
+