nLab Hilb


Functional analysis

Operator algebra

algebraic quantum field theory (perturbative, on curved spacetimes, homotopical)



field theory:

Lagrangian field theory


quantum mechanical system, quantum probability

free field quantization

gauge theories

interacting field quantization



States and observables

Operator algebra

Local QFT

Perturbative QFT



A category whose objects are Hilbert spaces is typically denoted HilbHilb or similar.

There are different choices of morphisms in use, such as all linear maps or just the short linear maps (linear maps of norm at most 11).

One may regard HilbHilb as a dagger category with morphisms the bounded linear maps between them and the dagger operation assigning adjoint operators. The full subcategory FinHilbFin Hilb of finite-dimensional Hilbert spaces becomes a dagger compact category.

Note that either way, the core (of isomorphisms in the first case, or of unitary isomorphisms in the other case) is the same groupoid, whose morphisms are all invertible linear maps of norm exactly 11.

In any case, the forgetful functor from HilbHilb to Vect is faithful, confirming the intuition that a Hilbert space is a vector space equipped with extra structure. HilbHilb is also a full subcategory of Ban, the category of Banach spaces.

Explicit definition

Assuming excluded middle, Hilb Hilb_\mathbb{R} is a concrete dagger category with

  • a tensor product \otimes and tensor unit Ι\Iota, such that (Hilb ,,Ι)(Hilb_\mathbb{R},\otimes,\Iota) is a symmetric monoidal dagger category and Ι\Iota is a simple object and a monoidal separator,

  • a biproduct \oplus and zero object 00 such that (Hilb ,,0)(Hilb_\mathbb{R},\oplus,0) is a semiadditive dagger category

  • a dagger equaliser? eqeq such that (Hilb ,,0,eq)(Hilb_\mathbb{R},\oplus,0,eq) is a finitely complete dagger category?

  • a directed colimit underrightarrowlimF\underrightarrow{lim} F for any inductive system FF in the wide sub-dagger category of objects and dagger monomorphisms.

  • a morphism g:BCg:B \to C for any dagger monomorphism f:ABf:A \to B such that g=eq(f,0 B0 A )g = eq(f,0_B \circ 0_A^\dagger)

However, without excluded middle, this definition fails to result in the category of Hilbert spaces over the real or complex numbers. That a dagger monomorphism f:HIf:H \to I is either zero or invertible (in a symmetric monoidal dagger category where Ι\Iota is a simple monoidal separator) implies excluded middle, and Solèr’s theorem? also implies excluded middle. It is currently unknown what modifications are needed to the axioms and to Solèr’s theorem to result in a definition valid without propositional excluded middle in the type theory. It is also unknown what type of real or complex numbers would be derived from the modified axioms and modified Soler’s theorem in constructive mathematics.


A pedagogical description of the monoidal category structure on HilbHilb with an emphasis on their role in quantum mechanics and their relation to nCob:

An axiomatic characterization of the dagger-category of Hilbert spaces, with linear maps between them:

category: category

Last revised on October 25, 2022 at 10:40:47. See the history of this page for a list of all contributions to it.