Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
expanded the section Idea – In brief at Bohr topos just a little bit, in order to amplify the relation to Jordan algebras better (which previously was a bit hidden in entry).
Didn’t mean to give you extra work with my question on G+, Urs!
No, that’s good. Your comment showed that something I though had been made obvious in fact wasn’t. So I went back to the entry and noticed that it didn’t say this well. So I tried to improved it.
I gave the Idea-section at Bohr topos a more informal lead-in paragraph before the first subsection of the Idea section starts.
I came back to thinking about Bohr toposes, now in the context of homotopical algebraic quantum field theory.
Where an ordinary Bohr topos is a topos internal to which we find a locale such that ordinary probability distributions on it are, externally, quantum states, so a higher Bohr topos should probably contain internally a 1-localic topos, hence just a topos, thought of as a classifying topos of a localic groupoid internal to the to the Bohr topos, where the morphisms in that localic groupoid would be the gauge transformations.
The ambient Bohr topos itself is, in the ordinary case, the presheaves on the category of “classical contexts”, namely of types of things that may be measured simultaneously without quantum uncertainty.
A topos internal to that is equivalently just a presheaf of toposes on that category of classical contexts, isn’t it?
This made me think the whole Bohr topos idea is maybe better formulated in the language of dependent type theory/hyperdoctrines. What’s really going on is a 2-layered system of dependent types:
each spacetime region is a context (of things that may be measured in this region)
for each of these contexts, there is a poset of classical context (of those of these things that may be measured simultaneously)
for each of those, finally, there is a topos whose lattice of subterminal objects is the propositions about these measurements.
So it’s something like a poset of spacetime regions, and fibered over this a category whose fibers are posets of classical contexts, and fibered over these in turn a category whose fibers are toposes whose internal logic is that reasoning about the possible measurements in these classical contexts over these spacetime regions.
How can one speak of being “measured simultaneously” in a spacetime region? Do you mean the observables commute? Does this need the kind of thing Joost Nuiten discusses about ’strong locality’ (p. 19 of his 2011)?
Interesting! Multi-layer dependent type systems seem to be popping up all over the place these days. Cohesive type theory has crisp/cohesive contexts, simplicial and cubical type theory have a separate context of cubes/simplices and their faces, etc.
Re #6, is that what the discussion of the Cauchy problem contributes, that you have a time slice with which to define simultaneity?
How can one speak of being “measured simultaneously” in a spacetime region?
I used “simultaneous” not to refer to the time inside the spacetime, but to us discussing it. But in a sensible local net of observables for an actual quantum field theory, the spacetimes on which we evaluate are globally hyperbolic, meaning that they have a Cauchy surface, and the algebra of observables assigned to the spacetime is that to this spatial slice (or any one of them, up to isomorphism).
Re #6, is that what the discussion of the Cauchy problem contributes, that you have a time slice with which to define simultaneity?
Yes!
Urs, thanks. This is a natural idea. Of course, the two levels only show up once we go to AQFT. The use of DTT in topos theory is well-understood, but sometimes a bit hidden in the presentation.
Would you like to add something to the page?
BTW another place where these multi-layers show up recently is in our guarded cubical type theory. We are currently working on a version which brings this out even more clearly.
brushed up the first few lead-in sentences, cross-linking more with quantum probability.
added pointer to:
added pointer to:
1 to 14 of 14