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.
Right, elsewhere (at order-theoretic structure in quantum mechanics) I had emphasized the observation that the foundational theorems in quantum mechanics taken all together show that the idea that quantum observables form a Bohr topos – the glorified incarnation of the Jordan algebra of observables – is, essentially not a speculation but a derivable fact.
Now in the discussion of “quantization via linear homotopy-type theory” I have been adopting alltogether the “dual” perspective (in the sense that Bohr toposophy is Heisenberg picture where quantum logic as linear type theory is Schrödinger picture).
I don’t know yet how these two “pcictures” eventually want to merge to a single whole.
We had talked about this issue once before, when we were discussing “coordination” (I am providing links just for completeness for eventual bystanders). There I had speculated that the issue is the following:
suppose you manage to form the full extended quantization of 3d CS in $tmf Mod_4$. Then it ends up producing for you statements such as “the space of states on this manifold here is this tmf-$k$-module”. This raises a clear coordination issue: what does that mean physically?
We know by inspection how to do this coordination in some cases (e.g. an element of a $tmf$-1-module may be regarded as a Witten genus, hence as a partition function of a string). But we (well, me) don’t know how to “coordinate” systematically and generally.
Maybe Bohr toposophy is telling us that we should figure out to assign some kind of topos to any $E$-$k$-module such that the internal logic of this topos is the logic of statements about the universe of quantum states that make up this $E$-$k$-module.
But this is just a vague hunch. I have no idea at the moment about how to make this more concrete.
Mellies makes a big deal about the factorization of ! in linear logic in his Categorical Semantics of Linear Logic, e.g.,
One lesson of categorical semantics is that the exponential modality of linear logic should be described as an adjunction, rather than as a comonad. The observation is not simply technical: it has also a deep eﬀect upon the way we understand logic in the wider sense…This reﬁned decomposition requires to think diﬀerently about proofs, and to accept the idea that
logic is polychrome, not monochrome
this meaning that several universes of discourse (in this case, the categories L and M) generally coexist in logic, and that the purpose of a proof is precisely to intertwine these various universes by applying back and forth modalities (in this case, the functors L and M). In this account of logic, each universe of discourse implements its own body of internal laws. Typically, in the case of linear logic, the category M is cartesian in order to interpret the structural rules (weakening and contraction) while the category L is symmetric monoidal closed, or ∗-autonomous, in order to interpret the logical rules.
In view of #56
$! Z = \Sigma_+^\infty \Omega^\infty Z : \mathbf{H} \to Mod(\ast),$could we have a similarly florid description of what’s going on? Does something like that distinction between structural and logical rules persist?
First of all it was Mike who emphasized that once we talk about dependent linear type theory then this adjunction arises canonically. In dependent linear type theory there are already two “universes of discourse”: the intuitionistic logic of the base types and the linear logic of the linear types parameterized over them. The adjunction that gives the exponential modality is just one small aspect of this more general “interplay of two universes”.
Then of course in the application to cohomological quantization we find very naturally familar names for these “universes of discourse”: that of the cartesian base category is the discourse of pre-quantum (“classical”) geometry/physics, whereas the other one is that of quantum geometry/physics. The fact that one is parameterized over the other is really the content of geometric quantization.
So we could still say something of Mellies’ structural/logical split persists - weakening and contraction available in the classical world, logical rules as linear operators in the quantum world?
Hmm, or does the shift to dependent type theory muddle things up? I guess there’s type formation and term intro/elim/computation going on in the base and in the linear fibres.
Is
what became of that forthcoming paper, Gepner, D. and J. Kock, Polynomial functors over inﬁnity categories, mentioned in #76?
I guess at the time I was wondering if it might be useful for Quantization via Linear homotopy types. Was def 3.20 the first appearance of the $\infty$-version of polynomial functor?
I hadn’t seen this reference. Best to add a pointer to it to a relevant entry!
I’ve added it to (infinity,1)-operad. I would also add to a suitable page on polynomial functors, but we’ve already reserved polynomial (∞,1)-functor for the Goodwillie version.
This seems a recipe for confusion:
The notion of “polynomial functor” we consider here should not be confused with the notion of “polynomial functor” introduced by Eilenberg and Mac Lane and subsequently used in the study of functor homology, nor with the notion occurring in Goodwillie’s calculus of functors.
Their version is a homotopified version of what we have as polynomial functor. They note:
The fundamental nature of these three operations is witnessed by the fact that they correspond precisely to substitution, dependent sums, and dependent products, the most basic building blocks of type theory [HoTT].
Not sure I’m up to cleaning out the Augean stables of mathematicians’ naming conventions.
Ugh. I’m not familiar with the functor-homology version, does anyone know what that is?
There’s not much content at polynomial (∞,1)-functor currently, and the definition suggests that anything one might want to say about that kind of polynomial (∞,1)-functor could equally well be placed at n-excisive (∞,1)-functor. So could we take over polynomial (∞,1)-functor for this, aligning terminologically with our page polynomial functor, and include a hatnote pointing the reader to n-excisive (∞,1)-functor or Goodwillie calculus if that’s what they’re after (like we already have at polynomial functor)?
Sounds good to me!
And we wouldn’t then have to change the currently misleading link to ’polynomial (infinity,1)-functor’ at polynomial functor.
Ok, I did that.
Re #99
In the KU-example above, for the particle on the boundary of the 2d PCS theory, the role of $A$ is played by tensoring with the prequantum line bundle of the boundary theory. Traditional geometric quantization is recovered here in the form that “the Hilbert space of quantum states of the particle is the 2-expectation value of its prequantum line bundle regarded as a boundary operator of the cobounding 2d PCS theory”.
In the tmf-example above, for the string on the boundary of the 3d CS theory, the role of $A$ is similarly played by tensoring with the Kalb-Ramond B-field 2-bundle.
Presumably this continues with something to do with the C-field. And what then if
the C-field is simply a cocycle in J- twisted Cohomotopy ?