Homotopy Type Theory HilbR > history (Rev #2)

Idea

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

(Todo: address size issues with regards to universes, as well as the non-constructive nature of the proof…)

Assuming propositional excluded middle in the type theory, Hilb Hilb_\mathbb{R} is a 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).

References

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

Revision on February 14, 2022 at 23:49:16 by Anonymous?. See the history of this page for a list of all contributions to it.