What are kets?
Yuri Gurevich, Andreas Blass
TL;DR
The note analyzes Dirac bra-ket notation in inner-product spaces over $\mathbb{C}$, clarifying whether kets should be treated as vectors or as functions and how a functional view interacts with the usual vector interpretation. It introduces a Tentative Convention that marks each ket as either a vector ket or a function ket and formalizes Dirac terms as alternating sequences of bra and ket characters with parseable structure. A semantic map $\text{Val}(s)$ is defined inductively with typing rules (E1–E4) and an associative product $*$ on Dirac terms, yielding consistent reductions to vectors, scalars, linear functionals, or vector/scalar-valued functions. The Resolution section discusses robustness across interpretations, proposing natural conventions that recover the familiar scalar inner product and outer products as composition or scalar multiples, and showing these choices yield context-dependent, yet coherent, meanings.
Abstract
According to Dirac's bra-ket notation, in an inner-product space, the inner product $\langle x\,|\,y\rangle$ of vectors $x,y$ can be viewed as an application of the bra $\langle x|$ to the ket $|y\rangle$. Here $\langle x|$ is the linear functional $|y\rangle \mapsto \langle x\,|\,y\rangle$ and $|y\rangle$ is the vector $y$. But often -- though not always -- there are advantages in seeing $|y\rangle$ as the function $a \mapsto a\cdot y$ where $a$ ranges over the scalars. For example, the outer product $|y\rangle\langle x|$ becomes simply the composition $|y\rangle \circ \langle x|$. It would be most convenient to view kets sometimes as vectors and sometimes as functions, depending on the context. This turns out to be possible. While the bra-ket notation arose in quantum mechanics, this note presupposes no familiarity with quantum mechanics.