Quantum and Reality


Formalizations of quantum information theory in category theory and type theory, for the design of verifiable quantum programming languages, need to express its two fundamental characteristics: (1) parameterized linearity and (2) metricity. The first is naturally addressed by dependent-linearly typed languages such as Proto- or, following our recent observations [[1]][2]: Linear Homotopy Type Theory (). The second point has received much attention (only) in the form of semantics in “dagger-categories”, where operator adjoints are axiomatized but their specification to Hermitian adjoints still needs to be imposed by hand.

In this brief note, we describe a natural emergence of Hermiticity which is rooted in principles of equivariant homotopy theory, lends itself to homotopically-typed languages and naturally connects to topological quantum states classified by twisted equivariant KR-theory. Namely, we observe that when the complex numbers are considered as a monoid internal to \({\mathbb{Z}_{2}}\)-equivariant real linear types, via complex conjugation (the “Real numbers”), then (finite-dimensional) Hilbert spaces do become self-dual objects among internally-complex Real modules. This move absorbs the dagger-structure into the type structure; for instance, a complex linear map is unitary iff seen internally to Real modules it is orthogonal.

The point is that this construction of Hermitian forms requires of the ambient linear type theory nothing further than a negative unit term of tensor unit type. We observe that just such a term is constructible in plain , where it interprets as the non-trivial degree=0 element of the \(\infty\)-group of units of the sphere spectrum, interestingly tying the foundations of quantum theory to homotopy theory. We close by indicating how this observation allows for encoding (and verifying) the unitarity of quantum gates and of quantum channels in quantum languages embedded into , as described in [1].

\({}^*\) Mathematics, Division of Science; and
Center for Quantum and Topological Systems,
NYUAD Research Institute,
New York University Abu Dhabi, UAE.

\({}^\dagger\)The Courant Institute for Mathematical Sciences, NYU, NY

The authors acknowledge the support by Tamkeen under the NYU Abu Dhabi Research Institute grant CG008.

Quantum theory rests on two principles: (1) parameterized linearity and (2) metricity. The former is embodied by tensor-linear algebra and controls quantum phenomena such as the no-cloning/no-deleting and entanglement. The latter is embodied by quadratic forms and controls (via the Born rule) the probabilistic content of quantum physics and hence its relation to observable reality. (Extensive review and references may be found in [1].) The Hermitian core of Quantum physics.

Ever since the foundations of quantum physics were laid, [[3]][4], the quadratic form on vector spaces \(H\) of quantum states is known to arise from a Hermitian form1 \(\langle \cdot \vert \cdot \rangle\) (e.g. [5]), hence complex sesqui-linear instead of complex bi-linear (e.g. [6]): \[\label{HermitianFormInIntroduction} \big\langle c_1 \psi_1 \big\vert c_2\psi_2 \big\rangle \;=\; \overline{c}_1 c_2 \langle \psi_1 \vert \psi_2 \rangle \,, \;\;\;\;\;\;\; \langle \psi_2 \vert \psi_1 \rangle \;=\; \overline{ \langle \psi_1 \vert \psi_2 \rangle } \,.\tag{1}\] The whole probabilistic interpretation of quantum physics via the Born rule (see pointers in [1]), hence its observable content, relies on this mild failure, if you will, of complex-linearity in an otherwise complex-linear theory.

This is not a logical tautology, but a core feature of quantum physics: Complex bi-linear forms do certainly play a role elsewhere in mathematics, for instance as Killing forms on semisimple complex Lie algebras. Here we consider the question at the foundations of quantum theory: How to fundamentally (category-theoretically) think of the phenomenon of Hermitian structure underlying quantum physics?

The subtle abstract nature of Hermitian structure. Abstractly, sesqui-linear forms are more subtle than complex bi-linear forms, since the plain monoidal category \((\mathcal{C}, \otimes, \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}})\) of complex vector spaces \((\mathrm{Mod}_{\scalebox{.7}{\mathbb{C}}}, \otimes_{{}_{\mathbb{C}}}, \mathbb{C})\) does not support them: While a bi-linear form is equivalently an isomorphism in this category to the dual space, \(\begin{tikzcd}[column sep=10pt]\mathcal{V} \ar[r, shorten=-2pt, "\sim"{yshift=-1pt, pos=.4}] & \mathcal{V}^\ast := \mathrm{Map}_{\mathbb{C}}(\mathcal{V}, \mathbb{C})\end{tikzcd}\) (cf. [7]), a sesquilinear form is an anti-linear such isomorphism or equivalently a complex-linear isomorphism but to the anti-dual space \(\mathcal{V} \xrightarrow{\,\sim\,} \overline{\mathcal{V}^\ast}\): The first does not exist in \(\mathrm{Mor}(\mathrm{Mod}_{\scalebox{.7}{\mathbb{C}}})\), while the latter does not have a universal construction among \(\mathrm{Obj}(\mathrm{Mod}_{\scalebox{.7}{\mathbb{C}}})\) – not without invoking further structure. 2

The problem in typed quantum programming languages. This does become an issue when formalizing quantum information theory (eg. [12]), such as in formulating typed functional quantum programming languages: Modern quantum type systems such as Proto-Quipper [13] or [Riley22?][14] (as explained in [1]), axiomatize linear types with semantics in (parameterized versions of) distributive symmetric closed monoidal categories [[15]][16][2], but do not explicitly express anti-linear structure. In these formal languages, one can speak about inner products in terms of self-dual objects in any such monoidal category, but one just cannot speak directly about sesqui-linearity.

Of course, it is possible (see [17]) to add inference rules to linear type theories which force an involution \(\overline{(-)}\) on the type system such that function types \(\mathcal{H}_1 \to \overline{\mathcal{H}}_2\) behave like spaces of antilinear maps. However, part of the beauty at least of is that it simultaneously serves as a proof system for general abstract parameterized stable homotopy theory (cf. [1]); and here we would rather discover sesqui-linear structure than to artificially enforce it.

Motivation: Anyonic quantum states as Real K-modules. Concretely, we are motivated by our recent observation [18] [[19]][20] that spaces of anyonic quantum states — thought to be needed for topological quantum computation — have a profound description as (twisted equivariant) cohomology groups (of configuration spaces of points), receiving the Chern-character map from the same twisted equivariant K-theory which is thought to classify topological ground states of crystalline quantum materials. This makes the quantum state spaces appear via modules over the Eilenberg-MacLane spectrum \(H^{\mathrm{ev}}\mathbb{C}\) which is the complex-rationalization of the complex K-theory spectrum \(\mathrm{KU}\) (the classifying spectrum for “K-theory with complex coefficients”).

Or rather — and this is the pivotal point — since generally these topological phases are classified by Real K-theory (with capital “R”) whose equivariant spectrum \({\mathbb{Z}_{2}}\!\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathrm{KU}\) encapsulates the \({\mathbb{Z}_{2}}\)-action by complex conjugation (e.g. [21]), anyonic quantum ground states really arise via modules of the equivariant EM-spectrum \({\mathbb{Z}_{2}}\!\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, H^{\mathrm{ev}} \mathbb{C}\), being modules over the monoid \({\mathbb{Z}_{2}}\!\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}\) of complex numbers equipped with their involution by complex-conjugation.

Real modules and Real vector bundles. This suggests that the category of \({\mathbb{Z}_{2}}\!\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}\)-modules over base \({\mathbb{Z}_{2}}\)-spaces is a good context for understanding Hermitian forms. This is Atiyah’s category of Real vector bundles [22]. The now traditional capitalization “Real” was introduced by later authors who felt the need for disambiguation, while the original [22] just speaks of “real vector bundles”, suggestive of the relevance of this generalization. This hunch is maybe further confirmed by our following observations:

The Real modules. First to recall (from [22]) that Real vector bundles over the point (we will say Real modules, for short) are simply \(\mathbb{C}\)-vector spaces \(V\) equipped with anti-linear involutions \(C\), and homomorphisms between them are \(\mathbb{C}\)-linear maps which intertwine these involutions:

\[\label{CategoryOfRealModules} \mathrm{Mod}_{\scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}} \;\;\;\;\; \equiv \;\;\;\;\; \left\{ \adjustbox{ raise=-3pt }{ \begin{tikzcd}[ column sep=50pt ] \underset{ \mathclap{ \raisebox{-5pt}{ \scalebox{.7}{ \color{darkblue} \boldsymbol{\def}\arraystretch{.8} \begin{tabular}{c} Real \\ module \end{tabular} } } } }{ V_1 } \ar[out=40+90, in=-40+90, looseness=3.3, shorten <=-3pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ C_1 }}}"{pos=.5, description} ] \ar[ rr, "{ f }", "{ \scalebox{.7}{ \color{darkgreen} \boldsymbol{R}eal homomorphism } }"{swap, yshift=-1pt} ] && \underset{ \mathclap{ \raisebox{-5pt}{ \scalebox{.7}{ \color{darkblue} \boldsymbol{\def}\arraystretch{.8} \begin{tabular}{c} Real \\ module \end{tabular} } } } }{ V_2 } \ar[out=40+90, in=-40+90, looseness=3.3, shorten <=-3pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ C_1 }}}"{pos=.5, description} ] \\[-15pt] \overset{ \mathclap{ \raisebox{6pt}{ \scalebox{.7}{ \color{darkblue} \boldsymbol{\def}\arraystretch{.8} \begin{tabular}{c} \mathbb{C}-vector \\ space \end{tabular} } } } }{ W_1 } \ar[ rr, "{ f }", "{ \scalebox{.7}{ \color{darkgreen} \boldsymbol{\scalebox{1.4}}{\mathbb{C}}-linear map } }"{swap} ] \ar[ d, <->, "{ C_1 }", "{ \scalebox{.6}{ \def\arraystretch{.8} \begin{tabular}{c} anti-lin \\ involut. \end{tabular} } }"{sloped, swap, yshift=-1pt} ] && \overset{ \mathclap{ \raisebox{6pt}{ \scalebox{.7}{ \color{darkblue} \boldsymbol{\def}\arraystretch{.8} \begin{tabular}{c} \mathbb{C}-vector \\ space \end{tabular} } } } }{ W_2 } \ar[ d, <->, "{ C_2 }"{swap}, "{ \scalebox{.6}{ \def\arraystretch{.8} \begin{tabular}{c} anti-lin \\ involut. \end{tabular} } }"{sloped, yshift=0pt} ] \\ W_1 \ar[ rr, "{ f }" ] && W_2 \end{tikzcd} } \right\} \,.\tag{2}\]

This becomes a symmectric closed monoidal category \((\mathcal{C}, \otimes, \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}, \sigma)\) [23] under forming \(\mathbb{C}\)-linear tensor products equipped with the tensor involutions; the tensor unit \(\adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}\) is the “Real numbers” \(\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}\) given by \(\mathbb{C}\) equipped with its involution by complex conjugation \(\overline{(-)}\) and the symmetric braiding \(\sigma\) is that of \(\mathrm{Mod}_{\scalebox{.7}{\mathbb{C}}}\) and swapping the involutions. This monoidal category of Real modules is equivalent to that of \(\mathbb{R}\)-vector spaces, via complexification (cf. [22]): \[\label{EquivalenceBetweenRVectorSpaceAndRealVectorBundlesOverPoint} \begin{tikzcd}[ row sep=-3pt, column sep=30pt ] \overset{ \mathclap{ \raisebox{5pt}{ \scalebox{.7}{ \color{darkblue} \boldsymbol{\scalebox{1}}{\mathbb{R}}-vector spaces } } } }{ \big( \mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}}, \otimes_{{}_{\mathbb{R}}}, \mathbb{R}, \sigma_{\!{}_\mathbb{R}} \big) } \ar[ rr, "{ \sim }", "{ \scalebox{.6}{ \color{darkgreen} \boldsymbol{c}omplexification } }"{swap, yshift=-1pt} ] && \overset{ \mathclap{ \raisebox{3pt}{ \scalebox{.7}{ \boldsymbol{\color{darkblue}} Real modules } } } }{ \big( \mathrm{Mod}_{\scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}}, \otimes_{\scalebox{.6}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}}, \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}, \sigma_{{}_\mathbb{R}} \big) } \\[10pt] V \ar[ d, "{ \phi }"{swap} ] \ar[ rr, shift right=20pt, phantom, "{ \longmapsto }" ] && V \otimes_{{}_{\mathbb{R}}} \! \mathbb{C} \ar[out=-30, in=30, looseness=3.2, shorten <=-3pt, "\scalebox{1}{{\mathclap{ \overline{(-)} \mathrlap{ \scalebox{.6}{ \color{gray} complex conjugation } } }}}"{pos=.5, description} ] \ar[ d, "{ \phi \, \otimes_{{}_{\mathbb{R}}} \mathbb{C} }" {swap} ] \\[30pt] V' && V \otimes_{{}_{\mathbb{R}}} \! \mathbb{C} \ar[out=-30, in=30, looseness=3.2, shorten <=-3pt, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.5, description} ] \end{tikzcd}\tag{3}\]

We observe that it is interesting to pass inner product spaces through this equivalence:

Hermitian forms are Real inner products. It is classical that \(\mathbb{R}\)-inner product spaces \((V, g)\) with isometric complex structure \(J\) (e.g. [24])

\[\label{RealPartOfHermitianForm} \def\arraystretch{1.3} V \,\in\, \mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}} \,,\begin{array}{l} J \,:\, V \xrightarrow{\;} V \,, \\ g \,:\, V \otimes_{{}_{\mathbb{R}}} V \xrightarrow{\;} \mathbb{R} \,, \end{array}\begin{array}{l} J \circ J \,=\, - \mathrm{id}_{V}, \\ g\big( J(-) ,\, J(-) \big) \;=\; g(-,-) \end{array}\tag{4}\]

uniquely determine Hermitian forms on the corresponding complex vector space \(V_{J}\), via the formula 3

\[\label{HermitianFormInTermsOfRealMetric} \begin{tikzcd} \langle -\vert-\rangle \;:\, V_{-J} \otimes_{{}_\mathbb{C}} V_{+J} \ar[ r ] &[+4pt] \mathbb{C} \,, \end{tikzcd}\langle -\vert-\rangle \;\;\;\equiv\;\;\; g(-,-) + \mathrm{i} g\big(J(-), -\big) \,,\tag{5}\]

(e.g. [24]). However, we highlight that under the equivalence 3 they actually become these Hermitian forms, as follows:

\[\label{InnerProductsMappedToHermitianForms} \begin{tikzcd}[ row sep=0pt, column sep=41.5 ] \big( \mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}}, \otimes_{{}_{\mathbb{R}}}, \mathbb{R} \big) \ar[ rr, "{ \sim }", "{ \scalebox{.7}{ { \color{darkgreen} \boldsymbol{e}quivalence } \eqref{EquivalenceBetweenRVectorSpaceAndRealVectorBundlesOverPoint} } }"{swap} ] && \big( \mathrm{Mod}_{\scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}}, \otimes_{\scalebox{.6}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} }}, \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \big) \\[12pt] V \otimes_{{}_{\mathbb{R}}} V \ar[ d, ->>, "{ \mathrm{Eig}( J \otimes J ,\, +1 ) }"{description, pos=.4} ] \ar[ rr, phantom, "{ \mapsto }" ] && \big( V_{-J} \oplus V_{+J} \big) \otimes \big( V_{-J} \oplus V_{+J} \big) \ar[ <->, bend left=60, shift left=7pt, start anchor={[xshift={-11-33pt}]}, end anchor={[xshift={11-33pt}]}, ] \ar[ <->, bend left=60, shift left=7pt, start anchor={[xshift={-11+25pt}]}, end anchor={[xshift={11+25pt}]}, ] \ar[ d, ->>, "{ \mathrm{Eig}( \mathrm{I} \otimes \mathrm{I} ,\, +1 ) }"{description, pos=.4} ] \\[30pt] {} \ar[ d, "{ g \mathrlap{ \raisebox{-1pt}{ \scalebox{.7}{ \color{darkblue} \boldsymbol{\scalebox{1.3}}{\mathbb{R}}-inner product \color{darkgreen} corresponds to } } } }"{swap} ] && V_{-J} \otimes V_{+J} \;\;\oplus\;\; V_{+J} \otimes V_{-J} \ar[ <->, bend right=20, shift right=7pt, start anchor={[xshift=-13pt]}, end anchor={[xshift=+13pt]}, ] \ar[ d, start anchor={[xshift=-27pt]}, end anchor={[xshift=-5pt]}, "{ \mathllap{ \raisebox{1pt}{ \scalebox{.7}{ \color{darkblue} \boldsymbol{H}ermitian form } } } \langle-\vert-\rangle }"{description} ] \ar[ d, start anchor={[xshift=+27pt]}, end anchor={[xshift=+5pt]}, "{ \langle-\vert-\rangle \circ \sigma }"{description} ] \\[25pt] \mathbb{R} \ar[ rr, phantom, "{ \mapsto }" ] && \mathbb{C} \ar[out=-45-90, in=45-90, looseness=3.5, shorten=-3pt, "\scalebox{.7}{{\mathclap{ \overline{(-)} }}}"{pos=.51, description, yshift=2pt} ] \end{tikzcd}\tag{6}\]

(This map 6 of quadratic forms is closely related to the “hyperbolic functor” [26] of key relevance in Hermitian K-theory [[27]][28][29]. For discussion relating this to KR-theory see also [30].)

To see that 6 indeed follows from 3 , observe the \(\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}\)-module isomorphism (cf. [24]) \[\label{IsomorphismFromComplexficationToHyperbolicConstruction} \begin{tikzcd}[ row sep=-1pt, column sep=20pt ] \scalebox{.83}{ v + \mathrm{i} v' } \ar[ rr, phantom, pos=.65, "{ \mapsto }" ] && \scalebox{.83}{ \tfrac{1}{\sqrt{2}} \big( v - J(v') ,\, v + J(v') \big) } \\[+4pt] \mathbb{C} \otimes_{{}_\mathbb{R}}\! V \ar[out=+22+180, in=-22+180, looseness=3, shift right=6pt, shorten <=-2pt, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.5, description} ] \ar[ rr, <->, "{ \sim }" ] && V_{-J} \oplus V_{+J} \ar[ <->, bend left=40, shift left=7pt, start anchor={[xshift={-12-3pt}]}, end anchor={[xshift={12-3pt}]}, ] \\ \scalebox{.83}{ \tfrac{1}{\sqrt{2}} ( v_- + v_+ ) + \tfrac{ \mathrm{i} }{\sqrt{2}} \big( J(v_-) - J(v_+) \big) } \ar[ rr, phantom, pos=.28, "{ \mapsfrom }" ] && \scalebox{.83}{ (v_-,\, v_+) } \end{tikzcd}\tag{7}\]

which serves to diagonalize \(J \!\otimes_{{}_\mathbb{R}}\!\! \mathbb{C}\): \[\label{TheRealComplexStructure} \begin{tikzcd}[ row sep=-1pt ] \big( V \otimes_{{}_\mathbb{R}} \mathbb{C} \big) \ar[ rr, "{ ( J \otimes_{{}_\mathbb{R}}\! \mathbb{C} ) }" ] \ar[ from=d, "{ \sim }"{sloped} ] && \big( V \otimes_{{}_\mathbb{R}} \mathbb{C} \big) \ar[ d, "{ \sim }"{sloped} ] \\[15pt] \big( V_{-J} \oplus V_{+J} \big) \ar[ rr, "{ \mathrm{I} }" ] && \big( V_{-J} \oplus V_{+J} \big) \\ \scalebox{.83}{ (v_- ,\, v_+ ) } \ar[ rr, phantom, "{ \mapsto }" ] && \scalebox{.83}{ ( - \mathrm{i} v ,\, + \mathrm{i} v ) \mathrlap{\,.} } \end{tikzcd}\tag{8}\]

With 7 , the isometry condition \(g \circ (J \otimes J) = g\) on the left of 6 — which means that \(g\) factors through the \((+1)\)-eigenspace of \(J \!\otimes_{{}_\mathbb{R}}\! J\) — implies by functoriality of the equivalence 3 that the pairing on the right of 5 factors through the \((+1)\)-eigenspace of \(\mathrm{I}\otimes \mathrm{I}\) 8 , which already makes it a Hermitian form on \(V_{+J}\), as shown on the right of 6 . Explicit computation shows that this is indeed the one given by the traditional formula 5 : \[ \begin{tikzcd}[ row sep = 0pt, column sep=30pt ] V_{-J} \otimes_{{}_\mathbb{C}} V_{+J} \ar[ r, hook ] & \big( V_{-J} \oplus V_{+J} \big) \otimes_{{}_\mathbb{C}} \big( V_{-J} \oplus V_{+J} \big) \ar[ r, "{ \sim }", "{ \scalebox{.7}{ \color{gray} \scalebox{.7}{ \eqref{IsomorphismFromComplexficationToHyperbolicConstruction} } } }"{swap} ] &[-15pt] \big( V \otimes_{{}_\mathbb{R}} \! \mathbb{C} \big) \otimes_{{}_\mathbb{C}} \big( V \otimes_{{}_\mathbb{R}} \! \mathbb{C} \big) \ar[ r, "{ ( g \,\otimes_{{}_\mathbb{R}} \mathbb{C} ) \,\otimes_{{}_\mathbb{C}} ( g \,\otimes_{{}_\mathbb{R}} \mathbb{C} ) }" ] & \mathbb{C} \\ \scalebox{.83}{ v_- \otimes_{{}_\mathbb{C}} v_+ } \ar[ r, phantom, pos=.3, "{ \mapsto }" ] & \scalebox{.83}{ (v_-,0) \otimes_{{}_\mathbb{C}} (0,v_+) } \ar[ r, phantom, pos=1, "{ \mapsto }" ] & \quad \scalebox{.83}{ \tfrac{1}{2} \big( v_- + \mathrm{i} J(v_-) \big) \!\otimes_{{}_\mathbb{C}}\! \big( v_+ - \mathrm{i} J(v_+) \big) } \ar[ r, phantom, pos=1, "{ \mapsto }" ] & \quad \scalebox{.83}{ g(v_-, v_+) + \mathrm{i} g\big( J(v_-) , v_+ \big). } \end{tikzcd}\]

Inner products with isometric complex structure internal to Real modules are Hermitian forms. It is instructive to restate this equivalence in the other direction: Given a Real module equipped with a symmetric self-duality structure and an isometric complex structure (all internal to the category of Real modules!, see [1] for background):

\[\label{SelfDualRealModulesWithIsometricComplexStructure} \def\arraystretch{1.2} \begin{array}{ccc}\color{gray} \begin{tabular}{c} Real module \end{tabular}& \begin{tikzcd}[sep=0pt] \ar[out=-40+180, in=40+180, looseness=3.3, shorten <=-3pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ C }}}"{pos=.5, description} ] \mathcal{H} &\in& \mathrm{Mod}_{\scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}} \end{tikzcd} \\\color{gray} \def\arraystretch{.9} \begin{tabular}{c} Symmetric \\ inner product \end{tabular}& \adjustbox{raise=-10pt}{ \begin{tikzcd} \mathbb{C} \ar[out=-41+90, in=41+90, looseness=3.7, shorten <=-2pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.5, description} ] \ar[ r, "{ \Delta }" ] & \mathcal{H} \otimes_{{}_\mathbb{C}} \mathcal{H} \ar[out=-41+90, in=41+90, looseness=3.7, shorten <=-2pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ C \otimes C }}}"{pos=.5, description} ] \ar[ rr, "{ (-,-) }" ] && \ar[out=-41+90, in=41+90, looseness=3.7, shorten <=-2pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.5, description} ] \mathbb{C} \end{tikzcd} } & \def\arraystretch{1.4} \begin{array}{c} \big( (-) \otimes (-,-) \big) \circ \big( \Delta \otimes (-) \big) \;=\; \mathrm{id}_{\mathcal{H}} \\ \big( (-,-) \otimes (-) \big) \circ \big( (-) \otimes \Delta \big) \;=\; \mathrm{id}_{\mathcal{H}} \\ (-,-) \circ \sigma \;=\; (-,-) \end{array} \\\color{gray} \def\arraystretch{.9} \begin{tabular}{c} Isometric \\ complex structure \end{tabular}& \begin{tikzcd} \mathcal{H} \ar[out=-41+90, in=41+90, looseness=3.7, shorten <=-2pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ C }}}"{pos=.5, description} ] \ar[ rr, "{ \mathrm{I}}" ] && \mathcal{H} \ar[out=-41+90, in=41+90, looseness=3.7, shorten <=-2pt, shorten >=-3pt, "\scalebox{1}{{\mathclap{ C }}}"{pos=.5, description} ] \end{tikzcd} & \def\arraystretch{1.2} \begin{array}{c} \mathrm{I}\circ \mathrm{I} \,=\, - \mathrm{id}_{\mathcal{H}} \\ \big( \mathrm{I}(-) ,\, \mathrm{I}(-) \big) \;=\; (-,- ) \end{array} \end{array}\tag{9}\] we recognize it as encoding a Hermitian form as follows. Observing that \(\mathrm{I}\) is \(\mathbb{C}\)-diagonalizable with \(\mp \mathrm{i}\)-eigenspaces swapped by the anilinear involution (for instance by applying the previous argument 8 to \(J \,\equiv\, \mathrm{I}^{{\mathbb{Z}_{2}}}\)) \[\label{UnderlyingSpaceOfComplexRealModule} \begin{tikzcd} \mathcal{H} \ar[out=+32+180, in=-32+180, looseness=4, shift right=4pt, shorten <=-0pt, "\scalebox{1}{{\mathclap{ C }}}"{pos=.5, description} ] \ar[ rr, <->, "{ \sim }" ] && \overline{H} \oplus H \mathrlap{\,,} \ar[ <->, bend left=40, shift left=9pt, start anchor={[xshift={-8-0pt}]}, end anchor={[xshift={8-0pt}]}, ] \end{tikzcd}\tag{10}\]

the isometry property of \(\mathrm{I}\) implies that \((-,-)\) is non-vanishing only on the \(+1\) eigenspace of \(\mathrm{I}\otimes \mathrm{I}\), which is the mixed summands \(\begin{tikzcd} \!\! \overline{H} \!\otimes\! H \;\oplus\; H \!\otimes\! \overline{H} \ar[ <->, shift left=6pt, bend left=23, start anchor={[xshift={-17pt}, yshift=+1pt]}, end anchor={[xshift={18pt}, yshift=+1pt]}, ] \end{tikzcd}\). Here the inner product \((-,-)\) exhibits \(\overline{H}\) as the dual object (cf. [[31]][9]) of \(H\), inducing a \(\mathbb{C}\)-linear identification of \(H\) with its anti-dual space, this defining (e.g. [29]) a sesqui-linear form \(\langle - \vert - \rangle\): \[\begin{tikzcd}[row sep=-2pt] H \ar[ rr, "{ \sim }" ] && \overline{H}^\ast \\ \scalebox{.83}{ \vert \psi \rangle } \ar[ rr, phantom, "{ \mapsto }" ] && \scalebox{.83}{ \langle \psi \vert } \,, \end{tikzcd}\]

which is forced to be Hermitian by symmetry and \({\mathbb{Z}_{2}}\)-equivariance of \((-,-)\) (on the right, \(\big\{\vert w \rangle\big\}_{w \in W}\) is any orthonormal basis): \[\label{CoEvaluationForHilbertSpaceAsSDObject} \begin{tikzcd}[row sep=10pt] \big( H \oplus H^\ast \big) \ar[ <->, shift left=8pt, bend left=30, start anchor={[xshift=-8pt]}, end anchor={[xshift=+8pt]}, ] \ar[ r, phantom, "{\otimes}" ] &[-24pt] \big( H \oplus H^\ast \big) \ar[ <->, shift left=8pt, bend left=30, start anchor={[xshift=-8pt]}, end anchor={[xshift=+8pt]}, ] \ar[ rr, "{ (-,-) }" ] && \mathbb{C} \ar[out=180-60, in=60, looseness=4.6, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.41, description}, shift right=0, start anchor={[xshift=-0pt]}, end anchor={[xshift=-0pt]}, ] \\[-12pt] \scalebox{.83}{ \mathrlap{ \;\; \langle \psi_1 \vert } } \ar[ r, phantom, "{ \otimes }" ] & \scalebox{.83}{ \mathllap{ \vert \psi_2 \rangle \;\; } } \ar[ d, |->, shift right=22pt, shorten=1pt ] \ar[ rr, |->, shorten=20pt ] && \scalebox{.83}{ \langle \psi_1 \vert \psi_2 \rangle } \ar[ d, |->, shorten=1pt ] \\ \scalebox{.83}{ \mathrlap{ \;\; \vert \psi_1 \rangle } } \ar[ r, phantom, "{ \otimes }" ] & \scalebox{.83}{ \mathllap{ \langle \psi_2 \vert \;\; } } \ar[ r, |->, shorten >=10pt, shorten <=23pt ] & \scalebox{.83}{ \langle \psi_2 \vert \psi_1 \rangle } \ar[ r, equals ] & \scalebox{.83}{ \overline{ \langle \psi_1 \vert \psi_2 \rangle } } \\ \scalebox{.83}{ \mathrlap{ \;\; \vert \psi_1 \rangle } } \ar[ r, phantom, "{ \otimes }" ] & \scalebox{.83}{ \mathllap{ \vert \psi_2 \rangle \;\; } } \ar[ d, |->, shift right=24pt, shorten=1pt ] \ar[ rr, |->, shorten=25pt ] && \scalebox{.83}{ 0 } \ar[ d, |->, shorten=2pt ] \\ \scalebox{.83}{ \mathrlap{ \;\; \langle \psi_1 \vert } } \ar[ r, phantom, "{ \otimes }" ] & \scalebox{.83}{ \mathllap{ \langle \psi_2 \vert \;\; } } \ar[ rr, |->, shorten=25pt ] && \scalebox{.83}{ 0 } \end{tikzcd}\begin{tikzcd}[row sep=10pt] \mathbb{C} \ar[out=180-60, in=60, looseness=4.6, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.41, description}, shift right=0, start anchor={[xshift=-0pt]}, end anchor={[xshift=-0pt]}, ] \ar[ rr, "{ \Delta }" ] && \big( H \oplus H^\ast \big) \ar[ <->, shift left=8pt, bend left=30, start anchor={[xshift=-8pt]}, end anchor={[xshift=+8pt]}, ] \ar[ r, phantom, "{\otimes}" ] &[-24pt] \big( H \oplus H^\ast \big) \ar[ <->, shift left=8pt, bend left=30, start anchor={[xshift=-8pt]}, end anchor={[xshift=+8pt]}, ] \\[-8pt] \scalebox{.83}{ 1 } \ar[ dd, |->, shorten=12pt, ] \ar[ rr, |->, shorten=15pt ] && \scalebox{.83}{ \sum_w \; \vert w \rangle }\ar[ r, phantom, "{ \otimes }"{pos=.26} ] &\scalebox{.83}{ \langle w \vert } \\[-10pt] && \scalebox{.83}{ + \sum_w \; \langle w \vert } \; \ar[ r, phantom, "{ \otimes }"{pos=.08} ] &\scalebox{.83}{ \vert w \rangle } \ar[ d, |->, shift right=23pt, shorten=2pt ] \\[+10pt] \scalebox{.83}{ 1 } \ar[ rr, |->, shorten=15pt ] && \scalebox{.83}{ \sum_w \; \langle w \vert }\ar[ r, phantom, "{ \otimes }"{pos=.26} ] &\scalebox{.83}{ \vert w \rangle } \\[-10pt] && \scalebox{.83}{ + \sum_w \; \vert w \rangle } \; \ar[ r, phantom, "{ \otimes }"{pos=.06} ] &\scalebox{.83}{ \langle w \vert } \end{tikzcd}\tag{11}\]

The dagger emerges. Observe now that the internally complex-linear morphisms \(G \,:\,\mathcal{H}_1 \to \mathcal{H}_2\) of self-dual Real modules with internal complex structure \(\mathrm{I}\) 9 — hence the Real homomorphisms \(G\) satisfying \(G \circ \mathrm{I}_1 \,=\, \mathrm{I}_2 \circ G\) — bijectively correspond to ordinary \(\mathbb{C}\)-linear maps \(g \,:\,H_1 \to H_2\) between the \((+ \mathrm{i} )\)-eigenspaces 10 – because \({\mathbb{Z}_{2}}\)-equivariance forces the other component to be the Hermitian adjoint operator \(g^\dagger\), defined by \(\langle - \vert g^\dagger - \rangle \,=\, \langle g - \vert - \rangle\) (e.g. [5]): \[\label{ComplexLinearMapsAsIBetaComplexLinearRealHomomorphisms} \adjustbox{raise=4pt}{ \begin{tikzcd}[ row sep=-2pt, column sep=15pt ] \mathllap{ g \;:\;\; } H_1 \ar[ rr, "{ \scalebox{.7}{ \rm \scalebox{1.2}{\mathbb{C}}-linear map } }" ] && H_2 \\ \scalebox{.83}{ \vert \psi \rangle } &\mapsto& \scalebox{.83}{ g \vert \psi \rangle } \end{tikzcd} }\leftrightarrow\begin{tikzcd}[ column sep=40pt, row sep=5pt ] \mathllap{ G \;\;:\;\; } \mathcal{H}_1 \ar[ rr, "{ \scalebox{.8}{ \rm\def\arraystretch{.9} \begin{tabular}{c} \scalebox{1.3}{\mathrm{I}}-complex-linear \\ Real-module homom. \end{tabular} } }" ] &\phantom{----}& \mathcal{H}_2 \\[-4pt] \scalebox{.83}{ \vert \psi \rangle } \ar[ dd, |->, shorten=2pt ] \ar[ rr, |->, shorten=25pt ] && \scalebox{.83}{ g\vert \psi \rangle } \ar[ dd, |->, shorten=2pt ] \\ \\ \scalebox{.83}{ \langle \psi \vert } \ar[ r, |->, shorten=2pt ] & \scalebox{.83}{ \langle \psi \vert \, {\color{purple}g^\dagger} } \ar[ r, equals ] & \scalebox{.83}{ \langle g \psi \vert } \mathrlap{\,.} \end{tikzcd}\tag{12}\]

In particular, the internally isometric internally-complex-linear Real module homomorphisms correspond bijectively to the complex isometries on the underlying Hermitian spaces: \[\label{InternalIsometryProperty} \begin{tikzcd}[row sep=-3pt, column sep=2pt] \mathcal{H}_1 \otimes \mathcal{H}_1 \ar[ rrrr, "{ G \,\otimes\, G }" ] \ar[ dddd, "{ (-,-)_1 }" {swap} ] &&&& \mathcal{H}_2 \otimes \mathcal{H}_2 \ar[ dddd, "{ (-,-)_2 }" ] \\ & \scalebox{.83}{ \langle \phi \vert \otimes \vert \psi \rangle } \ar[ dd, phantom, "{ \longmapsto }"{sloped} ] &\longmapsto& \scalebox{.83}{ \langle \phi \vert g^\dagger \otimes g \vert \psi \rangle } \\ & \rotatebox[origin=c]{-90}{\longmapsto} && \rotatebox[origin=c]{-90}{\longmapsto} \\ & \scalebox{.83}{ \langle \phi \vert \psi \rangle } \ar[ rr, equals ] && \scalebox{.83}{ \langle \phi \vert g^\dagger g \vert \psi \rangle } \\ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \ar[ rrrr, equals ] &&&& \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \end{tikzcd}\tag{13}\]

hence to unitary operators iff they are also invertible; and the dagger-functor on the category of Hermitian spaces is now just the duality-involution (cf. eg. [9]) on this category of self-dual Real modules, as shown here: \[\label{HermitianAdjointFromSelfDuality} \begin{tikzcd}[ row sep=-5pt, column sep=10pt ] & & \mathcal{H}_1 \ar[ rr, equals ] && \mathcal{H}_1 \ar[ rr, equals ] && \mathcal{H}_1 \\ & \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \ar[ r, "{ \Delta }" ] & \otimes && \otimes \\ & & \mathcal{H}_1 \ar[ rr, "{ G }" ] &\phantom{---}& \mathcal{H}_2 \\ & & \otimes && \otimes \ar[ r, "{ (-,-) }" ] & \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \\ \mathcal{H}_2 \ar[ rr, equals ] && \mathcal{H}_2 \ar[ rr, equals ] && \mathcal{H}_2 \\[+5pt] \scalebox{.83}{ \vert \psi \rangle } \ar[ rr, phantom, "{ \mapsto }" ] & & \def\arraystretch{.9} \begin{array}{r} \scalebox{.83}{ \underset{ w }{\sum} \, \vert w \rangle \otimes \langle w \vert \otimes \vert \psi \rangle } \\ \scalebox{.83}{ + \, \underset{ w }{\sum} \, \langle w \vert \otimes \vert w \rangle \otimes \vert \psi \rangle } \end{array} \ar[ rr, phantom, "{ \mapsto }" ] && \def\arraystretch{.9} \begin{array}{r} \scalebox{.83}{ \underset{ w }{\sum} \, \vert w \rangle \otimes \langle w \vert \, g^\dagger \otimes \vert \psi \rangle } \\ \scalebox{.83}{ +\, \underset{ w }{\sum} \, \langle w \vert \otimes \; g \, \vert w \rangle \otimes \vert \psi \rangle } \end{array} \ar[ rr, phantom, "{ \mapsto }" ] && \scalebox{.83}{ \underset{ { \color{purple} g^\dagger } \, \vert \psi \rangle }{ \underbrace{ \underset{w}{\textstyle{\sum}} \vert w \rangle \langle w \vert G^\dagger \vert \psi \rangle }} } \end{tikzcd}\tag{14}\]

Hermitian operators as Real matrices. Similarly, we find that “density matrices”, hence Hermitian operators on (finite-dimensional, in our case) Hilbert spaces (see [1] for background) are just the complex symmetric matrices internal to Real modules. The Real space \(\mathrm{CSMat}(\mathcal{H})\) of internally-complex (C) and symmetric (S) matrices on an internally complex self-dual Real space \(\mathcal{H}\) is the following iterated equalizer: \[\begin{tikzcd}[column sep=large] \mathrm{CSMat}(\mathcal{H}) \ar[r] \ar[d] \ar[ dr, phantom, "{ \scalebox{.7}{(pb)} }" ] & \mathrm{CMat}(\mathcal{H}) \ar[ d, hook, "{ \mathrm{eq} }" ] \ar[ rr, dashed, "{ \mathrm{braid}^{\scalebox{.7}{ \otimes }}_{\scalebox{.7}{ \mathrm{CMat}(\mathcal{H}) }} }" ] && \mathrm{CMat}(\mathcal{H}) \ar[ d, hook, "{ \mathrm{eq} }" ] \\ \mathrm{SMat}(\mathcal{H}) \ar[ r, hook, "{ \mathrm{eq} }" ] \ar[ dd, dashed, "{ \mathrm{I} \,\otimes\, \mathrm{I}_{ \vert \mathrm{SMat}(\mathcal{H}) } }"{description} ] & \mathcal{H} \otimes \mathcal{H} \ar[ rr, shift left=6pt, "{ \mathrm{braid}^{\scalebox{.7}{ \otimes }}_{\scalebox{.7}{ \mathcal{H} \otimes \mathcal{H} }} }"{description} ] \ar[ rr, shift right=6pt, "{ \mathrm{id} }"{description} ] \ar[ dd, shift left=7pt, "{ \mathrm{I} \,\otimes\, \mathrm{I} }"{description} ] \ar[ dd, shift right=7pt, "{ \mathrm{id} }"{description} ] && \mathcal{H} \otimes \mathcal{H} \ar[ dd, shift left=7pt, "{ \mathrm{I} \,\otimes\, \mathrm{I} }"{description} ] \ar[ dd, shift right=7pt, "{ \mathrm{id} }"{description} ] \\ \\ \mathrm{SMat}(\mathcal{H}) \ar[ r, hook, "{ \mathrm{eq} }" ] & \mathcal{H} \otimes \mathcal{H} \ar[ rr, shift left=6pt, "{ \mathrm{braid}^{\scalebox{.7}{ \otimes }}_{\scalebox{.7}{ \mathcal{H} \otimes \mathcal{H} }} }"{description} ] \ar[ rr, shift right=6pt, "{ \mathrm{id} }"{description} ] && \mathcal{H} \otimes \mathcal{H} \end{tikzcd}\] Unwinding the definitions, one has \[\begin{tikzcd}[ row sep=0pt ] \mathllap{ \mathrm{CMat}(\mathcal{H}) \;\simeq\;\; } \big( H \!\otimes_{{}_\mathbb{C}}\! H^\ast \,\oplus\, H^\ast \!\otimes_{{}_\mathbb{C}}\! H \big) \ar[ <->, bend left=25pt, shift left=9pt, start anchor={[xshift=-22pt]}, end anchor={[xshift=+20pt]}, ] \ar[ rr, "{ \mathrm{braid}^{\scalebox{.7}{ \otimes }}_{\scalebox{.7}{ \mathrm{CMat}(\mathcal{H}) }} }" ] && \big( H \!\otimes_{{}_\mathbb{C}}\! H^\ast \,\oplus\, H^\ast \!\otimes_{{}_\mathbb{C}}\! H \big) \ar[ <->, bend left=25pt, shift left=9pt, start anchor={[xshift=-22pt]}, end anchor={[xshift=+20pt]}, ] \\ \scalebox{.83}{ \vert \psi \rangle \otimes \langle \phi \vert { \;\; \color{gray}\leftrightarrow\; \langle \psi \vert \otimes \vert \phi \rangle } } \ar[ rr, phantom, "{ \longmapsto }" ] && \scalebox{.83}{ { \color{gray}\vert \phi \rangle \otimes \langle \psi \vert \;\leftrightarrow\; } \langle \phi \vert \otimes \vert \psi \rangle } \mathrlap{\,,} \end{tikzcd}\] which means that the \({\mathbb{Z}_{2}}\)-fixed locus of \(\mathrm{CMat}(\mathcal{H})\) is identified with the \(\mathbb{R}\)-vector space underlying \(H \!\otimes_{{}_\mathbb{C}}\! H^\ast\), under which identification the braiding acts as the Hermitian adjoint operation \((-)^\dagger \,:\, \vert \psi \rangle \langle \phi \vert \,\mapsto\, \vert \phi \rangle \langle \psi \vert\):


\[\begin{tikzcd}[ row sep=-2pt, column sep=small ] \mathrm{CMat}(\mathcal{H})^{{\mathbb{Z}_{2}}} \ar[ dddd, hook ] &[+10pt] H \otimes_{{}_\mathbb{C}} H^\ast \ar[ rrrr ] \ar[ dddd, hook ] &[-30pt] && &[-30pt] H \otimes_{{}_\mathbb{C}} H^\ast \ar[ dddd, hook ] \\ & & \scalebox{.83}{ \vert \psi \rangle \langle \phi \vert } &\longmapsto& \scalebox{.83}{ \vert \phi \rangle \langle \psi \vert } \\ & & \rotatebox[origin=c]{-90}{\longmapsto} && \rotatebox[origin=c]{-90}{\longmapsto} \\ & & \scalebox{.83}{ \vert \psi \rangle \otimes \langle \phi \vert \;+\; \langle \psi \vert \otimes \vert \phi \rangle } &\longmapsto& \scalebox{.83}{ \vert \phi \rangle \otimes \langle \psi \vert \;+\; \langle \phi \vert \otimes \vert \psi \rangle } \\ \mathrm{CMat}(\mathcal{H}) & \big( H \!\otimes_{{}_\mathbb{C}}\! H^\ast \,\oplus\, H^\ast \!\otimes_{{}_\mathbb{C}}\! H \big) \ar[ rrrr, "{ \mathrm{braid}^{\scalebox{.7}{ \otimes }}_{\scalebox{.7}{ \mathrm{CMat}(\mathcal{H}) }} }"{swap} ] &&&& \big( H \!\otimes_{{}_\mathbb{C}}\! H^\ast \,\oplus\, H^\ast \!\otimes_{{}_\mathbb{C}}\! H \big) \end{tikzcd}\]

This reveals \(\mathrm{CSMat}(\mathcal{H})\) as the Real space corresponding under 3 to the \(\mathbb{R}\)-vector space of Hermitian operators: \[\mathrm{CSMat}(\mathcal{H}) \;\simeq\; \mathrm{Herm}\big( H ,\, \langle-\vert-\rangle \big) \otimes_{{}_\mathbb{R}}\begin{tikzcd} \mathbb{C} \ar[out=-40, in=40, looseness=3.4, shorten <=-3pt, shift left=3pt, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.5, description} ] \end{tikzcd}\]

The Real incarnation of a unitary quantum channel induced by a unitary operator 12 is hence simply: \[\begin{tikzcd}[row sep=0pt, column sep=large ] \scalebox{.83}{ \vert \psi \rangle \langle \phi \vert } &\longmapsto& \scalebox{.83}{ g\, \vert \psi \rangle \langle \phi \vert \, g^\dagger } \\ \mathcal{H} \otimes \mathcal{H} \ar[ rr, "{ G \,\otimes\, G }" ] && \mathcal{H} \otimes \mathcal{H} \\[15pt] \mathrm{CSMat}(\mathcal{H}) \ar[ rr ] \ar[ u, hook ] && \mathrm{CSMat}(\mathcal{H}) \ar[ u, hook ] \\[-3pt] \scalebox{.83}{ \rho } &\longmapsto& \scalebox{.83}{ g \cdot \rho \cdot g^\dagger } \end{tikzcd}\]

In conclusion so far, the above shows that the Hermitian structures in the foundations of quantum information theory are naturally expressed by isometrically complex self-dual objects 9 internal to the category of Real modules. Since the latter is monoidally equivalent 3 to that of \(\mathbb{R}\)-vector spaces, the same is already true there, where the above constructions amount to strictly referring to Hermitian forms only through their real part 5 regarded as a symmetric form on the underlying \(\mathbb{R}\)-vector space 4 – which is an elementarily equivalent but unusual perspective. It is only when that same construction is transported back through the equivalence with Real modules 3 that all the familiar \(\mathbb{C}\)-component formulas of quantum theory manifest themselves, such as for Hermitian adjoints 14 .

However, abstractly, such as for formal languages, the component expressions are invisible/irrelevant anyway – they are part of the “semantics” (the model) but not of the “syntax” (the theory). One may understand these observations as one way of seeing “why” the (spectral) theory of Hermitian forms on \(\mathbb{C}\)-vector famously parallels that of symmetric inner products on \(\mathbb{R}\)-vector spaces: They secretly are symmetric inner products when seen internally to Real modules.

In amplification of this point, we now indicate how one may formalize (finite-dimensional) Hilbert space structure internal to a formal language like , without introducing further inference rules for anti-linear maps.

Formalization in linearly homotopy-typed languages. Looking back, one may notice that the only property of the tensor unit \(\adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}\,\equiv\, \mathbb{R}\) in the symmetric closed monoidal category \((\mathcal{C}, \otimes, \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}, \sigma) \,\equiv\,(\mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}}, \otimes_{{}_\mathbb{R}}, \mathbb{R}, \sigma_{{}_\mathbb{R}})\) that we used above — namely for saying “internal complex structure” in 4 and 9 — is that it contains a negative unit scalar, in the sense of a non-trivial involutive endomorphism: \[\label{NegativeUnitScalar} -\mathrm{id} \,:\, \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \to \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} ,\;\;\big(-\mathrm{id} = \mathrm{id}\big) \,\to\, \varnothing , -\mathrm{id} \circ -\mathrm{id} \,=\, \mathrm{id} \,.\tag{15}\] Trivial as this may seem, it is not generally the case for tensor units of monoidal categories and it needs an argument that a term like 15 is constructible in a given formal language for such categories. Interestingly, that this is the case for relies on its homotopy-theoretic nature. In indicating now how this works, we will here not go into the formal syntax of , but discuss the relevant universal constructions in its expected categorical sematics which interpret this term:

Namely, in refinement of how plain has categorical semantics in general \(\infty\)-toposes (see [20] for pointers)4 and expresses the universal constructions that are generically available in all of them, so is meant to have categorical semantics in “tangent \(\infty\)-toposes” of parameterized \(R\)-module spectra (for \(R\) an \(E_\infty\)-ring, for pointers see [1]) and to express the universal constructions generically available in all of these.

Since such tangent \(\infty\)-topos is meant to be (categorical semantics for) the type universe of we suggestively denote it by “\(\mathrm{Type}\)”, as in [1], with the reflective sub-\(\infty\)-categories of purely classical types (homotopy types, \(\infty\)-groupoids) and of purely linear (quantum) types (module spectra) denoted

\[\label{TheToposOfTypes} \begin{tikzcd}[ row sep=0pt, column sep=large ] \mathrm{Cla}\mathrm{Type} \quad \ar[ r, hook, shift right=5pt ] \ar[ from=r, ->>, shift right=5pt, "{ \natural}"{swap} ] \ar[ r, phantom, "{ \scalebox{.7}{\bot} }" ] & \quad \mathrm{Type}\quad & \quad \mathrm{Qu}\mathrm{Type} \ar[ l, hook', shift left=5pt ] \ar[ from=l, ->>, shift left=5pt, "{ \raisebox{-0pt}{\scalebox{.95}{\rotatebox{30}{\triangle}}}}" ] \ar[ l, phantom, "{ \scalebox{.7}{\bot} }" ] \\ \scalebox{.83}{ \left\{\, \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { 0 } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { X } \end{array} \right] \, \right\} } & \scalebox{.83}{ \left\{\, \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V_\bullet } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { X } \end{array} \right] \, \right\} } & \scalebox{.83}{ \left\{\, \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \ast } \end{array} \right] \, \right\} } \mathrlap{\,.} \end{tikzcd}\tag{16}\]

The doubly symmetric closed monoidal structure. Here

  • \(\mathrm{Cla}\mathrm{Type}\) is Cartesian monoidal with Cartesian product denoted \(\times\) and tensor unit denoted \(\ast\),

  • \(\mathrm{Qu}\mathrm{Type}\) is symmetric monoidal with tensor product \(\otimes\) and tensor unit \(\adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}\), distributing over a Cartesian biproduct (direct sum) \(\oplus\) with tensor unit the zero object,

  • \(\mathrm{Type}\) is doubly monoidal with the corresponding “external” Cartesian and tensor products (cf. [2], here to be denoted by the same symbols \(\times\) and \(\otimes\), respectively),

such that all functors in 16 are strong monoidal.

Moreover, \(\mathrm{Qu}\mathrm{Type}\) is stable (in the sense of [32], namely under suspension), meaning that for \(V \,\in\, \mathrm{Qu}\mathrm{Type}\) the canonical comparison map to the looping \(\Omega(-)\) of its suspension \(\Sigma(-)\) is an equivalence (cf. [32]):

\[\begin{tikzcd}[row sep=7pt, column sep=20pt] & 0 \ar[ dr, shorten=-2pt ] \ar[ dd, Rightarrow, shorten=4pt, "{ \scalebox{.7}{(po)} }"{description, pos=.47} ] \\ V \ar[ ur, shorten=-2pt ] \ar[ dr, shorten=-2pt ] && \Sigma V \mathrlap{\,,} \\ & 0 \ar[ ur, shorten=-2pt ] \end{tikzcd}\begin{tikzcd}[sep=7pt, column sep=20pt] & 0 \ar[ dr, shorten=-2pt ] \ar[ dd, Rightarrow, shorten=4pt, "{ \scalebox{.7}{(pb)} }"{description, pos=.47} ] \\ \Omega V \ar[ ur, shorten=-2pt ] \ar[ dr, shorten=-2pt ] && V \mathrlap{\,,} \\ & 0 \ar[ ur, shorten=-2pt ] \end{tikzcd}\begin{tikzcd}[ column sep=20pt, row sep=4pt ] &[8pt] &[-8pt] 0 \ar[ddrr] \\ \\ V \ar[ uurr, bend left=10pt ] \ar[ ddrr, bend right=10pt ] \ar[ r, dashed, "{ \sim }" ] & \Omega \Sigma V \ar[ uur, end anchor={[xshift=3.5pt]} ] \ar[ ddr, end anchor={[xshift=3.5pt]} ] &&& \Sigma V \, . \\ \\ && 0 \ar[uurr] \end{tikzcd}\]

Of interest for our application to quantum information theory is the case where the ground \(E_\infty\)-ring is the real Eilenberg-MacLane spectrum \(R \,\equiv\, H\mathbb{R}\), in which case \(\mathrm{Type}\) is equivalently the flat \(\infty\)-vector bundles or \(\infty\)-local systems, see [2], hence \(\mathrm{Qu}\mathrm{Type}\) is equivalently given by \(\mathbb{R}\)-chain complexes; see 19 below.

The negative unit scalar in . If we denote the homotopy exhibiting the suspension type (cf. [20]) of the tensor unit \(\adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}\) by \(s\), then its inverse \(s^{-1}\) induces an endomorphism of \(\Sigma \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}\) (by the universal property of the pushout) whose looping is the scalar which we may denote by “\(-\mathrm{id}\)”:

\[\label{TheNegativeUnitScalar}\begin{tikzcd}[ column sep=25pt, row sep=10pt ] & 0 \ar[ dr, shorten=-2pt ] \ar[ dd, Rightarrow, shorten=4pt, "{ s }", "{ \scalebox{.65}{(po)} }"{swap} ] \\ \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \ar[ ur, shorten=-2pt ] \ar[ dr, shorten=-2pt ] && \Sigma \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \\ & 0 \ar[ ur, shorten=-2pt ] \end{tikzcd}\begin{tikzcd}[ column sep=30pt, row sep=6pt ] &[-10pt] & 0 \ar[ ddr, "{\;}"{swap, pos=.1, name=s1} ] \ar[ ddrr, bend left=10pt, "{\;}"{swap, pos=.2, name=s2} ] &&[+10pt] \\ \\ \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \ar[uurr] \ar[ ddrr, "{\;}"{name=t1, pos=.8} ] &&& \Sigma \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \ar[ r, dashed, "{ \Sigma(-\mathrm{id}) }"{pos=.35}, "{ \sim }"{swap, pos=.35} ] & \Sigma \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \mathrlap{\,,} \\ \\ && 0 \ar[ uurr, bend right=10pt, "{\;}"{pos=.2, name=t2} ] \ar[ uur ] \ar[ from=s1, to=t1, Rightarrow, "{ s }"{description} ] \ar[ from=s2, to=t2, Rightarrow, crossing over, "{ s^{-1} }"{description} ] \end{tikzcd}-\mathrm{id} \,=\, \Omega \Sigma(-\mathrm{id}) \;:\; \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \to \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \mathrlap{\,.}\tag{17}\]

The desired characteristic properties 15 of this \(-\mathrm{id}\) 17 follow immediately from similar uses of the universal property of the defining pushouts. In the language of higher algebra, this is the non-trivial element of degree=0 in \(\mathrm{GL}(1, \mathbb{S})\), the “group of units of the sphere spectrum” (cf. [[33]][34]): \(\pi_0\big(\mathrm{GL}(1,\mathbb{S})\big) = \big(\pi_0\mathbb{S}\big)^\times \,=\, \mathbb{Z}^\times \,=\, {\mathbb{Z}_{2}}\).

The heart of . With the negative unit scalar 17 in hand, it is immediate to define data structures (see [20] for background) in \(\mathrm{Qu}\mathrm{Type}\) of symmetric inner product spaces with isometric complex structure according to 9 . The only further subtlety to take care of is that the definition 9 comes out as intended (only) on linear base types which are in the “heart” of \(\mathrm{Qu}\mathrm{Type}\). For completeness, we briefly explain this. In plain the \(n\)-truncation modality (for \(n \in \mathbb{N}\), see [20] for pointers) sends a homotopy type \(X \,:\, \mathrm{Type}\) to a type \([X]_n \,:\, \mathrm{Type}\) which left-universally approximates \(X\) while containing no non-trivial \((n+1)\)-fold homotopies. In particular, the ordinary definitions of mathematical structures, such as of groups (cf. [20]), come out as intended (only) on 0-truncated base types \(X = [X]_0\). Instead, for higher base types these definitions need to be refined to “higher structures”. While higher structures are profoundly interesting — and while we have here at our fingertips a definition of higher “\((\infty,1)\)-Hilbert spaces” (of finite type) which is worth exploring further — for the scope of this note we want to restrict attention to ordinary quantum state spaces.

To that end, the further subtlety in is that in a stable \(\infty\)-category like the \(\mathrm{Qu}\mathrm{Type}\), the plain notion of truncation becomes meaningless: For all \(n \in \mathbb{N}\), the only object of \(\mathrm{Qu}\mathrm{Type}\) which is \(n\)-truncated is the 0-object ([32]). Instead, the proper notion that replaces \(n\)-truncation in stable \(\infty\)-categories are “t-structures” ([32]), and the stable (i.e., linear) analog of the 0-truncated sector is the “heart” of the t-structure ([32]).

Concretely, the heart of may be characterized as follows. Consider the function which sends a quantum type to \[\Omega^\infty \;\equiv\; \natural\big( \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \to (-) \big) \;:\; \mathrm{Qu}\mathrm{Type} \longrightarrow \mathrm{Cla}\mathrm{Type} \,,\]

the classicalization 16 of its internal hom out of the tensor unit (cf. [Riley22?][1]). Then a linear type belongs to the heart iff

  • under classicization \(\natural\) 16 it is identified with its 0-truncation,

  • the 0-truncations of the classicization of all its suspensions are contractible: (cf. [32]): 5

\[\label{ConditionForTheHeart} \mathrm{Qu}\mathrm{Type}^\heartsuit \;\; \equiv \;\; \Big(\, V \,:\, \mathrm{Qu}\mathrm{Type} ,\;\;\; \Omega^\infty V \,=\, [\Omega^\infty V]_0 ,\;\;\; \underset{n \in \mathbb{N}}{\forall}\; [\Omega^\infty \Sigma^n V]_0 \,=\, \ast \, \Big)\, .\tag{18}\]

In particular, the heart of \(H\mathbb{R}\)-module-spectra is the ordinary category of \(\mathbb{R}\)-vector spaces: \[\label{HeartOfHRSpectra} \big( \mathrm{Mod}_{\scalebox{.7}{H\mathbb{R}}} ,\, \otimes_{{}_{H\mathbb{R}}} ,\, H\mathbb{R} ,\, \sigma_{{}_{H\mathbb{R}}} \big)^\heartsuit \;\simeq\; \big( \mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}} ,\, \otimes_{{}_{\mathbb{R}}} ,\, \mathbb{R} ,\, \sigma_{{}_{\mathbb{R}}} \big) \,.\tag{19}\]

In conclusion, for the purpose of using as a universal quantum programming and certification language (as laid out in [1], in certifiable refinement of the Proto- language), one may code (finite-dimensional) Hilbert spaces in as heart-types 18 among purely linear types 16 equipped with symmetric self-duality and isometric complex structure as in 9 , using the negative unit scalar type 17 . When interpreted into \(H\mathbb{R}\)-module spectra (as in [2]), this gives, up to equivalence 6 , the ordinary symmetric closed monoidal category of (finite-dimensional) \(\mathbb{C}\)-Hilbert spaces with isometries between them, whose dagger-structure is induced by plain dualization 14 .

Outlook. The restriction to the heart of in 18 serves the purpose (only) of showing that traditional quantum information theory does embed faithfully into . If we just drop this constraint then the language construct 9 with suitable higher coherences added speaks about a generalization of (finite-dimensional) Hilbert spaces to higher “\((\infty,1)\)-Hilbert spaces” (of finite type), such as modeled by (unbounded) \(\mathbb{R}\)-chain complexes equipped with self-duality under the tensor product of chain complexes (cf. [35]). Progenitors of such \((\infty,1)\)-Hilbert spaces appear in [20], where spaces of \(\mathfrak{su}(2)\)-anyonic quantum ground states arise as the homology of chain complexes for twisted/equivariant cohomology of configuration spaces of points. Generally, topological quantum effects needed for topological quantum computing are described by (linear) higher homotopy theory (“higher structures”) of the kind expressed by the language.

On a more elemenary note, it may be worth highlighting that the semantics of 9 in Real modules may readily be internalized into the formal language itself:

The internal complex numbers. Using the negative unit scalar 17 we may define a commutative monoid internal to \(\mathrm{Qu}\mathrm{Type}\) \[\label{InternalComplexNumbers} \mathbb{C} \;\; \mathrel{\vcenter{:}}= \;\; \Big( \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \!\oplus\! \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Im} ,\; (-) \cdot (-) ,\; 1 \Big) \;\; \in \;\; \mathrm{CMon}\big( \mathrm{Qu}\mathrm{Type} ,\, \otimes ,\, \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} ,\, \sigma \big) \,,\tag{20}\] (the subscripts just to keep track of the two copies of what in both cases is the tensor unit of \(\mathrm{Qu}\mathrm{Type}\)) with multiplication and unit given by the time-honored formulas for the complex numbers, sraightforwardly internalized into the monoidal category of module spectra: \[\label{InternalComplexMultiplication} \begin{tikzcd}[ row sep=-1pt ] \mathbb{C} \otimes \mathbb{C} \ar[ rr, "{ \cdot }" ] && \mathbb{C} \\[+6pt] \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \!\otimes\! \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \,\oplus\, \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Im} \!\otimes\! \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Im} \ar[ rr, "{ \mathrm{id} \;\oplus\; -\mathrm{id} }"{description} ] && \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \\ \oplus && \oplus \\ \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \!\otimes\! \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Im} \,\oplus\, \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Im} \!\otimes\! \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \ar[ rr, "{ \mathrm{id} \;\oplus\; \mathrm{id} }"{description} ] && \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Im} \mathrlap{\,,} \end{tikzcd}\begin{tikzcd}[row sep=-1pt] \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \ar[ rr, "{ 1 }" ] && \mathbb{C} \\[+6pt] \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}} \ar[ rr, "{ \mathrm{id} }" ] && \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \\ && \otimes \\ && \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Im} \mathrlap{\,.} \end{tikzcd}\tag{21}\] Similarly, internal complex conjugation is the monoid endomorphism on \(\mathbb{C}\) given by \[\label{InternalComplexConjugation} \begin{tikzcd}[row sep=0pt] \mathbb{C} \ar[ rr, "{ \overline{(-)} }" ] && \mathbb{C} \\[7pt] \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_\Re \ar[ rr, "{ \mathrm{id} }" ] && \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_{\Re} \\ \oplus && \oplus \\ \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_\Im \ar[ rr, "{ -\mathrm{id} }" ] && \adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}_\Im \mathrlap{\,,} \end{tikzcd}\tag{22}\] which is an involutive equivalence, by 15 .

In the model of paramaterized \(H\mathbb{R}\)-module spectra by local systems of \(\mathbb{R}\)-chain complex, this construction produces, up to equivalence, the dg-\(\mathbb{R}\)-algebra which is concentrated on the \(\mathbb{R}\)-algebra of complex numbers in degree 0.

The same construction works, of course, in the \(\infty\)-topos of \(R\)-module spectra for any \(E_\infty\)-ring \(R\). Over the sphere spectrum, \(R \,\equiv\, \mathbb{S}\), it produces what might be called the “homotopy complex integers”. The specification to \(R \,\equiv\, H\mathbb{R}\) is eventually necessary for actual application to quantum physics: Formal definition even of something as elementary as a Hadamard quantum gate requires that one can find a term \(\sqrt{2}\) of type \(\adjustbox{scale=1.1,raise=-.4pt}{\mathbb{1}}\).

Real homotopy types. Left base change to the slice over \(\mathbf{B}{\mathbb{Z}_{2}}\) induces a monad \(\scalebox{1.06}{\lozenge}_{{\mathbb{Z}_{2}}}\) whose modal types are equivalent to types in the slice \[\begin{tikzcd}[ row sep=10pt ] \ast \ar[ rr, "{ \exists ! }" ] && \mathbf{B}{\mathbb{Z}_{2}} \\ \mathrm{Type} \ar[out=30+180, in=-30+180, looseness=3.2, shorten=-2pt, shift right=2pt, "\scalebox{1.3}{{ \mathclap{ \scalebox{1.06}{\lozenge}_{{\mathbb{Z}_{2}}} }}}"{pos=.5, description} ] \ar[ rr, shift left=14pt, "{ \coprod_{{\mathbb{Z}_{2}}} }"{description} ] \ar[ from=rr, ] \ar[ rr, shift right=14pt, lightgray, "{ \prod_{{\mathbb{Z}_{2}}} }"{description} ] \ar[ rr, phantom, shift left=5pt, "{ \scalebox{.7}{\bot} }" ] \ar[ rr, phantom, shift right=5pt, "{ \scalebox{.7}{\bot} }"{lightgray} ] && \mathrm{Type}_{/\mathbf{B}{\mathbb{Z}_{2}}} \mathrlap{\,,} \end{tikzcd}\mathrm{Type}_{\scalebox{1.06}{\lozenge}_{{\mathbb{Z}_{2}}}} \;\simeq\; \mathrm{Type}_{/\mathbf{B}{\mathbb{Z}_{2}}} \,.\] This slice is still stable and distributive monoidal.

The Real internal numbers. Equipped with the involution 22 , the internal complex numbers 20 become a monoid internal to \(\scalebox{1.06}{\lozenge}_{\mathbb{Z}_{2}}\)-modal type, as in the previous discussion: \[\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \;\; \equiv \;\; \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \begin{tikzcd} \mathbb{C} \sqcup \mathbb{C} \ar[ <->, bend right=25pt, shift right=10pt, start anchor={[xshift=-10pt]}, end anchor={[xshift=+10pt]}, "{ \overline{(-)} }"{description} ] \end{tikzcd} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \begin{tikzcd} \ast \sqcup \ast \ar[ <->, bend right=20pt, shift right=8pt, start anchor={[xshift=-9pt]}, end anchor={[xshift=+9pt]} ] \end{tikzcd} } \end{array} \right] \;\; \in \;\; \mathrm{Mon}\big( \mathrm{Type}_{\scalebox{1.06}{\lozenge}_{{\mathbb{Z}_{2}}}} \big) \,.\] We may think of this equivalently as monad structure (the \(\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}\)-Writer monad) on the endofunctor that tensors with the underlying \(\scalebox{1.06}{\lozenge}_{\mathbb{Z}_{2}}\)-modal type \[\begin{tikzcd}[sep=0pt] \mathrm{Qu}\mathrm{Type}_{\scalebox{1.06}{\lozenge}_{\mathbb{Z}_{2}}} \ar[ rr, "{}" ] && \mathrm{Qu}\mathrm{Type}_{\scalebox{1.06}{\lozenge}_{\mathbb{Z}_{2}}} \\ \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V_\bullet } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { {X}\!\sslash\!{{\mathbb{Z}_{2}}} } \end{array} \right] &\mapsto& \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \otimes_{{}_{\mathbf{B}{\mathbb{Z}_{2}}}} \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V_\bullet } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { {X}\!\sslash\!{{\mathbb{Z}_{2}}} } \end{array} \right] \end{tikzcd}\]

The Real quantum types. This way, the real quantum types are the modal types \[\mathrm{Qu}\mathrm{Type}_{ \scalebox{1.06}{\lozenge}_{\mathbb{Z}_{2}}, \scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}} }\]

1 Quantization for Real↩︎

Beyond purely linear/quantum types, there is classical/quantum interaction (through quantum measurement and state preparation) which is described by linear types dependent on classical types.

It is in this parameterized context that Real modules become strictly more general than \(\mathbb{R}\)-vector spaces, since Real modules may not just depent on plain sets, but generally on Real sets:

The Real sets. We write \[\label{CategoryOfRealSets} {\mathbb{Z}_{2}} \mathrm{Set} \;\;\; \equiv \;\;\; {{\mathbb{Z}_{2}}}\,\mathrm{Act} ( \mathrm{Set} ) \;\; \simeq \;\; \mathrm{Func}\big( \mathbf{B}{\mathbb{Z}_{2}} ,\, \mathrm{Set} \big)\tag{23}\] for the category of sets equipped with \({\mathbb{Z}_{2}}\)-actions (often “\({\mathbb{Z}_{2}}\)-sets”, the Real sets among Atiyah’s Real spaces [22]).

There are two distinct embeddings of plain sets into Real sets:

  • as sets with trivial action \[\begin{tikzcd}[sep=0pt] \mathrm{Set} \ar[ rr, hook, "{ }" ] && {\mathbb{Z}_{2}} \mathrm{Set} \\ W &\mapsto& \scalebox{.83}{ (\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \ast) \times W } \end{tikzcd}\] This inclusion is fully faithful and reflects the “discrete sets” as seen internally in the topos of Real sets.

  • as sets with free action \[\label{FormingFreeZTwoActionsOnSets} \begin{tikzcd}[sep=0pt] \mathrm{Set} \ar[ rr ] && {\mathbb{Z}_{2}} \mathrm{Set} \\ W &\mapsto& ({\mathbb{Z}_{2}}\!\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\; {\mathbb{Z}_{2}})\times W \end{tikzcd}\tag{24}\] This inclusion is only faithful (though not far from full: the inclusion of hom-sets is “of index two”) but is the left adjoint of a monadic functor:

\[\label{BaseChangeToAndFromBZTwo} \begin{tikzcd}[ row sep=20pt, column sep=55pt ] \ast \ar[ rr, "{ \vdash \, \mathrm{pt} }"{description} ] && \mathbf{B}{\mathbb{Z}_{2}} \ar[rr] && \ast \\ \mathrm{Set} \ar[out=180+30, in=180-30, looseness=3.5, shift right=4pt, "\scalebox{1}{{\mathclap{ {(-)}_{\!\mathrm{sm}} }}}"{pos=.5, description}, ] \ar[ rr, shift left=16pt, "{ {\mathbb{Z}_{2}} \! \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, ( {\mathbb{Z}_{2}} \times - ) }"{description} ] \ar[ from=rr, "{ U }"{description} ] \ar[ rr, gray, shift right=16pt, "{ \color{gray} {\mathbb{Z}_{2}} \! \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathrm{Hom}( {\mathbb{Z}_{2}} ,\, - ) }"{description} ] \ar[ rr, phantom, shift left=7pt, "{ \scalebox{.7}{\bot} }" ] \ar[ rr, phantom, shift right=8pt, "{ \scalebox{.7}{\color{gray}\bot} }" ] && {\mathbb{Z}_{2}} \mathrm{Set} \ar[ rr, gray, shift left=16pt, "{ \color{gray} (-)/{\mathbb{Z}_{2}} }"{description} ] \ar[ from=rr, hook', "{ ({\mathbb{Z}_{2}}\!\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \ast) \times (-) }"{description} ] \ar[ rr, shift right=16pt, "{ (-)^{{\mathbb{Z}_{2}}} }"{description} ] \ar[ rr, phantom, shift left=8pt, "{ \scalebox{.7}{\color{gray}\bot} }" ] \ar[ rr, phantom, shift right=8pt, "{ \scalebox{.7}{\bot} }" ] && \mathrm{Set} \end{tikzcd}\tag{25}\]

The category of Real sets 23 is equivalently the category of the corresponding action groupoids \({X}\!\sslash\!{{\mathbb{Z}_{2}}}\) fibered over \(\mathbf{B}{\mathbb{Z}_{2}}\,\equiv\, {\ast}\!\sslash\!{{\mathbb{Z}_{2}}}\): \[\begin{tikzcd}[sep=0pt] {\mathbb{Z}_{2}} \mathrm{Set} \ar[ rr, hook ] && \mathrm{Grpd}_{/\mathbf{B}{\mathbb{Z}_{2}}} \\ {\mathbb{Z}_{2}}\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, X &\mapsto& \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { {X}\!\sslash\!{{\mathbb{Z}_{2}}} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \mathbf{B}{\mathbb{Z}_{2}} } \end{array} \right] \end{tikzcd}\] This brings out the fact that we may think of Real sets as discrete \({\mathbb{Z}_{2}}\)-orbifolds (in fact: orientifolds, when we consider Real bundles over them): The sets in the image of the free functor correspond to the “smooth” (namely: non-singular) spaces among these orbifolds, which gives the name to the monad \({(-)}_{\!\mathrm{sm}}\) in 24 .

Hence Real sets are disjoint unions of smooth points \({\ast}_{\!\mathrm{sm}}\) and singular points \({\ast}\!\sslash\!{{\mathbb{Z}_{2}}}\).

The Real bundles over Real sets. The orbi/orienti-fold perspective 24 makes it manifest that the system of categories of \(\mathbb{R}\)-vector bundles over underlying sets equipped with \(\mathbb{R}\)-vector bundle involutions covering those on the base is an ambidextrous pseudofunctor on Real Sets (for background on this and the following statements see [2]): \[\begin{tikzcd}[ row sep=0pt ] {\mathbb{Z}_{2}} \mathrm{Set} \ar[ rr ] &[-35pt]&[+35pt] \mathrm{Cat}_{\mathrm{adj}} \\ {X}\!\sslash\!{{\mathbb{Z}_{2}}} \ar[ rr, phantom, "{ \mapsto }" ] \ar[dr] \ar[ dd, "{ f }"{swap} ] && \mathrm{Mod}_{\scalebox{.7}{ \mathbb{R}}}^{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{X} }} \;\equiv\; \mathrm{Func}\big( {X}\!\sslash\!{{\mathbb{Z}_{2}}} ,\, \mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}} \big) \ar[ dd, shift right=65pt, "{ f_! }"{description} ] \ar[ dd, shift right=58pt, phantom, "{ \scalebox{.7}{\dashv} }" ] \ar[ from=dd, shift left=50pt, "{ f^\ast }"{description} ] \ar[ dd, shift right=65-70pt, "{ \mathrm{Lan}_f }"{swap} ] \ar[ dd, shift right=58-70pt, phantom, "{ \scalebox{.7}{\dashv} }" ] \ar[ from=dd, shift left=50-70pt, "{ \mathrm{Func}(f,\mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}}) }"{swap} ] \\[10pt] & \mathbf{B}{\mathbb{Z}_{2}} \\[10pt] {Y}\!\sslash\!{{\mathbb{Z}_{2}}} \ar[ rr, phantom, "{ \mapsto }" ] \ar[ ur ] && \mathrm{Mod}_{\scalebox{.7}{ \mathbb{R}}}^{\scalebox{.7}{ {\mathbb{Z}_{2}}\!\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}Y }} \;\equiv\; \mathrm{Func}\big( {Y}\!\sslash\!{{\mathbb{Z}_{2}}} ,\, \mathrm{Mod}_{\scalebox{.7}{\mathbb{R}}} \big) \,. \end{tikzcd}\] The resulting Grothendieck construction is the category of such bundles over varying Real base sets with vector bundle morphisms covering the base maps \[\underset{ \scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{X} } }{\int} \mathrm{Mod}_{\scalebox{.7}{ \mathbb{R}}}^{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{X} }}=\left\{ \begin{tikzcd} [ row sep=1pt, column sep=2pt ] & \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V_\bullet } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { {X}\!\sslash\!{{\mathbb{Z}_{2}}} } \end{array} \right] \ar[ rrrrrr, shift left=13pt, "{ \phi_\bullet }" ] \ar[ rrrrrr, shift right=13pt, "{ f }" ] &[-10pt]&[-10pt]&&&&[-10pt] \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V'_\bullet } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { {X'}\!\sslash\!{{\mathbb{Z}_{2}}} } \end{array} \right] &[-10pt] \\ V_{x} \ar[ rrrrrr, "{ \phi_x }"{description} ] \ar[ <->, ddrr, "{ \sim }"{sloped} ] &&&&&& V'_{f(x)} \ar[ <->, ddrr, "{ \sim }"{sloped} ] & \\ \scalebox{.8}{x} \ar[ <->, ddrr, shorten >=-2pt, "{ \sim }"{sloped} ] &&&&&& \\ && V_{x'} \ar[ rrrrrr, "{ \phi_{x'} }"{description, pos=.6} ] &&&&&& V'_{f(x')} \\ && \scalebox{.8}{x'} \end{tikzcd} \right\} \,.\] This becomes a symmetric monoidal category under the “external” tensor product \(\otimes_{{}_\mathbb{R}}\) of bundles with tensor unit the \(\mathbb{R}\)-line regarded as a bundle over the point equipped with the trivial \({\mathbb{Z}_{2}}\)-action.

The Real numbers constitute a monoid in this monoidal category \[\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \;\; \equiv \;\; \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \mathbb{C} _{\scalebox{.6}{\overline{(-)}}} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { { \ast }\!\sslash\!{ {\mathbb{Z}_{2}}} } \end{array} \right] \;\in\; \mathrm{Mon} \left( \underset{ \scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{X}} }{\int} \mathrm{Mod}_{\scalebox{.7}{ \mathbb{R}}}^{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{X} }} ,\; \otimes_{{}_\mathbb{R}} ,\; \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \mathbb{R}_{\mathrm{id}} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { {\ast}\!\sslash\!{{\mathbb{Z}_{2}}} } \end{array} \right] \right)\] and its category of modules is equivalently Atiyah’s Real vector bundles [22] over Real sets. \[\label{CategoryOfRealBundlesOverRealSets} \mathrm{Mod}_{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}}^{\scalebox{.7}{ {\mathbb{Z}_{2}} \mathrm{Set} }} \;\;\; \equiv \;\;\; \mathrm{Mod}_{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}} \left( \underset{ \scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{X}} }{\int} \mathrm{Mod}_{\scalebox{.7}{ \mathbb{R}}}^{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{X} }} ,\; \otimes_{{}_\mathbb{R}} ,\; \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \mathbb{R}_{\mathrm{id}} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { {\ast}\!\sslash\!{{\mathbb{Z}_{2}}} } \end{array} \right] \right) \,.\tag{26}\] In particular, the Real modules over the point, from 2 , are indeed the \(\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}\)-modules over \({\ast}\!\sslash\!{{\mathbb{Z}_{2}}}\) in the general sense of 26 : \[\mathrm{Mod}_{\scalebox{.7}{\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}} \;\;\simeq\;\; \mathrm{Mod}_{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}}^{\scalebox{.7}{ {\ast}\!\sslash\!{{\mathbb{Z}_{2}}} }}\] because the \(\raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}\)-module structure implies the \(\mathbb{C}\)-anti-linearity of the involution: \[\begin{tikzcd}[ column sep=-7pt, row sep=small ] \mathbb{C} \ar[out=180-60, in=60, looseness=4.4, "\scalebox{1}{{\mathclap{ \overline{(-)} }}}"{pos=.41, description}, shift right=3pt ] &\otimes_{{}_\mathbb{R}}\!\!& V \ar[out=180-60, in=60, looseness=4.4, "\scalebox{1}{{\mathclap{ C }}}"{pos=.41, description}, shift right=3pt ] \ar[ rrr ] &[10pt] &[10pt] &[0pt] V \ar[out=180-60, in=60, looseness=4.4, "\scalebox{1}{{\mathclap{ C }}}"{pos=.41, description}, shift right=3pt ] \\[-9pt] z & \otimes \ar[ dd, phantom, "{\mapsto}"{rotate=-90} ] & v &&\mapsto& z \cdot v \ar[ d, phantom, "{\mapsto}"{rotate=-90} ] \\ && && & C(z \cdot v) \\[-10pt] \overline{c} &\otimes& C(v) &\mapsto& \overline{c} \cdot C(v) \ar[ ur, equals ] & \end{tikzcd}\]

Complex vector bundles among Real vector bundles. Notice that the canonical “embedding” of \(\mathbb{C}\)-vector bundles (over varying base sets) into Real vector bundles (over varying Real sets) \[\label{ComplexVectorBundlesAmongRealVectorBundles} \begin{array}{c} \begin{tikzcd}[ column sep=13pt ] \mathrm{Mod}_{\scalebox{.7}{ \mathbb{C}}}^{\scalebox{.7}{ \mathrm{Set} }} \ar[ rr ] && \mathrm{Mod}_{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}}^{\scalebox{.7}{ {\mathbb{Z}_{2}} \mathrm{Set} }} \end{tikzcd} \\ \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { X } \end{array} \right] \;\;\;\mapsto\;\;\; \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \begin{tikzcd} V \sqcup \overline{V} \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \begin{tikzcd} X \sqcup X \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \end{array} \right] \end{array}\tag{27}\] is (faithful but) not full, cf. 24 : The morphisms on the right contain both (fiberwise) \(\mathbb{C}\)-linear as well as \(\mathbb{C}\)-anti-linear maps, depending on whether the base maps they cover are in the image of 27 or compositions of these with the \({\mathbb{Z}_{2}}\)-action.

Instead, to get a full embedding one needs to consider, on the right, Real vector bundles equipped, internally, with fiberwise complex structure, namely with endomorphisms that fix the base and square to \(-1\) on the fibers. These act by multiplication with \(\mathrm{i}\) on some fibers and with \(- \mathrm{i}\) on their involution-mirrors, thus breaking the \({\mathbb{Z}_{2}}\)-symmetry. Specifically, the Real bundles which are images of \(\mathbb{C}\)-linear bundles 27 carry a canonical internal complex structure: \[\label{InternalComplexStructureOnComplexBundleSeenAsRealBundle} \begin{tikzcd} V \sqcup \overline{V} \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \ar[ rr, "{ + \mathrm{i} \;\sqcup\; - \mathrm{i} }" ] \ar[ d, ->>, shorten <=5pt ] && V \sqcup \overline{V} \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \ar[ d, ->>, shorten <=5pt ] \\ X \sqcup X \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \ar[ rr, equals ] && X \sqcup X \mathrlap{\,.} \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd}\tag{28}\]

Interestingly, the \(\mathbb{C}\)-line bundle over the point may be written as the Cartesian product of the smooth point with the Real numbers \[\label{ComplexLineAsSmoothPointTimesRealNumbers} {\ast}_{\!\mathrm{sm}} \times \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \;\;\; = \;\;\; \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \begin{tikzcd} 0 \sqcup 0 \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \begin{tikzcd} \ast \sqcup \ast \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \end{array} \right] \times \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}} \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}{\ast} } \end{array} \right] \;\;\; = \;\;\; \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \begin{tikzcd} \mathbb{C} \sqcup \overline{\mathbb{C}} \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \begin{tikzcd} \ast \sqcup \ast \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \end{array} \right]\tag{29}\]

Real modules reflected inside Real bundles. We may now observe that the canonical inclusion of Real modules into Real bundles is reflective, the reflector \(\raisebox{-0pt}{\scalebox{.95}{\rotatebox{30}{\triangle}}}\) given by forming the direct sum of fibers equipped with the induced involution, we indicate the corresponding hom-isomorphism on the right: \[\label{ReflectionOfRealModulesInRealBundles} \begin{array}{c} \begin{tikzcd} \underset{ \mathclap{ x \in X } }{\oplus} \; V_x \ar[out=56+90, in=-56+90, looseness=3, shorten=-3pt, "\scalebox{1}{{ V_x \leftrightarrow V_{\sigma(x)} }}"{pos=.5, description} ] \end{tikzcd}\mapsfrom\left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V_\bullet } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { { X }\!\sslash\!{ {\mathbb{Z}_{2}}} } \end{array} \right] \\ \begin{tikzcd} \mathrm{Mod}_{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}} \ar[ from=rr, ->>, shift right=7pt, "{ \raisebox{-0pt}{\scalebox{.95}{\rotatebox{30}{\triangle}}}}"{swap} ] \ar[ rr, phantom, "{ \scalebox{.7}{ \bot } }" ] \ar[ rr, shift right=7pt, hook ] && \mathrm{Mod}_{\scalebox{.7}{ \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C}}}^{\scalebox{.7}{ {\mathbb{Z}_{2}} \mathrm{Set} }} \end{tikzcd} \\ \begin{tikzcd} V \ar[out=40+90, in=-40+90, looseness=3.3, shorten=-3pt, "\scalebox{1}{{\mathclap{ C }}}"{pos=.5, description} ] \end{tikzcd}\mapsto\Bigg[\begin{tikzcd}[row sep=14pt] V \ar[out=40+90, in=-40+90, looseness=3.3, shorten=-3pt, "\scalebox{1}{{\mathclap{ C }}}"{pos=.5, description} ] \ar[ d, ->> ] \\ \ast \ar[out=40-90, in=-40-90, looseness=3.3, shorten=-3pt, "\scalebox{1}{{\mathclap{ {\mathbb{Z}_{2}} }}}"{pos=.5, description} ] \end{tikzcd}\Bigg] \end{array}\begin{tikzcd} [ row sep=1pt, column sep=2pt ] & \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V_\bullet } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { {X}\!\sslash\!{{\mathbb{Z}_{2}}} } \end{array} \right] \ar[ rrrrrr, shift left=13pt, "{ \phi_\bullet }" ] \ar[ rrrrrr, shift right=13pt, "{ \exists ! }" ] &[-25pt]&[-10pt]&&&&[-0pt] \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { V' } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \mathbf{B}{\mathbb{Z}_{2}}} \end{array} \right] &[-10pt] \\ V_{x} \ar[ rrrrrr, "{ \phi_x }"{description} ] \ar[ <->, ddrr, "{ \sim }"{sloped} ] &&&&&& V' \ar[ <->, ddrr, "{ \sim }"{sloped} ] & \\ \scalebox{.8}{x} \ar[ <->, ddrr, "{ \sim }", shorten >=-2pt ] &&&&&& \\ && V_{x'} \ar[ rrrrrr, "{ \phi_{x'} }"{description, pos=.6} ] &&&&&& V' \\ && \scalebox{.8}{x'} \end{tikzcd}\leftrightarrow\begin{tikzcd} \underset{ \mathclap{ x \in X } }{\oplus} \; V_x \ar[out=56+90, in=-56+90, looseness=3, shorten=-3pt, "\scalebox{1}{{ V_x \leftrightarrow V_{\sigma(x)} }}"{pos=.5, description} ] \ar[ rr, "{ \underset{ \mathclap{ x \in X } }{\oplus} \; \phi_x }" ] && V' \mathrlap{\,.} \ar[out=30+90, in=-30+90, looseness=3, shorten=-3pt, "{ \sim }" ] \end{tikzcd}\tag{30}\]

Notice that, by functoriality, this reflection sends complex structures on Real bundles, such as in 28 , to complex structures on Real modules, such as in 9 .

The Real quantization. In enhancement of [1], we now have a quantization (relative) monad \(\mathrm{Q}\) which produces not just linear spaces but Hermitian spaces, regarded as self-dual Real modules with isometric complex structure:

\[\label{RealQuantization} \mathrm{Q}{W}_{\!\mathrm{sm}} \;\;\; \equiv \;\;\; \raisebox{-0pt}{\scalebox{.95}{\rotatebox{30}{\triangle}}} \Big( {W}_{\!\mathrm{sm}} \times \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \Big)\tag{31}\]

For finite \(W\), the complex Real modules arising this way admit self-duality structure.

In particular the Real quantization of the non-singular point is the \(\mathbb{C}\)-line \[\mathrm{Q}({\ast}_{\!\mathrm{sm}}) \;\;\; \underset{ \mathclap{ \scalebox{.7}{ \color{gray} \eqref{RealQuantization} } } }{ \simeq } \;\;\; \raisebox{-0pt}{\scalebox{.95}{\rotatebox{30}{\triangle}}} \Big( {\ast}_{\!\mathrm{sm}} \times \raisebox{1.4pt}{\;\rotatebox[origin=c]{90}{\curvearrowright}}\, \mathbb{C} \Big) \;\;\; \underset{ \mathclap{ \scalebox{.7}{ \color{gray} \eqref{ComplexLineAsSmoothPointTimesRealNumbers} } } }{ \simeq } \;\;\; \raisebox{-0pt}{\scalebox{.95}{\rotatebox{30}{\triangle}}} \left[ \def\arraystretch{1}\def\arraycolsep{1pt} \begin{array}{c} { \begin{tikzcd} \mathbb{C} \sqcup \overline{\mathbb{C}} \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \\ \rotatebox[origin=c]{-90}{\twoheadrightarrow} \\ { \begin{tikzcd} \ast \sqcup \ast \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd} } \end{array} \right] \;\;\; \underset{ \mathclap{ \scalebox{.7}{ \color{gray} \eqref{ReflectionOfRealModulesInRealBundles} } } }{ \simeq } \;\;\; \begin{tikzcd} \mathbb{C} \oplus \overline{\mathbb{C}} \ar[ <->, shift right=5pt, bend right=23pt, start anchor={[xshift=-8pt]}, end anchor={[xshift=+7pt]} ] \end{tikzcd}\]

This carries an essentially unique inner product structure, up to a sign. We can fix the sign by demanding that \(\langle 1 \vert 1 \rangle = + 1\). That’s the positivity condition.

Remark. The above is the Real version of the quantization modality in [1]. Notice that the analogous construction with \(\mathbb{R}\)-bundles fails to provide complex spaces of quantum states. It is here that Real bundles are more than just an equivalent perspective on \(\mathbb{R}\)-bundles.


H. Sati and U. Schreiber, The Quantum Monadology, [https://arxiv.org/abs/2310.15735].
H. Sati and U. Schreiber, Entanglement of Sections: The pushout of entangled and parameterized quantum information, [https://arxiv.org/abs/2309.07245].
J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Math. Ann. 102(1930), 49–131, [https://doi.org/10.1007/BF01782338].
J. von Neumann, Mathematische Grundlagen der Quantenmechanik(1932), [https://link.springer.com/book/10.1007/978-3-642-96048-2]; , Princeton University Press (1955), .
K. Landsman, Foundations of quantum theory – From classical concepts to Operator algebras, Springer Open (2017), [https://link.springer.com/book/10.1007/978-3-319-51777-3].
N. Bourbaki, Topological Vector Spaces, Chapters 1–5, Masson (1981), Springer, Berlin (2003), .
P. Selinger, Autonomous categories in which \(A \simeq A^\ast\), talk at QPL 2012,.
P. Selinger, Dagger compact closed categories and completely positive maps, Electronic Notes Theor. Comp. Sci. 170(2007), 139-163, [https://doi.org/10.1016/j.entcs.2006.12.018].
C. Heunen and J. Vicary, Categories for Quantum Theory, Oxford University Press (2019), [https://global.oup.com/academic/product/categories-for-quantum-theory-9780198739616], [https://www.cs.ox.ac.uk/files/4551/cqm-notes.pdf].
S. Abramsky and B. Coecke, A categorical semantics of quantum protocols, Proceedings of the 19th IEEE conference on Logic in Computer Science (LiCS’04), IEEE Computer Science Press (2004), [https://arxiv.org/abs/quant-ph/0402130], [https://doi.org/10.1109/LICS.2004.1319636].
L. Stehouwer and J. Steinebrunner, Dagger categories via anti-involutions and positivity, [https://arxiv.org/abs/2304.02928].
M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press (2000), [https://doi.org/10.1017/CBO9780511976667].
P. Fu, K. Kishida, and P. Selinger, Linear Dependent Type Theory for Quantum Programming Languages, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (2020), 440–453, [https://arxiv.org/abs/2004.13472].
M. Riley, A Linear Dependent Type Theory with Identity Types(2023),.
F. Rios and P. Selinger, A Categorical Model for a Quantum Circuit Description Language, EPTCS 266(2018), 164-178, [https://doi.org/10.4204/EPTCS.266.11], [https://arxiv.org/abs/1706.02630].
M. Riley, E. Finster, and D. R. Licata Synthetic Spectra via a Monadic and Comonadic Modality(2021), [https://arxiv.org/abs/2102.04099].
D. J. Myers and M. Riley, Sesqui-Linear Homotopy Type Theory, in preparation.
H. Sati and U. Schreiber, Anyonic defect branes in TED-K-theory, Rev. Math. Phys 35(2023) 2350009, , [https://arxiv.org/abs/2203.11838].
H. Sati and U. Schreiber, Anyonic topological order in TED K-theory, Rev. Math. Phys. 35 03 (2023) 2350001, [https://doi.org/10.1142/S0129055X23500010], [https://arxiv.org/abs/2206.13563].
D. J. Myers, H. Sati, and U. Schreiber, Topological Quantum Gates in Homotopy Type Theory, .
H. Sati and U. Schreiber, Equivariant Principal \(\infty\)-Bundles, [https://arxiv.org/abs/2112.13654].
M. Atiyah, K-theory and Reality, Quarterly J. Math. 17(1966), 367-386, [https://doi.org/10.1093/qmath/17.1.367].
S. Eilenberg and G. M. Kelly, Closed Categories, in: Proceedings of the Conference on Categorical Algebra – La Jolla 1965, Springer, Berlin (1966), 421-562, [https://doi.org/10.1007/978-3-642-99902-4].
D. Huybrechts, Complex geometry: An introduction, Universitext, Springer, Berlin (2004), .
R. Berndt, An introduction to symplectic geometry, Graduate Studies in Mathematics 26, American Mathematical Society (2001), [https://bookstore.ams.org/gsm-26].
H. Bass (notes by A. Roy), Lectures on Topics in Algebraic K-Theory, Tata Institute of Fundamental Research (1965), [https://ncatlab.org/nlab/files/Bass-HyperbolicFunctor.pdf].
M. Karoubi, Périodicité de la K-théorie hermitienne, in: Algebraic K-Theory III – Hermitian K-Theory and Geometric Applications, Lecture Notes in Mathematics 343(1973), 301-411, Springer, Berlin, [https://doi.org/10.1007/BFb0061366].
A. Bak, Grothendieck Groups of Modules and Forms Over Commutative Orders, Amer. J. Math. 99 1 (1977), 107-120, [https://www.jstor.org/stable/2374010], [https://doi.org/10.2307/2374010].
M. Karoubi, Le théorème de périodicité en K-théorie hermitienne, in Quanta of Maths, Clay Mathematics Proceedings 11, AMS and Clay Math Institute Publications (2010), 257-282, [https://arxiv.org/abs/0810.4707].
M. C. Crabb, \(\mathbb{Z}/2\)-Homotopy Theory, Lond. Math. Soc. Lecture Notes 44 Cambridge University Press (1980), [https://archive.org/details/zz2homotopytheor0000crab].
A. Dold and D. Puppe, Duality, Trace and Transfer, Proc. Steklov Inst. Math. 154(1984), 85–103,.
J. Lurie, Higher Algebra(2017), [https://www.math.ias.edu/ lurie/papers/HA.pdf].
M. Ando, A. Blumberg, D. Gepner, M. Hopkins, and C. Rezk, An \(\infty\)-categorical approach to \(R\)-line bundles, \(R\)-module Thom spectra, and twisted \(R\)-homology, J. Topology 7(2014) 869893, [https://doi.org/10.1112/jtopol/jtt035], [https://arxiv.org/abs/1403.4325].
D. Fiorenza, H. Sati, and U. Schreiber: The Character map in Nonabelian Cohomology: Twisted, Differential and Generalized, World Scientific, Singapore (2023), [https://doi.org/10.1142/13422 ], [https://arxiv.org/abs/2009.11909], .
J. Lurie, On the Classification of Topological Field Theories, Current Developments in Mathematics 2008(2009) 129-280 [https://arxiv.org/abs/0905.0465][https://dx.doi.org/10.4310/CDM.2008.v2008.n1.a3].

  1. For the purpose of this article, “Hermitian form”, “metric”, and “inner product” all imply the non-degeneracy and (conjugate-)symmetry of the pairing but not necessarily its signature.↩︎

  2. That further structure may and often is taken to be that of a dagger-category ([8], cf. [9], which recovers inner products according to [10], see e.g. [9] for general review and [11] for more recent developments). Just to highlight that dagger-structure serves to parameterize the issue more than it illuminates it: Besides the usual dagger structure for Hermitian inner products, \(\mathrm{Mod}_{\scalebox{.7}{\mathbb{C}}}\) also carries a dagger-structure encoding bilinear inner products. Dagger-theory by itself does not select one over the other for the purpose of quantum theory.↩︎

  3. In symplectic geometry, the data \(\big(V, J, \mathrm{i} g(J(-),-)\big)\) in 5 is called a Kähler vector space (e.g. [25]) with \(g\) its Kähler metric and \(g\big(J(-),-\big)\) the corresponding symplectic form.↩︎

  4. We will notationally suppress the “\(\infty\)-”-prefix in the following. All constructions are understood to be homotopy-theoretic. Similarly, all diagrams are filled by 2-morphisms, even when these are not explicitly indicated.↩︎

  5. In terms of module spectra this may be readily understood from the fact that the stable homotopy groups of the suspensions of a spectrum relate to those of its underlying homotopy type by \(\pi_k\big( \Omega^\infty \Sigma^n V \big) \, = \, \pi_{n-k}\big( V \big) \,.\) In view of this, the heart condition 18 says equivalently that the \(\mathbb{Z}\)-graded stable homotopy groups \(\pi_\bullet(V)\) are concentrated in degree 0.↩︎