Homotopy Type Theory HilbR > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Idea

< Hilb

Hilb 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 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)

  • an identity t:f =ft:f^\dagger = f for any f:hom(Ι,Ι)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:HIf: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)

Revision on June 7, 2022 at 00:01:56 by Anonymous?. See the history of this page for a list of all contributions to it.