Schreiber Quantum and Reality

A brief note that we are finalizing:

---

• Hisham Sati$\;\;$and$\;\;$ Urs Schreiber:

  
  

  Quantum and Reality

  
  

  download:

  • arXiv:2311.11035

  • pdf

Abstract. 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-Quipper or, following our recent observations [Mon, EoS]: Linear Homotopy Type Theory (LHoTT). 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 LHoTT, 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 to encode (and verify) unitarity of quantum gates and of quantum channels in quantum languages embedded into LHoTT, as described in [Mon].

---

This is part of the CQTS-project:

• Quantum Certification via Linear Homotopy Types