5 Quantum sets

Definition 5.0.1

✓

Given a \(^*\)-algebra \((\mathcal{A},m,\eta )\) that is also a finite-dimensional Hilbert space, we say it is a 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 (for a fixed \(k\in \mathbb {R}\)):

\(\sigma _t\circ \sigma _s=\sigma _{t+s}\),
\(\sigma _t^{\operatorname {r}}=\sigma _{-t}\),
\(\sigma _t\) is self-adjoint,
\(\forall {x,y,z}\in \mathcal{A}:\left\langle xy \mid z\right\rangle =\left\langle y \mid \sigma _{-k}(x)^*z\right\rangle \),
\(\forall {x,y,z}\in \mathcal{A}:\left\langle xy \mid z\right\rangle =\left\langle x \mid z\sigma _{-k-1}(y^*)\right\rangle \).

By Proposition 3.1.4, we see that \((\mathcal{A},m,\eta ,k)\) is a Frobenius algebra.

And by Proposition 3.1.3, 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 \(\left\langle x \mid y\right\rangle =\eta ^*(x^*\sigma _k(y))\) for all \(x,y\in \mathcal{A}\).

It is clear that we get \(\sigma _0=1\) and \(\sigma _{t}^{-1}=\sigma _{-t}\) for \(t\in \mathbb {R}\).

Remark 5.0.2

In the Lean code, we start with a \(^*\)-algebra and define a modular automorphism \(\sigma _t\) that satisfies properties 1–3 above. Then we add the Hilbert space structure on top of that. The reason for this is so that we can define more quantum sets on the same space (with a different \(k\)-value; in practice, we either use \(k=0\) for the GNS-inner product, or \(k=-1/2\) for the KMS-inner product). This way minimises the instance diamonds created.

Normally, we start with a finite-dimensional \(^*\)-algebra \((\mathcal{A},m,\eta )\) with a faithful and positive linear functional \(\psi \). Then define the Hilbert space structure by \(\left\langle x \mid y\right\rangle =\psi (x^*y)\). The modular automorphism is then defined by \(\sigma _t(x)=Q^{-t}xQ^t\), where \(Q\) is the “weight” of \(\psi \) (in other words, \(\psi (x)=\operatorname{Tr}(Q x)\)). Then one has a quantum set.

Clearly, the Hilbert space of \(\bigoplus _iM_{n_i}\) given by a positive and faithful linear functional \(\psi \) (Definition 4.2.1) is a quantum set with modular automorphism defined in Definition 4.3.1.

Lemma 5.0.3

✓

Given a Hilbert space \(\mathcal{H}\) that is also a \(^*\)-algebra, and \(x\in \mathcal{H}\), we get \(\left\lvert x\right\rangle ^{\operatorname {r}}=\left\lvert x^*\right\rangle \).

Proof ▶

\[ {\left\lvert x\right\rangle (1^*)}^*=\left\lvert x^*\right\rangle (1). \]

Lemma 5.0.4

✓

Given a quantum set \((\mathcal{A},m,\eta ,\sigma _r)\) and \(x\in \mathcal{A}\), we get \(\left\langle x\right\rvert ^{\operatorname {r}}=\left\langle \sigma _{-1}(x^*)\right\rvert \).

Proof ▶

\[ {\left\langle x\right\rvert (y^*)}^*=\left\langle y^* \mid x\right\rangle =\left\langle \sigma _{-1}(x^*) \mid y\right\rangle =\left\langle \sigma _{-1}(x^*)\right\rvert (y). \]

Corollary 5.0.5

✓

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

\[ \left\lvert a\right\rangle \! \! \left\langle b\right\rvert ^{\operatorname {r}}=\left\lvert a^*\right\rangle \! \! \left\langle \vartheta _{-1}(b^*)\right\rvert . \]

Proof ▶

Use Lemmas 5.0.3, 5.0.4, and 2.0.4.

Proposition 5.0.6

✓

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}. \]

Proof ▶

Let \(x\in {\mathcal{A}_2}\) and \(y\in \mathcal{A}_1\), and compute,

\begin{align*} \left\langle {A^{*\operatorname {r}}}(x) \mid y\right\rangle & = \left\langle {A^*(x^*)}^* \mid y\right\rangle =\left\langle y^* \mid \sigma _{-1}(A^*(x^*))\right\rangle \\ & = \left\langle A(\sigma _{-1}(y^*)) \mid x^*\right\rangle \\ & = \left\langle A({\sigma _{1}(y)}^*) \mid x^*\right\rangle = \left\langle x \mid \vartheta _{-1}A^{\operatorname {r}}\sigma _{1}(y)\right\rangle \\ & = \left\langle \sigma _{1}A^{\operatorname {r}*}\vartheta _{-1}(x) \mid y\right\rangle \end{align*}

Thus, \(A^{*\operatorname {r}}=\sigma _{1}A^{\operatorname {r}*}\vartheta _{-1}\).

Proposition 5.0.7

✓

Given a quantum set \((\mathcal{A},m,\eta ,\sigma _r)\), we get

\[ (\eta ^*m\otimes \operatorname {id})(\operatorname {id}\otimes \, \varkappa )(m^*\eta \otimes \operatorname {id})=\sigma _1. \]

Here, \(\varkappa \) is the identification \(\mathcal{A}\otimes \mathcal{A}\cong \mathcal{A}\otimes \mathcal{A}\) given by \(x\otimes y\mapsto y\otimes x\).

Proof ▶

Let \(x,y\in \mathcal{A}\), and let \(m^*(1)=\sum _i\alpha _i\otimes \beta _i\) for some tuples \((\alpha _i),(\beta _i)\) in \(\mathcal{A}\). Then we compute,

\begin{align*} & \, \left\langle (\eta ^*m\otimes \operatorname {id})(\operatorname {id}\otimes \, \varkappa )(m^*\eta \otimes \operatorname {id})(x) \mid y\right\rangle \\ =& \sum _i\left\langle (\eta ^*m\otimes \operatorname {id})(\operatorname {id}\otimes \, \varkappa )(\alpha _i\otimes \beta _i\otimes x) \mid y\right\rangle \\ =& \, \sum _i\left\langle (\eta ^*m\otimes \operatorname {id})(\alpha _i\otimes x\otimes \beta _i) \mid y\right\rangle \\ =& \, \sum _i\left\langle \eta ^*(\alpha _ix)\beta _i \mid y\right\rangle = \sum _i\left\langle \alpha _ix \mid 1\right\rangle \left\langle \beta _i \mid y\right\rangle \\ =& \, \sum _i\left\langle \alpha _i \mid \sigma _{-1}(x^*)\right\rangle \left\langle \beta _i \mid y\right\rangle \\ =& \, \sum _i\left\langle \alpha _i\otimes \beta _i \mid \sigma _{-1}(x^*)\otimes y\right\rangle =\left\langle m^*(1) \mid \sigma _{-1}(x^*)\otimes y\right\rangle \\ =& \, \left\langle 1 \mid \sigma _{-1}(x^*)y\right\rangle =\left\langle \sigma _{1}(x) \mid y\right\rangle . \end{align*}

Proposition 5.0.8

✓

Given a quantum set \((\mathcal{A},m,\eta ,\sigma _r)\), we get

\[ (\operatorname {id}\otimes \, \eta ^*m)(\varkappa \otimes \operatorname {id})(\operatorname {id}\otimes \, m^*\eta )=\sigma _{-1}. \]

Here, \(\varkappa \) is the identification \(\mathcal{A}\otimes \mathcal{A}\cong \mathcal{A}\otimes \mathcal{A}\) given by \(x\otimes y\mapsto y\otimes x\).

Proof ▶

We let \(x,y\in \mathcal{A}\) and \(m^*(1)=\sum _i\alpha _i\otimes \beta _i\) for some tuples \((\alpha _i),(\beta _i)\) in \(\mathcal{A}\). Then we compute,

\begin{align*} & \left\langle (\operatorname {id}\otimes \, \eta ^*m)(\varkappa \otimes \operatorname {id})(\operatorname {id}\otimes \, m^*\eta )(x) \mid y\right\rangle \\ =& \sum _i\left\langle (\operatorname {id}\otimes \, \eta ^*m)(\varkappa \otimes \operatorname {id})(x\otimes \alpha _i\otimes \beta _i) \mid y\right\rangle \\ =& \sum _i\left\langle (\operatorname {id}\otimes \, \eta ^*m)(\alpha _i\otimes x\otimes \beta _i) \mid y\right\rangle \\ =& \sum _i\left\langle \left\langle 1 \mid x\beta _i\right\rangle \alpha _i \mid y\right\rangle = \sum _i\left\langle \alpha _i \mid y\right\rangle \left\langle x\beta _i \mid 1\right\rangle \\ =& \sum _i\left\langle \alpha _i \mid y\right\rangle \left\langle \beta _i \mid x^*\right\rangle \\ =& \left\langle m^*(1) \mid y\otimes x^*\right\rangle =\left\langle 1 \mid yx^*\right\rangle \\ =& \left\langle \sigma _{-1}(x) \mid y\right\rangle . \end{align*}

Lemma 5.0.9

✓

Given a quantum set \((\mathcal{A},m,\eta ,\sigma )\), we get

\[ \eta ^*(a\sigma _r(b)) = \eta ^*(\sigma _{r + 1}(b)a), \]

for any \(r\in \mathbb {R}\).

Proof ▶

\begin{align*} \eta ^*(a\sigma _r(b)) & = \left\langle 1 \mid a\sigma _r(b)\right\rangle = \left\langle \sigma _{-(r+1)}(b^*) \mid a\right\rangle \\ & = \left\langle {\sigma _{r+1}(b)}^* \mid a\right\rangle =\eta ^*(\sigma _{r+1}(b)a). \end{align*}

Corollary 5.0.10

✓

Given a quantum set \((\mathcal{A},m,\eta ,\sigma )\), we get

\[ \eta ^* m(\sigma _{1}\otimes \operatorname {id})=\eta ^*\circ m\circ \varkappa . \]

Proof ▶

Use Lemma 5.0.9.

Corollary 5.0.11

✓

Given a quantum set \((\mathcal{A},m,\eta ,\sigma )\), we get

\[ \eta ^* m(\operatorname {id}\otimes \sigma _{-1})=\eta ^*\circ m\circ \varkappa . \]

Proof ▶

Use Lemma 5.0.9.

Definition 5.0.12

✓

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 \(\mathcal{B}(\mathcal{A}_1,\mathcal{A}_2)\) to \(\mathcal{A}_2\otimes \mathcal{A}_1^{\operatorname {op}}\) given by

\[ \Psi _{t,r}(\left\lvert a\right\rangle \! \! \left\langle b\right\rvert )=\vartheta _t(a)\otimes {\sigma _r(b)}^{*\operatorname {op}}, \]

with inverse given by

\[ \Psi _{t,r}^{-1}(a\otimes b^{\operatorname {op}})=\left\lvert \sigma _{-t}(a)\right\rangle \! \! \left\langle \vartheta _{-r}(b^*)\right\rvert . \]

Definition 5.0.13

✓

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}}\).

Definition 5.0.14

✓

We define \(\Upsilon \) to be the linear isomorphism from \(\mathcal{B}(\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}\).

Definition 5.0.15

✓

We define \(\Phi \) to be the linear isomorphism from \(\mathcal{B}(\mathcal{A}_1,\mathcal{A}_2)\) to the bimodule maps in \(\mathcal{B}(\mathcal{A}_1\otimes \mathcal{A}_2)\) given by \((\operatorname {rmul}\otimes \operatorname {lmul})\Upsilon \).

Lemma 5.0.16

\[ \Phi (A)=(\operatorname {id}\otimes m)(\operatorname {id}\otimes A\otimes \operatorname {id})(m^*\otimes \operatorname {id}). \]

Proof ▶