From 093c1b9730415a7924d3c21aa9ddc34147422a86 Mon Sep 17 00:00:00 2001 From: Monica Omar <2497250a@research.gla.ac.uk> Date: Mon, 24 Jun 2024 19:35:27 +0000 Subject: [PATCH] docs --- blueprint/src/chapters/ips.tex | 4 +- blueprint/src/chapters/quantumset.tex | 57 ++++++++++++++++++++++++++- 2 files changed, 57 insertions(+), 4 deletions(-) diff --git a/blueprint/src/chapters/ips.tex b/blueprint/src/chapters/ips.tex index e2bfda5..2c963c5 100644 --- a/blueprint/src/chapters/ips.tex +++ b/blueprint/src/chapters/ips.tex @@ -197,11 +197,11 @@ \section{The modular automorphism} \begin{proof}\uses{modAut_real_apply, dual_eq_trace}\leanok Let $x,y\in{B}$. Then we compute \begin{align*} - \ip{x}{\sigma_{t}^*(y)} &= \ip{\sigma_{t}(x)}{y}=\psi({\sigma_{t}(x)}^*y)=\psi(\sigma_{-t}(x^*)y) &\text{by \ref{modAut_real_apply}}\\ + \ip{x}{\sigma_{t}^*(y)} &= \ip{\sigma_{t}(x)}{y}=\psi({\sigma_{t}(x)}^*y)=\psi(\sigma_{-t}(x^*)y)\\ &=\Tr(Q\sigma_{-t}(x^*)y)=\Tr(QQ^tx^*Q^{-t}y)\\ &= \Tr(Q x^*Q^{-t}yQ^t)=\ip{x}{\sigma_{t}(y)}. \end{align*} - Thus $\sigma_{t}$ is self-adjoint. Note that we used the fact $\psi\colon x\mapsto\Tr(Q x)$ (Proposition \ref{dual_eq_trace}). + Thus $\sigma_{t}$ is self-adjoint. \end{proof} \begin{corollary}\label{modAut_isCoalgHom}\uses{modAut} diff --git a/blueprint/src/chapters/quantumset.tex b/blueprint/src/chapters/quantumset.tex index 51bd9fe..54cff9e 100644 --- a/blueprint/src/chapters/quantumset.tex +++ b/blueprint/src/chapters/quantumset.tex @@ -4,7 +4,7 @@ \chapter{Quantum sets} \uses{LinearMap.real, FiniteDimensionalCoAlgebra_isFrobeniusAlgebra_of, isAlgHom_iff_adjoint_isCoalgHom} \lean{QuantumSet}\leanok Given a $^*$-algebra $(\mathcal{A},m,\eta)$ that is also a finite-dimensional Hilbert space, - we say it is a \textit{quantum set} when there is a modular automorphism $\sigma_t\colon\mathcal{A}\cong\mathcal{A}$, which is an algebra automorphism for each $t\in\RR$, and that the following properties are satisfied: + we say it is a \textit{quantum set} when there is a modular automorphism $\sigma_t\colon\mathcal{A}\cong\mathcal{A}$, which is an algebra automorphism for each $t\in\mathbb{R}$, and that the following properties are satisfied: \begin{enumerate} \item $\sigma_t\circ\sigma_s=\sigma_{t+s}$, \item $\sigma_0=\id$, @@ -15,9 +15,62 @@ \chapter{Quantum sets} \end{enumerate} By Proposition \ref{FiniteDimensionalCoAlgebra_isFrobeniusAlgebra_of}, we see that $(\mathcal{A},m,\eta)$ is a Frobenius algebra. - And by Proposition \ref{isAlgHom_iff_adjoint_isCoalgHom}, we can see that for any $t\in\RR$, we get $\sigma_t$ is also a co-algebra homomorphism. + And by Proposition \ref{isAlgHom_iff_adjoint_isCoalgHom}, we can see that for any $t\in\mathbb{R}$, we get $\sigma_t$ is also a co-algebra homomorphism. We can easily see that we get $\ip{x}{y}=\eta^*(x^*y)$ for all $x,y\in\mathcal{A}$. \end{definition} Clearly, the Hilbert space of $\bigoplus_iM_{n_i}$ given by a positive and faithful linear functional $\psi$ (Definition \ref{PiMat.InnerProductSpace}) is a quantum set with modular automorphism defined in Definition \ref{modAut}. + + \begin{lemma}\label{ket_real}\uses{LinearMap.real, ket}\lean{ket_real}\leanok + Given a Hilbert space $\Hcal$ that is also a $^*$-algebra, and $x\in\Hcal$, we get $\ket{x}^{\operatorname{r}}=\ket{x^*}$. + \end{lemma} + \begin{proof}\leanok + \[{\ket{x}(1^*)}^*=\ket{x^*}(1).\] + \end{proof} + + \begin{lemma}\label{bra_real}\uses{LinearMap.real, bra, QuantumSet}\lean{bra_real}\leanok + Given a quantum set $(\mathcal{A},m,\eta,\sigma_r)$ and $x\in\mathcal{A}$, we get $\bra{x}^{\operatorname{r}}=\bra{\sigma_{-1}(x^*)}$. + \end{lemma} + \begin{proof}\leanok + \[{\bra{x}(y^*)}^*=\ip{y^*}{x}=\ip{\sigma_{-1}(x^*)}{y}=\bra{\sigma_{-1}(x^*)}(y).\] + \end{proof} + \begin{corollary}\label{rankOne_real} + \uses{QuantumSet, LinearMap.real} + \lean{rankOne_real}\leanok + Given quantum sets $(\mathcal{A}_1,m_1,\eta_1,\sigma_r)$ and $(\mathcal{A}_2,m_2,\eta_2,\vartheta_r)$, and elements $a\in\mathcal{A}_1$ and $b\in\mathcal{A}_2$, we get + \[\ketbra{a}{b}^{\operatorname{r}}=\ketbra{a^*}{\theta_{-1}(b^*)}.\] + \end{corollary} + \begin{proof}\uses{ket_real, bra_real, LinearMap.real_comp}\leanok + Use Lemmas \ref{ket_real}, \ref{bra_real}, and \ref{LinearMap.real.comp}. + \end{proof} + + \begin{proposition}\label{LinearMap.adjoint_real_eq} + \uses{LinearMap.real, QuantumSet} + \lean{LinearMap.adjoint_real_eq}\leanok + Given quantum sets $(\mathcal{A}_1,m_1,\eta_1,\sigma_r)$ and $(\mathcal{A}_2,m_2,\eta_2,\vartheta_r)$, and $f\colon\mathcal{A}_1\to\mathcal{A}_2$, we get + \[ f^{*\operatorname{r}}=\vartheta_1f^{\operatorname{r}*}\sigma_{-1}.\] + \end{proposition} + \begin{proof}\leanok + Let $x\in{\mathcal{A}_2}$ and $y\in \mathcal{A}_1$, and compute, + \begin{align*} + \ip{{A^{*\operatorname{r}}}(x)}{y} &= \ip{{A^*(x^*)}^*}{y} =\ip{y^*}{\sigma_{-1}(A^*(x^*))}\\ + &= \ip{A(\sigma_{-1}(y^*))}{x^*}\\ + &= \ip{A({\sigma_{1}(y)}^*)}{x^*} + = \ip{x}{\vartheta_{-1}A^{\operatorname{r}}\sigma_{1}(y)}\\ + &= \ip{\sigma_{1}A^{\operatorname{r}*}\vartheta_{-1}(x)}{y} + \end{align*} + Thus, $A^{*\operatorname{r}}=\sigma_{1}A^{\operatorname{r}*}\vartheta_{-1}$. + \end{proof} + + + \begin{definition}\label{QuantumSet.Psi} + \uses{QuantumSet} + \lean{QuantumSet.Psi}\leanok + Given quantum sets $(\mathcal{A}_1,m_1,\eta_1,\sigma_r)$ and $(\mathcal{A}_2,m_2,\eta_2,\vartheta_r)$, then for each $t,r\in\mathbb{R}$, we define $\Psi_{t,r}$ to be the linear isomorphism from $\Bcal(\mathcal{A}_1,\mathcal{A}_2)$ to $\mathcal{A}_2\otimes\mathcal{A}_1^{\operatorname{op}}$ given by + \[\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} + +