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.
We should have a thread for Urs’s note.
Typo
found to be a concequence
The following is not easy to understand:
A type system as specified so far provides a scene for notions to be, but lacks as yet any determination of modes in which they may be, lacks qualification.
Concerning
A central insight of traditional formal logic is that such modalities are formalized by monads on the type system,
I wonder how many ’traditional’ modal logicians even know about (co)-monads.
Def. 2.5, Prop 2.6 arrive rather out of the blue.
Typo:
preserves all the and by assumption on infinitesimal extension,
Prop 2.12
which if
should be ’which is’
At the bottom of p.13 in ’proof’, should be , and the final should have s.
Oh, and the adjunction before ’proof’ is in terms of and rather than and .
Thanks!!
The typos you pointed out should be fixed now. (Eventually I need to make up my mind about about or …)
Concerning
The following is not easy to understand:
A type system H as specified so far provides a scene for notions to be, but lacks as yet any determination of modes in which they may be, lacks qualification.
Would this here be better:
A type system as specified so far provides a scene for notions to be, but lacks as yet any determination of qualities these notions may have, hence of modes of being.
?
Concerning
A central insight of traditional formal logic is that such modalities are formalized by monads on the type system,
I wonder how many ’traditional’ modal logicians even know about (co)-monads.
Would this here be better
A central insight of traditional formal logic is, when perceived from the foundations of type theory, that such \emph{modalities} are formalized by monads on the type system, traditionally called \emph{modalities} or \emph{modal operators} \cite{Lawvere70}:
?
Def. 2.5, Prop 2.6 arrive rather out of the blue.
The lines before it were supposed to lead up to it. But to make it clearer, I have added now the following remark below it:
The bottom piece of the diagram in prop. \ref{DecompositionIntoMoments} is the basic decomposition of into its dual moments and . The statement of prop. \ref{DecompositionIntoMoments} is that if is a stable homotopy type then first of all there is a further pair of opposite moments of , namely and and second that may be entirely reconstructed from either gluing with (along ) as well as from gluing with (along ).
Does that make the reasoning here clearer? If not, let me know and I’ll try to further clarify.
A type system H as specified so far provides a scene for notions to be, but lacks as yet any determination of qualities these notions may have, hence of modes of being.
That’s better. Still, it’s not clear how ’notion’ is being used. It appeared in the title of section 2.1 but not in the text. Used in any kind of technical way, it sounds old fashioned, as in old translations of Hegel, e.g. ’the absolute notion’. Most would use ’concept’ these days. ’Notion’ has a colloquial sense nowadays as a vague idea - ’I don’t have any notion what he’s on about’.
Whatever the word, you are presumably using it as something a type can be.
Maybe ’scene’ is a bit vague too. How about
A type system H as specified so far provides a setting for concepts, but lacks as yet any determination of qualities these concepts may have, hence of modes of being.
Then
A central insight of traditional formal logic is, when perceived from the foundations of type theory, that such \emph{modalities} are formalized by monads on the type system, traditionally called \emph{modalities} or \emph{modal operators} \cite{Lawvere70}:
Again, better, though traditional logicians only applied modalities to propositions.
Regarding Def. 2.5, Prop 2.6, I guess the question is who is your audience? If it’s only mathematicians, then I guess you can get away without any account of what a homotopy fiber is, or what and are, or a stable homotopy type,…. On the other hand, to have to explain all the ideas thoroughly would turn the note into several hundred pages. I’m just saying that a chunk of people at that Paris meeting won’t have much idea at various points, and there perhaps in particular.
Maybe regarding the last point, it’s because I myself am struggling with an intuitive image of the gluing in remark 2.7.
Thanks for the feedback. I’ll fine-tune a bit more in just a moment. One quick comment, on what you write:
I guess the question is who is your audience?
Yes, that’s indeed a big and unsolved question for me, not just for this note. How to communicate research that involves more than one academic speciality.
But for the moment I don’t want to be fine-tuning for exposition quite yet. I’ll extract an actual set of talk slides later.
Okay, I have now changed “scene” to “setting” and removed “notion” in favor of “type”.
Concerning the modal operators I have rephrased it
A central insight of traditional formal logic is, when generalized from propositions to types, that such modalities are formalized by monads on the type system, traditionally called modalities or modal operators [Law70, Moggi91, Shul12b]:
and added the Moggi-citation. It is curious that of all the citations that I once collected at modal type theory none really gives a clear review of the basic simple idea, Moggi91 itself is maybe still the best published reference. (?)
Prop. 2.8. in the diagrams there’s an which should be (bottom right corner).
Thanks! Fixed now.
You needed to fix two instances.
Oh, wow, that’s impressive. Impressively careless of me and impressively attentive of you!
Fixed now. Thanks!
I just had the document open there and refreshed. Doing that again I see ’morphsims’.
I was wondering whether the appearance of fibers and cofibers in 2.8 had anything to do with the modalities I noted over here. But I can’t see how.
p. 6 The commutative diagram should have not .
interpeting
p. 9
Thanks once more! Fixed now.
Yesterday night I finally got to turn to section 4 again, which I want to develop further once I find the time and energy.
First thing I did was to streamline the basic definition, now 4.7. I used to have this in an asymmetric form where I wa pull-pushing everything to the right of the correspondence, but now I have changed to the evident symmetric version, and I think that looks much more suggestive of how to proceed and what to make of this all.
It also made me think that there is something like amplimorphisms going on (whence the recent entry on that).
because given a correspondence of contexts
in some dependent linear type theory, and given types and , then a morphism of the form
is like a matrix (integral kernel) with entries parameterized by and values in maps betwen the components of and .
To quantize this (pass to the integral transformation that it defines) we form the “path integral” in the form of
and evaluate on the fundamental class by forming the composite
Now looking at this one sees that this only depends on not on the original matrix directly. Therefore one could consider allowing here maps
that do not nececearrily come from applying to some .
Comparison with the examples in Nuiten’s thesis show that these correspond to genuine “quantum propagators” that don’t come from quantizing anything. For instance the Freed-Witten anomaly cancellation for the superstring comes from a but the more general Freed-Witten-Kapustin version more generally from a .
Moreover, comparison with example 4.11 in the present note shows that in the special case where everything reduces to ordinary matrix calculus that having a that does not come from a means tensoring with an additional matrix, as in the definition of amplimorphism.
I have now finally made more explicit how the genral abstract integral transform reproduces pull-push in twisted generalized cohomology, now in section 4.3.2
Will you return to the paragraph beginning
The more philosophically inclined reader (and all others should skip ahead) might appreciate that our formalization has something to offer beyond just technical problem solving. It may also be regarded as resolving some of the infamous “problems of interpretation” of quantum physics, by translating them from inadequate common language to a genuinely well adapted formal logic…
Is the idea of a translation from ordinary language similar to what we saw in the case of general covariance from a context-free statement to “in the equivariant context, …”?
More typos:
statetement; cadinality; identifyign; remark 4.4 missing \dashv; fum; fumdamental; tradtional; associatd; leafs; with indicating (by indicating)
Thanks once more for spotting typos! Fixed now.
Regarding that remark: yes, I still want to add more discussin of this, still need to think about how to best say it. This is all about the form of def. 4.9, the stuff in #14 above. The dependent sums appearing here express the quantization:
First, on the far left, forms the space of quantum states. In models is the prequantum line bundle (I should maybe change notation to “”(?)), and the dependent sum produces its linear space of sections.
So logically this expresses something like “there is a point in phase space such that the system is in that state”. Now since we interpret this, first of all, in type theory, this becomes “the space of all such states”. Second, since we do it in homotopy type theory it becomes “the space of all such states and the gauge equivalences between them”. Finally third, since we do it even in linear homotopy type theory it becomes “the space formed as the linear superposition of all these states, added up and interfering (and taking gauge equivalences into account)”.
Next, there is the dependent sum over appearing in the middle of the big composite in def. 4.9. While and have the interpretation of phase spaces, the here has the interpretation of a space of paths between these two. (I should maybe find more suggestive notation to reflect this.) So the dependent sum here is really a path integral, and indeed it is, that’s what example 4.10 makes clear, this regards all the paths as forming a big matrix and acts with this matrix by summing up the contributions of all its entries between given source and domain.
Here the same comment as above applies: logically the expresses “there is a path”, type theoretically it is “the collection of all paths”, then homotopy-type theoretically it is “space of all paths and gauge transformations between them” and finally linear homotopy-type theoretically it is “superposition of all paths (with gauge transformations between them)”.
I’ll add comments along these lines to the file. Maybe now.
So logically this expresses something like “there is a point x in phase space X such that the system is in that state”. Now since we interpret this, first of all, in type theory, this becomes “the space of all such states”. Second, since we do it in homotopy type theory it becomes “the space of all such states and the gauge equivalences between them”. Finally third, since we do it even in linear homotopy type theory it becomes “the space formed as the linear superposition of all these states, added up and interfering (and taking gauge equivalences into account)”.
Does this sequence of logical unfolding of existence go some way to explain what you wrote elsewhere:
the fact that requires extra attention is not that quantum mechanics seems weird to our sensory apparatus, but that there is an approximation by classical physics where it does not. For some reason the earlier stages of the logical sequence are those we came to understand first.
I am not sure if it explains it. I find this pretty mysterious.
But also I think these kinds of questions are a bit too far ahead, this is why they seem so mysterious. The best to do here is, I’d think, to first just explore the formalism further (here: quantum physics axiomatized synthetically in linear/cohesive homotopy type theory) and then after a while the formalism will strengthen our senses and we might be able to think better questions.
If it has anything to do with Hegel, it will necessarily have a mysterious side to it. As Collingwood put it, Hegel was saying that the Universe “argued itself into existence”. It’s a theology of sorts.
As you say, probably it’s a better strategy to find how a working quantum type theory must go.
Typo: Writhmüller
I see you’ve added section 3.1. Can we understand how those who tried to relate linear logic with quantum mechanics would have confronted problems not having the full resources of a linear homotopy type theory? Don’t issues of gauge occur even in classical mechanics? So wouldn’t they be expected to need the ’homotopy’ aspect?
Right, thanks, I should give/recall more motivation at that point.
I’ll add a paragraph. Briefly, some key points are this:
as you notice, most every linear logic ever used as quantum logic applies to quantum mechanics only, not quantum field theory, and in fact typically authors concentrate on compact closed categories, hence where all objects are dualizable, hence on finite dimensional Hilbert spaces. This is the proper context for discussion of quantum computation, but it is a fairly small fragment (to borrow a term) of quantum phyiscs.
refinement to higher linear homotopy types becomes necessary as soon as one considers a) gauge symmetry (making the space of states a complex, the BRST complex) and b) locality (in that the state spaces assigned in higher codimension are no longer plain vector spaces).
finally, also discussion of non-gauge quantum mechanics needs higher homotopy types as soon as one realizes the quantization of the system as the boundary quantization of the Poisson-CS theory, that’s one of the examples currently discussed in the entry.
I’ll expand on that. Progress is sluggish as I don’t find much time at all to do work.
And the third reason would be: to describe quantization we need to be able to sum up linear types, hence the internal type theory of a single monoidal category will not be enough, we need dependent linear type theory. To phrase this as a principle would be to say that we need to allow for “Lagrangian field theories”.
So in summary that’s three pillars of modern QFT (it’s a) local b) Lagrangian c) gauge field theory) translating into three reasons why one needs to pass from plain linear type theory to a linear version of dependent homotopy-type theory.
As we discussed above #18, there’s something interesting about the order of the unfolding of the logic. It seems as though it ought to concern the subjective side, our coming to find out more about the world, and that the reverse direction could be used to explain our successively better approximations. Until we remember Hegel’s lessons.
In the quantum case, re #22, does embedding quantum mechanics in the full context of QFT make a difference to how we might view the former?
E.g.,
… the quantization of the system as the boundary quantization of the Poisson-CS theory
How should one think of this? There I was looking at two entangled particles and the correlation of their spins, but now looking on the other side of the holographic duality,…
Hi David,
I’d need to think about if there is a connection of that holographic stuff with Hegel. Would make for a flashy-sounding statement, but I am not sure if there is something.
To my mind the raison d’etre of the holography business is rather simply explained as such:
As everybody knows, by the cobordism theorem it is, of course, the topological QFTs that find a very fundamental axiomatization. Some people now go and try to equip cobordisms with extra geometric structure in order to mimic this for non-topological, hence geometric QFT. Progress on this however has been rather slow.
But an obvious aspect has remained somewhat out of focus: the full cobordism theorem, the way Lurie gives it on the last 10 pages of “On the classification” concerns topological QFT but with “boundaries” and “defects”. Now if one analyzes what happens in a topological QFT on a boundary, just following these axioms and using higher-prequantum theory, as in section 6 of “Diff. Coh. in a Coh. Topos”, then one finds that on the boundary extra non-topological data may appear.
And this is precisely what the statement of “holography” in physics is supposed to be, that the boundary theories of TQFTs are non-topological field theories.
So I think the non-topological QFT and “holography” is something that flows naturally out of just the theory of monoidal (oo,n)-categories with all duals, if only one considers the “full fragment” of that theory.
And this is where somehow the connection to the linear homotopy-type theory happens. I may need to think a bit more on how this connection is most naturally exhibited, though.
By the way, re entanglement of particles in the context of holography and recent discussion about that: on the one hand it is clear that, by the very construction, any counit-like morphism in a TQFT produces an entangled state of a very special sort, on the other hand a priori there is nothing in sight that deserves to be called a “particle”. If one thinks of the TQFT as being a quantum theory of pure quantum gravity, then that entangled state is of that gravitational field of the “whole universe”, as seen by the TQFT. Discussion of how to extract a notion of “particle” in any standard sense from this will be rather subtle and in any case hasn’t been done in what I have seen.
I’m on shaky ground here, but to try and get clear, when I read something about
a holographic relation between higher geometric quantization of the 2d Poisson-Chern-Simons theory and quantum mechanics as a 1d quantum field theory,
is your comment #26 speaking to this? Something like there may be a particle account (QM) for the non-topological boundary, but this doesn’t mean there’s necessarily anything particle-like to extract from the bulk?
Yes, so the key here is to keep straight the difference between first quantized and second quantized theory, between the worldvolume theory of a single brane (which might be a particle) and the spacetime theory of fields that may have particles as quanta.
Given an -dimensional QFT, defined on arbitrary topology (-dimensional cobordisms) there are always two different physical interpretations of it:
the whole QFT may be thought of as describing the propagation of a single -brane through a “space” which may only be very indirectly be inferred from that QFT (namely by spectral geometry), here a cobordism in the domain is a piece of “worldvolume” of the -brane
we think of the cobordism as “spacetime” and of the whole QFT as being a theory of fields propagating on that spacetime.
The concept of particle comes in in both items, in different ways:
in the first case, the special case where we say is the worldline theory of a single particle; (the “first quantization” of a particle);
in the second case, we can try to find regimes of the theory in which it looks approximately like a free field theory. Then (and only then) is there an unambiguous notion of its fields as having “particle quanta”. In this case the field theory would be thought of as the “second quantization” of these particle quanta.
This second step is very subtle, as AQFT people like to highlight and many other people like to forget. A review is for instance in
following chapter VI of
If one wants to be on the safe side, then one does not speak of “particles” at all much in field theory. Some people like to say: “That’s why it’s called field theory.” Particles in second-quantized field theory are like a special kind of coordinates for fields that can be found only in favorable circumstances, typically for non-covariant free field theories .
This means first of all that if your n-dimensional QFT here is a theory of (quantum) gravity, the particle concept a priori is not available at all. To get it, you’d need to do two things first: 1. pass to a limit in which your QFT somehow decouples as a gravitational fixed background with non-gravitational quantum fields propagating on that and 2. pass in that limit further to a limit where the gravitational background is sufficiently flat or otherwise symmetric to allow a decomposition of the quantum fields on it into particle excitations (Fourier modes, and similar).
So in the example that you cite above we have the 2d Poisson-Chern-Simons QFT and on its boundary hence a 1d QFT. So the statement here is that 2d PCS theory has first quantized particles as its boundary theory.
As you see, this works exclusively for boundaries of 2d QFTs. An -dimensional QFT has first quantized (n-2)-branes as its boundary theory.
In another class of examples, if you consider 3d quantum gravity as given by one of the standard Chern-Simons type 3d TQFTs, then if you are looking from the perspective of first-quantized theories then its boundary theories are not particles, but strings. This is the AdS3-CFT2 and CS-WZW correspondence. If on the other hand you look from the perspective of second quantized particles, I am not aware of a way to extract anything at all of this kind from a CS-type 3d TQFT.
(Elsewhere people like to consider codimension 2-defects of 3d TQFT, and, by dimensional counting, these may be thought of as particles, more commonly they would be called 0-branes inside the 3d bulk theory.)
I have now added some of these comments to particle. But let’s move discussion of that to its own thread.
In a stolen free minute I have started a new section in the notes,
“4.4 Dagger-compactness and Positivity”
discussing how -compact structure is recovered as a special case of linear type theory equipped with what I called orientations and fundamental classes.
This needs to be expanded much more. But it’s a start. And now I have already to go offline again.
p. 15 better if the two ’1,2,3’s lined up. Now you have (local, Lagrangian, gauge) then (gauge, local, Lagrangian).
p. 23 “th concept”
Thanks. I have changed the order of the three items now. I had thought about that: It seemed to me that the permutation that flows most naturally is “local Lagrangian gauge field theory”, but in that order (local, Lagrangian, gauge) the explanation of what this comes down to in type theory seemed awkward. Now I opted for “Lagrangian local gauge field theory” which misses the desirable pair “local Lagrangian” but might be a compromise.
An occurence of “th concept” I fail to spot or have the editor search for. Maybe I am just too tired. Or maybe I had already fixed it locally earlier.
Then I have expanded the note in section “4.4 Dagger-Compactness and Positivity” just a bit more. I am not yet sure what to make of this. The observation there says that the structure in linear homotopy-type theory which equivalently deserves to be called “twisted orientation” or “Wirthmüller isomorphism” or “twisted ambidexterity” is a generalization of the dagger-compactness. That makes one want to look for completely positive maps on that level and in that generality. Applied to the example of pull-push in twisted generalized cohomology that might come down to something interesting about bivariant cohomology. But I am not sure yet.
Urs, I hope the question isn’t too obnoxious, but do you ever use spell-check? :-)
I suppose I should use it at least before finalizing. On documents like this, though, it gives me tons of spurious hits, to wade through.
Yes “th concept” has gone.
Tonyjones, thanks for this hint! Both bordisms as well as multi-dimensionality of syntax, which I suppose is related to wgat we here would call “directed homotopy type theory”, is something that, in the context of dependent linear type theory, is precisely the next big topic lurking behind the discusdion here so far. I usually think that this is presently out of reach. But maybe more is known than i am aware of. I’ll try to track down the reference tht you are indicating a soon as i have a spare minute.
I haven’t found a free copy of the article
yet, but I found the abstract:
We develop a multidimensional syntax for cut-free proofs of Multiplicative Linear Logic. This syntax is essentially equivalent to the traditional formalism of proof-nets; the interest of the multi-dimensional formalism consists in its explicit relationship with the formalism of bordisms. Bordisms are compact manifolds with boundary, which are treated as morphisms between the ‘incoming’ and ‘outgoing’ boundary components (composition is given by glueing bordisms along matching boundaries). The category of bordisms has recently become important in contemporary mathematics, in particular, because of developments in topological quantum theory and quantum gravity. A semantics of MLL underlying the multi-dimensional syntax is based on a certain category of bordisms, which we call ‘coherent space-times’. The resulting model has an extremely intuitive geometric description. The dual multiplicative connectives and correspond simply to disjoint unions and connected sums of bordisms. Following ideas from topological quantum field theory, we also discover deep relationships between this new model and the author’s coherent phase spaces model (Slavnov 2003), which is based on the context of symplectic geometry.
From your comment I started having the idea that this would be about extended cobordism, but it seems to be the observation that the ordinary category of cobordisms is symmetric monoidal and hence interprets MILL. Four years later that point was amplified in (Baez-Stay 09).
I’ve sent the paper to you.
That makes me think, what happened to diagrammatic syntax and HoTT? Should we be rolling out Mike’s diagrams for linear type theory? What can be done about the ’homotopy’ aspect?
Re #38: certainly others have floated the idea of cut elimination or beta reduction (which is being discussed in another thread) being modeled on cancellation of critical points in Morse theory, with “commutative conversions” (in the argot of Girard) modeled on various rearrangement lemmas for moving indexes of critical points around (replacing one Morse function by another in some controlled way). Certainly surface diagram models of eta expansion and beta reduction were among the applications that Ross Street and Dominic Verity and I were discussing when surface diagrams were being bandied about, back in that day.
Thanks, David!
Sure enough, Sergey Slavnov in 2005 made explicit the point that since multiplicative linear logic has semantics in symmetric monoidal categories, it in particular has so in categories of cobordisms that serve as domains for FQFT. He even mentions a version of the symplectic category as another example, this way at least hinting at interpreting also quantization this way, which certainly makes a connection to the present discussion.
I have added the citation at quantum logic here.
Thanks, Todd. My #41 overlapped with your #40, I only see it now.
Indeed, Slavnov credits private communitcation with Richard Blute for the idea!
If you have further (older) citations, I’d certainly be interested.
I think the first public instance I remember seeing of this idea was in a lecture by David Yetter, a long time ago (1988 or 1989) in the McGill Category Seminar. I might write him to ask. He certainly spoke of cut-elimination in the context of cancellation of critical points. It wouldn’t surprise me a bit if the idea were older still.
Note to self, and possibly others: Milnor’s Lectures on the h-cobordism theorem is a useful reference for these cancellation and rearrangement theorems.
I see. For my citation needs, I’d be particularly interested in citations that explicitly make the connection between linear logic and TQFT, via Atiyah’s observation from 1990 that cobordisms serve to model QFT.
Speaking of Yetter, while Slavnov does not cite Yetter, he cites Crane 1993, for the construction of a category of embedded cobordisms. Crane made the connection to QFT (clearly) but it seems he did not connect to linear logic.
In the lecture, Yetter definitely connected to (cyclic) linear logic. But I don’t know whether he published or pre-published anything on it.
The end of proposition 2.7 (after the diagrams) is ungrammatical (I guess you mean that the two squares are cartesian).
I like the CLI analogy, by the way. :-)
Thanks, David R.! Fixed now.
Is there any connection between the comodality ! being called exponential conjunction and the exponential map between Lie algebras and Lie groups? Would the tangent to provide an example in 4.2? What does that of the adjunction there typically do?
I doubt that there is any real relation to Lie theory or tangents. Much of this terminology in linear logic seems to be adopted just so as to have some term that is vaguely suggestive. Here for the !-modality the idea is that it produces arbitrary many “copies of a resource” and that reminds one of an exponential. (Over in another thread we saw an article by Richard Blute talk about “entropy” in linear logic, and I don’t think the concept he called by this name had anything much at all to do with entropy).
To get a feeling for what would do: consider the dependent linear type theory of vector spaces parameterized by sets. Then takes a finite set to the -dimensional vector space. And hence takes a vector space to its underlying set.
Typos
promt; bottom morphism if the
@David, re #48-#50:
One thought on the exponential: so in that archtypical model of vector spaces over sets, then the !-modality is the operation that takes a vector space to the vector space free on its underlying set of sectors, .
Which operation in quantum physics might that remind one of? Very, very vaguely it maybe reminds one of second quantization, it is a bit like weird variant of a Fock space construction. Not sure if that leads anywhere…
Thanks for yet more un-typos in #52 !
@Tonyjones re #51:
I am really not sure at this stage what one might be going to say about quantum cosmology.
My attitude with such issues is a bit like going through the third gate at the entry to the Southern Oracle: maybe if we forget the question and just immerse ourselves into a genuinely well adapted formalism (linear homotopy-type theory), then eventually both the question and its answer will become clear.
@David,
hm, what I just said reminded me of
For a symmetric monoidal category, p. 11 there considers the category of co-commutative comonoids in and on the bottom of page 11 there is a remark on how one should think of as a category of spaces.
Then def. 4.1 asks for a right adjoint to the canonical functor .
Then the induced “!-modality” is interpreted as the Fock space construction/second quantization construction on .
Indeed, on the next page Jamie points to a note by Fiore (pdf) that connects this to the linear-logic perspective.
Hm, so I was wrong above. And, hm, this is something to think about…
[ edit: I have now started to collect some material on this at Fock space and at !-modality ]
so I was wrong above
about what?
Fiore writes
Recent developments in the model theory of linear logic, starting with the work of Ehrhard [6, 7], have uncovered a variety of models with differential structure…. In this context, a differential operator is a natural linear map…that, when embedded as a map in the !-Kleisli category, enjoys the properties and satisfies the laws of differentiation. Intuitively, such an operator D provides a linear approximation…for every function…
Won’t there be some kind of connection between dependent linear type theory and Goodwillie calculus, tangent cohesion, parameterized spectra, etc.?
I was wrong above in voicing the ignorant opinion that the !-modality’s relation to exponentials is a bit of a stretch. Instead, it is quite apt.
Regarding your question: I certainly follow your intuition. I need to think about how to substantiate it. Might get to that tonight.
Thanks for the links.The first link is already listed at !-modality, Fock space. In the abstract there it says, if I understand correctly, that this is an expanded and improved version of the second one that you list. Is that right?
Thanks.
And it’s true, above I had only remembered Jamie’s article, and then found and added Blute’s at al’s without mentioning it here explicitly.
It seems that Blute’s work predates many things that were then rediscovered a good bit later…
Re #56, linear logic meets Goodwillie calculus, etc., there is an idea of something like an exponential function at play in the latter. Arone and Kankaanrinta are mentioned on Goodwillie calculus as having the idea that is like . So that’s an adjunction between and .
Thanks, David. I think you have a good point here. It is generally true that or more generally behaves like an exponential. And on pointed spaces with smash product suspension is monoidal.
Putting it together this would mean that if is regarded as the space of states of some TQFT, then would be a candidate for its “second quantized Fock space”.
I am not sure yet what to make of this. But this sure seems like something to think about more.
There is this MO discussion on “when spectra have diagonals” (hence in our language here: when do they have the structure of a non-linear type). John Klein points to an article of his that they do precisely if they are suspension spectra. Moreover, the proof crucially uses (the Goodwillie expansion of) what you would now call the exponential modality, namely
So that seems to harmonize well with your suggestion. Maybe this may be fleshed out a bit more.
So little time unfortunately these days for such interesting things, but I see Kuhn’s theorem mentioned by Klein parallels the expansion of the exponential function.
Thanks, I have added the link here
So how much will linear homotopy type theory detect of the Goodwillie calculus? Presumably the former is dealing in general with linear types over nonlinear types, so can’t say everything about the specifics of some particular functor from spaces to spectra, but something like
the th Taylor coefficient of the functor sending a spectrum to is the sphere spectrum for all Kuhn 2004
is just an interpretation of the exponential expansion of !. But maybe we wouldn’t expect the specifics of, say, chromatic homotopy theory to appear?
Is there something special about the case where the model of linear types dependent on nonlinear types is still a topos?
While we explore, this here seems to be worth keeping in mind:
as Mike emphasized elsewhere, following his work on monoidal fibrations, once we do consider not just linear type theory but dependent linear type theory then there is a canonical choice of the left-adjoint (or would-be left adjoint) from non-linear types to linear type, namely the map
When applied to the standard model of spectra parameterized over -groupoids, then this sends a homotopy type in general not to its suspension spectrum, but to homology spectrum (generalized Thom spectrum, if you wish ). Only if the homotopy type is a suitable finite homotopy type (a compact manifold) and some twists here and there do we have, by Atiyah duality, that the dual of that may be a suspension spectrum.
Of course in general we are free to make a choice for . But maybe this “canonical” choice for will be more interesting than others.
But I don’t know.
I’m not sure what you mean by , but the canonical functor I had in mind applies to the unit object of the monoidal category of -indexed spectra, i.e. the -parametrized sphere spectrum, and in that case you do get the suspension spectrum of .
Sorry, you are right, of course. I am being stupid.
What now then? Andre Joyal appears along many of the leads I can think of, e.g., tangent toposes, Goodwillie calculus, and there’s also some kind of connection between structure species and linear logic as here:
The construction leading to the Kleisli bicategory of generalised species is analogous to the construction of the relational model of linear logic [20]. This model can be seen to arise by observing that the monad on the category of sets whose algebras are commutative monoids extends to a monad on the category of relations via a distributive law. Using the duality available on the category of relations, this monad can be turned into a comonad that has the properties of a linear exponential comonad and thus determines a cartesian closed category via the Kleisli construction (see, e.g., [8]). Our work demonstrates that it is possible to carry over a similar programme in the context of 2-dimensional category theory, with the 2-category of small categories replacing the category of sets, the bicategory of profunctors replacing the category of relations, the 2-monad for symmetric [strict] monoidal categories replacing the monad for commutative monoids, and the duality on profunctors replacing the duality on relations.
Hi, okay, I am back online. Still haven’t really slept enough, but I trust that you guys will bear with me for the time being…
Regarding exploring the role of in the context of linear homotopy-type theory regarded as a context of quantum logic, maybe here is a thought:
so given a linear homotopy-type theory
then once the dust has settled, the quantization of a given action functional subject to a choice of consistent path integral measure yields a TQFT in the form of an -functor
which on objects is given by first assigning some (the “prequantum bundle” on ) and then sending that to its space of (dual) sections . (All as in section 7 of my note.)
Consider restricting the above functor along the inclusion
which sends morphisms in to the “right-way” morphisms in , so that we get
Then in the special case where the “twists” or “anomalies” of the theory are all trivial in that throughout, then this functor is just the -functor as in (Ponto-Shulman 12 (4.3)).
(The quantization functor sends a correspondence essentialy to “daggered-counit of right leg followed by integral kernel on correspondence space, followed by counit of left leg, and under the above embedding of this comes down to just “counit”, which is the formula in Ponto-Shulman. )
So, in general the path integral theory is a twisted generalized version of the canonical left adjoint in the adjunction for the exponential modality.
I suppose it would be interesting to ask now if or when this more general has a right adjoint, to make for other choices of exponential modalities.
And in view of this let’s come back to the idea that the exponential modality is supposed to “second quantize” a given QFT by sending each of its spaces of states to the corresponding Fock space.
Here this would mean something like that one starts out with a QFT , maybe restricts it again to , then first applies the right adjoint to it, let’s write it for definiteness, to produce a map which somehow is to be thought of as sending the phase space of a single system(particle) to a new huge phase space which is really the space where each classical configuration is a quantum state of the quantization of that single system. Then if we imagine that we can aggain assign consistent twists on that (or we just use the trivial one). we form
and this would now be interpreted as a the QFT which reads in a phase space and spits out a quantum theory whose states form something like the Fock space of the original theory over that . So indeed begins to look like a second quantization of .
Maybe something to explore. Let’s hope I am lucky and this will be a more quiet day…
Seems pretty lucid to me! I wonder how I fared when I entered the infant-induced sleep deprivation state nearly 22 years ago. It probably didn’t help my Masters thesis I was writing.
Anyway, will get back to this after my Philosophy of Medicine class.
Actually, I am in a comfortable situation; I can relax and fire around shaky statements without thinking, for in case they are nonsense I may always blame it on the little one’s digestion.
Anyway, I have now re-written section 4.2 “Exponential modality and Linear spaces of sections” of my notes in view of the points that you and Mike have been driving through my thick skull with some patience (I have added a footnote acknowledging this).
Now I’ll go back to section 7 and add some discussion of why the TQFT functors obtained there are in fact monoidal. Then I might have time to think about that second quantization story. Now that I see the pieces fit together, it looks pretty interesting.
Did anyone ever see a draft of
Gepner, D. and J. Kock, Polynomial functors over infinity categories, in preparation?
Can #73 be related to what you wrote here
a local TQFT is defined by a cocycle
After quantization this is supposed to give a morphism
Now one can make some plausibility arguments to the extent that what second quantization is supposed to be is a way to regard again as a cocycle on par with the original (an “-directed cocycle”, now, remember that we talked about this once) and so that there should be a way to just repeat the original quantization step, but now taking as input where previously we took as input.
I really feel like this will be the way it should work. But there is plenty of white space to be charted in making sense of what it would mean to generalize what we do to the cocycle more generally to an “-directed cocycle” .
I don’t see how it will be related, but beware also that these are two different concepts:
just forming Fock spaces is really just the “free” part of second quantization. It constructs a theory of arbitrarily many of the original systems (particles) which however don’t interact with each other. This is very rarely of actual interest in physics. Instead in physics one follows this “functorial” step of passing to Fock spaces by the step of adding interaction terms to the new Fock Hamiltonian.
And that kind of interaction is what my rough proposal in #73 is aiming at. What I indicate in #73 is meant to be a formalization of another way of going about second quantization, one that automatically has all the interactions built in, and that is the process of defining a second quantized S-matrix by taking its components to be the sum over all possible shapes of paths of the S-matrix of the first quantized theory.
The first process of quantization via Fock spaces is most commonly used in solid state physics and hence in non-relativistic particle physics. The second is what is used in fundamental particle physics (where it is known as the worldline method).
Both processes are clearly conceptually related. But I don’t see at the moment how the 1.5 formalizations of them that we have are related.
re #76
Did anyone ever see a draft of
Gepner, D. and J. Kock, Polynomial functors over infinity categories, in preparation?
I haven’t seen this yet… but if you allow me to go off a tangent:
you asking about this made me go and expand section 3.4 just a little bit.
The following observation, simple as it is, might be interesting:
so the notion of polynomial functor is a categorification of that of polynomial, hence is a “higher dimensional/directed polynomial”.
Now looking at which role the polynomial functors play in quantization in terms of linear homotopy-type theory, then we see:
the polynomial funtors themselves are the propagators of a -dimensional TQFT, and go between “2-modules”, hence higher directed space of states;
their boundary field theories are -dimensional TQFTs whose propagators are “actual linear polynomial functions” mapping between actual (non-categorified) spaces of states.
Section “7.4 Holography” is meant to comment a bit on this, though I guess that section is currently still lacking a decent lead-in.
It doesn’t sound like that paper will appear any time soon:
This is in a forthcoming(?) paper by Gepner and Kock, which unfortunately has been ‘nearly finished’ for the several years :-(
In 1.2.1, you’re suggesting that mathematicization + familiarity leads to demystification, and perhaps a further step from an initial mathematical theory to one which might be called a “logic”. Presumably this is exemplified by the demystification in the century from Newton to Lagrange. Still with Newton there are concerns about an instantaneous force acting between each pair of bodies without an account of an emanation of particles between them mediating the force. But then, couldn’t we think that this worry was a good worry to have, and would need addressing at some point.? But maybe most efficient to get on with the improvement of the mathematicization, say, to an analytical mechanics, and leave the earlier worry to reappear in the later formalism.
Hi David, thanks for the comment.
But then, couldn’t we think that this worry was a good worry to have
Yes! But you are one step ahead here. I am trying to address the concern of an audience potentially less far-sighted than you are. Because at that point I want to use this the other way around:
Most people usually tend not to feel worried by the concept of point masses acted on by forces-at-a-distance, while at the same time feeling worried about the concepts of quantum physics. This goes to the extent that many (most, I would say) feel that to “interpret” the latter one has to reduce them to the former! That’s what is the goal of most hidden variable theories, notably Bohmian mechanics is all about.
And exactly this is what I tried to critically highlight here: that many people tend to not feel they need an “interpretation” for point-masses-and-forces-at-a-distance is really not so much because at the face of it that had no weird aspects about it. But if that’s not what it is, then it must be something else. And I tried to convey the argument that one tends to feel less a need of further explanation when a state of affairs is transparent, and allows deduction that leads to plenty of insights. Then after a while it will feel obvious enough and not in need of further “interpretation”. It becomes in the genuine sense of the word: self-explanatory.
This was meant as the jumping-off point for my concluding motivation (since the hosts of the conference had stressed that they would like me to comment on potential impact of new mathematics on old riddles of quantum phyiscs). I wanted to say: let’s postpone worrying about the need for “interpretation” of quantum physics a bit. Once we have a formal language that is more transparent, more self-explanatory, and makes deep issues that presently seem subtle come out more obviously, then the feeling that any further “interpretation” is needed may just disappear.
I may not have found the best words for this, not sure. But this seems to be a common phenomenon of life that if reality seems weird to me (say as a small kid, or later when I first travel alone to a foreign country), then sometimes that’s because reality indeed is weird, but more often than not it is because my internal language does not yet well reflect what is really a straightforward affair.
But thanks for the comment. I’ll see if I can fine tune the sentence in question in my document a little.
The difficulty with worries at early stages is that it’s hard to know what’s important about them. With Newton things are tied up with theological concerns, “space is the sensorium of God”. It surely helped that it went through a deeper mathematicisation and that another force, electromagnetism, made Newtonian principles problematic. One might imagine that 1930s worries about QM will crystallise into important and discardable parts. An important part may be at stake in getting straight on quantum gravity. But as to when the time is ripe is not so clear. Untimely ’philosophical’ insight is possible, but is rarely causally effective, as with Hegel and the planets’ free motion.
Right, so I suppose we agree? Unless we have (and we don’t) a Hegelian oracle that we know we may trust (and know how to read) then worrying about the “interpretation” of a physical theory tends to better be postponed until its mathematical formulation has ripened.
Which leads to another comment which I tried to briefly make in that opening paragraph: it is curious how in the existing literature discussion of foundational issues in quantum physics tends to focus on quantum mechanics. Of course this is the case where we really understand the mathematical formulation of the theory, but we also know that this is just a toy example of the real issue, which is quantum field theory, where the mathematical foundations are much more under discussion.
I often find it weird to see those texts on foundations of quantum physics hold the banner of the quest for quantum gravity – quantum cosmology even – while at the same time entirely focusing on quantum mechanics, with no hint of even the existence of quantum field theory. That’s like trying to discover a new continent by setting sail in your garden pond.
Yes, we’re agreeing. And also on QFT. I remember worrying about this to an Oxford philosopher of physics about 12 years ago and being told that all the problems were already there in QM. That struck me as doubtful.
Anyway, as for timing, with linear dependent type theory, etc. available, how long until a useful thinking about interpretation becomes possible? Are we like 1860s electromagnetism, or nearer a late 19th century situation where reading Mach may give some pay off in a few years?
Hard to tell, but it seems plausible that at a few places one needs to get used to a rather drastic re-thinking.
Consider for instance how the traditionally notoriously elusive path integral appears in what I am discussing, also in (Hopkins-Lurie 14): what is traditionally thought of as a process that adds up numbers apparently really has to be thought of as something that adds up something rather different from just numbers. Instead what is being added up is more like elements of -rings. That has some relation to addition of numbers,but is in general a rather richer and in any case different process.
Concretely, for the quantization of particles: it used to be clear and fundamental that the ground ring of the whole theory is the complex numbers . But now it seems clear that the ground ring in this case is rather KU. The traditional theory of Hilbert spaces and operator algebra over complex numbers now appears only as a particular presentation of what intrinsically is higher linear algebra over (namely via the presentation of via KK-theory).
Or consider the by now decades-old attempts to realize the String orientation of tmf as the non-perturbative partition function of a mathematically precise quantization of the superstring. Despite all the hopes, that has yet to work out, and progress has pretty much stalled. And of course in these attempts one tries to quantize the superstring by something more or less traditional, involving states in vectors spaces over the complex numbers.
But now this result drops out naturally from quantization in linear homotopy-type theory. It’s the change in perspective that makes it fall into place: since the cobounding theory is 3-dimensional, it has as 3-group of phases and hence to quantize we need to find a natural linear representation of that in some automorpism -group. The “canonical” such is the representation in , simply because that has the right homotopical structure. Then one finds that given this linearization the universal boundary condition for the theory essentially is the String orientation of tmf and so the Witten genus comes out.
So that’s a change of perspective: instead of producing tmf (or related) by processes involving addition over the complex numbers, we see that the natural perspective is to entirely replace as a ground ring by . That puts much of previous effort upside down… and I would argue puts it from its head to its feet.
So that changes the landscape of what to ask about the numbers needed in QM, but will there be a moment where worries which are quite expressible in natural language come to be addressed, as when the problems with instantaneous action at a distance and absolute Space, Time, and Motion found their resolution? It seems that waiting for the mathematics to improve and so refine the issues is a good idea, but do such issues ever completely disappear or do we need also some new interpretative insight?
Maybe you need to give me a concrete worry so that I have a better idea what you are after.
Something general and something more specific which I can say is this:
Generally:
As long as physical concepts are just postulated, be it absolute space, or a spacetime manifold etc., we may always feel worried about whether there is something more natural that one could have thought of. (These days people in quantum gravity worry whether it is reasonable to assume that spacetime is really a smooth manifold, for instance.) But what I have been trying to advertize above is that once however we find that the physical concepts we use arise essentially by themselves from the very substrate of logic, then nothing much is left to worry about. If we may agree that linear homotopy-type theory is something essentially “god given” and when we then observe that quantum field theory arises in the interplay of correspondences in linear homotopy-type theory, then what would be left to worry about? It’s no longer a human choice. It just is.
Specifically:
The central worry about quantum mechanics that people have is its probabilistic nature combined with the postulate (or non-postulate, depending on school of thought) of “wavefunction collapse” after measurement, mathematically implemented by projection operators onto closed subspaces of the Hilbert space. (“The measurement problem”.) This – we had discussed this a while back in the thread on quantum logic – seems to be actually rather nicely dealt with in linear logic aka quantum logic, thought of as embedded into linear homotopy-type theory. The ambient linear homotopy-type theory provides, it seems, all of the infrastructure of what you’d want to see in quantum field theory, calming the complaint about BvN quantum logic as missing the main points of actual quantum dynamics; while at the same time the propositions in the linear type theory – the (-1)-truncated types – are still given by projections onto linear subspaces. So we have a refined kind of logic – linear homotopy-type theory – which describes quantum field theoretic processes in their probabilistic nature and is at the same time such that making propositions about these QFT systems means “wave function collapse”. All this from the logical substrate, nothing put in “by hand”. Seems to be rather beautiful to me. (But I guess this point deserves to be further elaborated on eventually…)
I can’t seem to find it now, but we did discuss once the problems with quantum gravity. Something like QFT/QM yields predictions for events in regions of spacetime in which an experiment takes place, and how could this be extended to the whole universe.
I have come to the heretic opinion that the problem of observers in “quantum cosmology” is not any different than that in “classical cosmology”. Here is what I mean:
Assume for the moment, as lots of people around us do, that once it is done then quantum gravity is a TQFT
(of course that’s a bit of an assumption here, but let’s go with this to have something a bit concrete to talk about).
Imagine that this arises from a quantization process the way it is discussed in the notes that this thread is about
Here the first functor is the “classical” (prequantum) theory, the second is the quantization step.
So feeding closed -manifolds into this it tells us about the spaces of states of “cosmologies” of shapes these manifolds, and how they propagate.
The intermediate functor gives classical states, the total functor quantum states. In either case, since, we imagine, all these functors are constructed (as done in the notes in high codimension) using homotopy-type theory and linear homotopy-type theory, we may formally analyze them within this logical framework. There are propositions about the states, and in the quantum case they come with projection/collapse operators and so forth. Nothing left mysterious, all formal logic.
Except one thing: now you ask “Fine, so this is the external perspective on this universe described by . But what do “observers inside that universe” see and feel? “
Yes, that’s a super-difficult question. In fact, how do we even see if “inside ” there is anything like an observer at all?
But this problem is not one of quantum, but one of cosmology: because the same problem we have for the functor . If I hand you such a functor, hence a “classical cosmology”, how do you know what “observers inside this cosmology” are and feel.
This is a deep riddle. It’s related to that Penrose triangle (not to mention Mr. H. yet again) which we discussed another time in another thread. But whatever it is, I come to think, for the above reason, that it’s not an issue related to “quantum”.
Re #88,
So we have a refined kind of logic – linear homotopy-type theory – which describes quantum field theoretic processes in their probabilistic nature and is at the same time such that making propositions about these QFT systems means “wave function collapse”. All this from the logical substrate, nothing put in “by hand”. Seems to be rather beautiful to me. (But I guess this point deserves to be further elaborated on eventually…)
This would be just the kind of account that we should take to philosophers of physics.
Re # 90, is there any room in this picture for the ’critical’ aspect in the Kantian sense? His ’Copernican revolution’ was to take our knowledge of the world not to be of the thing-in-itself, but the world as taken up within our faculty of reason, a combination of the categories of the understanding (objecthood, causality, necessity, etc.) and the contents of our intuition. This wasn’t meant just to apply to a person’s everyday judgements. Even the theoretical resources of the leading science of the day, Newtonianism, arose out of the categories.
Looking at what you just wrote, Kant would find enormously problematic your “external perspective on this universe described by ”. There can be no such thing for him. But then maybe that’s why you’re a Hegelian ;) – the categories aren’t just to be read off from our judgements, but derived in Logic, the same Logic that drove the creation of the universe.
So, any interesting reaction to the talks, especially from the philosophers there at the first one?
My lightning appearance and disappearance at the meeting in Paris limited the amount of possible discussion.
Over joint lunch after the talk one point that proved to resonate with some participants was the observation that the gauge principle in physics is the same as what makes types be homotopy types.
One participant said he enjoyed the appearance of motivic structures.
Another participant wondered if I could see in the formalization that I was talking about the point that he was advertizing in his talk, namely that the quantum phase should be thought of as a remnant of gauge equivalence. (My reply: maybe sort of, vaguely, but maybe not quite the way he is envisioning).
The observation that string-theoretic structures appear by themselves from the fromalization (not being explicitly asked for) led some to wonder.
The gentleman who runs that archive with plenty of historical records of talks by Lawvere videotaped my talk and expressed a fair bit of general interest.
Before my talk I had the chance to chat with Gabriel Catren and his group a bit and I expressed and we agreed that the existence alone of a group and grant like his (pairing physics with philosophy and mathematics) is quite remarkable. Indeed, he recounted a story of how a fellow professor, not recognizing him, vividly expressed his disdain for the European Union giving money to anything with both “philosophy” and “physics” in the title.
Myself, I feel that there is a bit of a technology distance between what I am advertizing and what most other participants who were at the workshop in Paris are working on.
That was of course different at the ESI meeting afterwards. There I didn’t dwell on any foundational questions but concentrated on the mathematical technology. Among the participants it seems that Uli Bunke and Thomas Nikolaus were those who appreciated the stuff genuinely. In fact there was some nice connection to Thomas’s talk (which was an impressive list of unpublished results on the generalized cohomology of T-duality). If all goes well then Joost and maybe myself will go to Regensburg for a little by summer or end of the year to talk more.
The gentleman who runs that archive
Michael Wright. I’d mentioned your work in a couple of talks he has attended.
I’d like to understand the following better:
So we have a refined kind of logic – linear homotopy-type theory – which describes quantum field theoretic processes in their probabilistic nature and is at the same time such that making propositions about these QFT systems means “wave function collapse”.
You relate the probabilistic nature of quantum physics to the dagger-compact structure, as laid out in section 4.5. Is that the place to look?
A Regensburg trip sounds interesting. It would be great to see some of these ideas penetrate further into number theory, such as arXiv:1209.6451.
Michael Wright. I’d mentioned your work in a couple of talks he has attended.
Thanks. We had agreed to stay in contact, but somehow we didn’t. I have created now an nLab entry Michael Wright and also one for his Archive for Mathematical Sciences and Philosophy. I was told fascinating stories about this archive. Too bad that it leads an offline analog life for the time being.
You relate the probabilistic nature of quantum physics to the dagger-compact structure, as laid out in section 4.5. Is that the place to look?
So the fact that the probabilistic nature of QM is well captured by the dagger-structure on a suitable linear category (say of finite-dimensional Hilbert spaces) is something very much emphasized by the “categorical quantum mechanics” crowd in the wake of Abramsky and Coecke. Maybe I should have added more of a comment on that in the file.
The observation that I meant to add in that section 4.5 is that in linear homotopy-type theory this becomes a bit deeper still. Here the dagger-structure becomes the existence of Umkehr maps/fiber integration maps via Poincaré duality in generalized cohomology and gives rise to a rigorous and useful path integral. Or put more simply: we have probability amplitudes not just with values in the complex numbers, but with values in rings like KU and tmf. I suppose it remains to be seen what to make of this relation…
Regarding Regensburg, yes, there will be plenty of interesting connections…
And how do you pass from KU and tmf to measurable quantities? Is there something like , for complex numbers? Don’t we have to pass from codomains of genera to the reals at some point?
So the relation between the dagger-structure and the inner product on Hilbert spaces is the following:
if a vector in a (finite dimensional, for simplicity) Hilbert space is thought of as a morphism
then of that is
and the pairing (which is a linear endomorphism of the ground rign, hence identified with an element of that ring) produces the probability of any observable operator .
All these ingredients lift to the field theoretic quantization in linear homotopy-type theory now.
For instance for the quantization of a compact symplectic manifold as the boundary theory of the 2d Poisson-Chern-Simons theory then the state is a -linear map
given by the K-theory class of the prequantum line bundle on , and then the dagger structure allows to pair to a -linear map
which represents a single K-theory class. The virtual vector space representing that is the Hilbert space of quantum states on the system described by the phase space .
Or for the string, then the ground field is tmf and the tmf class
is the refined Witten genus, hence the partition function of the string.
What you are wondering is probably how these “categoriefied” or “homotopyfied” statements transgress back to just expresssions in complex numbers. This I don’t fully know yet. I understand the transgrssion to lower codimension completely for the pre-quantum data, but not yet properly after quantization. Thomas Nikolaus had presented a related result in Vienna: where topological T-duality traditionally gives an equivalence of D-brane charges in , one really expects this to be the transgression of an equivalence of classes in . He shows that this this is the case under some assumptions and conjectures that it is true generally. But this needs further investigation.
And the KU and tmf cases have an equivalent of the that you had in the Hilbert space case as an operator?
What you are wondering is probably how these “categoriefied” or “homotopyfied” statements transgress back to just expresssions in complex numbers.
Presumably at some point there must be scattering and absorption probabilities to calculate.
And the KU and tmf cases have an equivalent of the A that you had in the Hilbert space case as an operator?
Yes, sorry I had been a bit telegraphic. That operator is the “integral kernel”, the “” in section 4.5.
In the KU-example above, for the particle on the boundary of the 2d PCS theory, the role of is played by tensoring with the prequantum line bundle of the boundary theory. Traditional geometric quantizatin 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 is similarly played by tensoring with the Kalb-Ramond B-field 2-bundle.
Presumably at some point there must be scattering and absorption probabilities to calculate.
Yes, and that’s what I meant by transgression to codimension 0, which is where these scattering amplitudes appear (as discussed at S-matrix – formalization).
So what is currently described in the notes is, as highlighted in the second summary section, QFT extended down to the point but described only in three possibly high codimensions. This needs to be completed, eventually, clearly.
On the other hand there is already quite a bit of correlation function data appearing even in this higher codimension. Not the least for instance by AdS3-CFT2 we know that the spaces of states of the 3d CS theory compute “pre-correlators” (conformal blocks) of the WZW 2d CFT.
And for instance the value on the boundary of the Spin-Chern-Simons theory in the codimensions that we describe being the String orientation in tmf and hence on homotopy groups the Witten genus captures a correlation function of the string: the one on the torus without insertions, the partition function.
But this needs to be better understood in generality. Does every QFT have an extended quantization over a coefficient -ring whose elements itself encode the partition function of the theory?
I don’t know yet.
I wonder if there something Jordan algebra-like about collections of such higher operators.