Homotopy Type Theory HilbR > history (Rev #4)

Idea

$Hilb_\mathbb{R}$ is the category of Hilbert spaces over the real numbers, with morphisms the linear maps between Hilbert spaces over the real numbers.

Definition

Assuming propositional excluded middle in the type theory, $Hilb_\mathbb{R}$ is a concrete dagger category with

• a tensor product $\otimes$ and tensor unit $\Iota$, such that $(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 $0$ such that $(Hilb_\mathbb{R},\oplus,0)$ is a semiadditive dagger category

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

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

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

• an identity $t:f^\dagger = f$ for any $f:hom(\Iota,\Iota)$.

However, without propositional excluded middle in the type theory, this definition fails to result in the category of Hilbert spaces over the real numbers. That a dagger monomorphism $f:H \to I$ is either zero or invertible (in a symmetric monoidal dagger category where $\Iota$ is a simple monoidal separator) implies propositional excluded middle, and Solèr’s theorem? also implies propositional 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 numbers would be derived from the modified axioms and modified Soler’s theorem in predicative constructive mathematics.

References

• Chris Heunen, Andre Kornell. Axioms for the category of Hilbert spaces (arXiv:2109.07418)