diff --git a/blueprint/src/chapters/qg.tex b/blueprint/src/chapters/qg.tex new file mode 100644 index 0000000..9c07010 --- /dev/null +++ b/blueprint/src/chapters/qg.tex @@ -0,0 +1,41 @@ +\chapter{Quantum graphs} + +\begin{definition}\label{QuantumGraph} + \uses{QuantumSet, schurMul} + \lean{QuantumGraph}\leanok + A \textit{quantum graph} is a pair $(B,A)$, where $B$ is a quantum set and $A$ is a linear map $B\to B$ such that $A\bullet A=A$. +\end{definition} + +\begin{definition}\label{QuantumGraph.Real} + \uses{QuantumGraph, LinearMap.IsReal} + \lean{QuantumGraph.Real}\leanok + A quantum graph $(B,A)$ is \textit{real} if $A$ is a real linear map. +\end{definition} + +\begin{lemma}\label{Coalgebra.comul_mul} + \uses{QuantumSet} + \lean{Coalgebra.comul_mul_of_gns}\leanok + Given a quantum set $B$, we have + \[m^*m=\sum_i\rmul(u_i)\otimes\lmul(u_i^*),\] + where $(u_i)_i$ is an orthonormal basis of $B$. +\end{lemma} +\begin{proof}\uses{rmulMapLmul_apply_Upsilon_eq}\leanok + Using Lemma \ref{rmulMapLmul_apply_Upsilon_eq}, we get + \[m^*m=\Phi(\operatorname{id})=\rmul(u_i)^*\otimes\lmul(u_i).\] + Taking adjoints of the above then gives us our desired result. +\end{proof} + +\begin{lemma}\label{QuantumGraph.Real.isPosMap} + \uses{QuantumGraph.Real, LinearMap.IsPosMap} + \lean{schurIdempotent.isSchurProjection_iff_isPosMap}\leanok + Given a quantum graph $(B,A)$, we have $(B,A)$ is real if and only if $A$ is a positive map. +\end{lemma} +\begin{proof}\uses{isReal_of_isPosMap, Coalgebra.comul_mul}\leanok + If $A$ is a positive map, then it is real by Theorem \ref{isReal_of_isPosMap}. + So suppose $A$ is real. Now let $x\in{B}$. Then using Lemma \ref{Coalgebra.comul_mul}, we compute, + \begin{align*} + A(x^*x) &= (A \bullet A)m(x^*\otimes x)\\ + &= \sum_im(A\otimes A)(x^*u_i\otimes u_i^*x)\\ + &= \sum_iA(x^*u_i)A(u_i^*x)=\sum_i{A(u_i^*x)}^*A(u_i^*x) \geq0. + \end{align*} +\end{proof} diff --git a/blueprint/src/chapters/quantumset.tex b/blueprint/src/chapters/quantumset.tex index 3ba9223..427ae60 100644 --- a/blueprint/src/chapters/quantumset.tex +++ b/blueprint/src/chapters/quantumset.tex @@ -157,4 +157,38 @@ \chapter{Quantum sets} \[\Psi_{t,r}(\ketbra{a}{b})=\vartheta_t(a)\otimes{\sigma_r(b)}^{*\operatorname{op}},\] with inverse given by \[\Psi_{t,r}^{-1}(a\otimes b^{\operatorname{op}})=\ketbra{\sigma_{-t}(a)}{\vartheta_{-r}(b^*)}.\] - \end{definition} \ No newline at end of file + \end{definition} + + \begin{definition}\label{tenSwap} + \lean{tenSwap}\leanok + We define the tensor swap map to be $\varrho\colon A\otimes B^{\operatorname{op}}\cong B\otimes A^{\operatorname{op}}$, given by $x\otimes y^{\operatorname{op}}\mapsto y\otimes x^{\operatorname{op}}$. + \end{definition} + + \begin{definition}\label{Upsilon} + \uses{QuantumSet.Psi, tenSwap} + \lean{Upsilon}\leanok + We define $\Upsilon$ to be the linear isomorphism from $\Bcal(\mathcal{A}_1,\mathcal{A}_2)$ to $\mathcal{A}_1\otimes\mathcal{A}_2$ given by $(\operatorname{id}\otimes\operatorname{unop})\varrho\Psi_{0,1}$. + \end{definition} + + % \begin{lemma}\lean{} + % $\Upsilon(\ketbra{a}{b})=\sigma_{-1}(b^*)\otimes a$. + % \end{lemma} + % \begin{lemma} + % $\Upsilon^{-1}(a\otimes b)=\ketbra{b}{\sigma_{-1}(a^*)}$. + % \end{lemma} + + \begin{definition}\label{PhiMap} + \uses{Upsilon} + \lean{PhiMap}\leanok + We define $\Phi$ to be the linear isomorphism from $\Bcal(\mathcal{A}_1,\mathcal{A}_2)$ to the bimodule maps in $\Bcal(\mathcal{A}_1\otimes\mathcal{A}_2)$ given by $(\rmul\otimes\lmul)\Upsilon$. + \end{definition} + + \begin{lemma}\label{rmulMapLmul_apply_Upsilon_eq} + \uses{PhiMap} + \lean{rmulMapLmul_apply_Upsilon_eq}\leanok + \[\Phi(A)=(\operatorname{id}\otimes m)(\operatorname{id}\otimes A\otimes\operatorname{id})(m^*\otimes\operatorname{id}).\] + \end{lemma} + \begin{proof} + + \end{proof} + diff --git a/blueprint/src/chapters/scene.tex b/blueprint/src/chapters/scene.tex index 3eaf231..8b8aec7 100644 --- a/blueprint/src/chapters/scene.tex +++ b/blueprint/src/chapters/scene.tex @@ -5,3 +5,4 @@ \input{chapters/quantumset.tex} \input{chapters/schur.tex} \input{chapters/posmap.tex} +\input{chapters/qg.tex}