You helped me so far - I’ll come back to it once I have the vocabulary to express a question. Urs.
]]>Nikolaj, I am not sure anymore what we are discussing. Could you try to restate what your question is? I think the points I mentioned above are self-evident, but you seem to be mixed up, and so maybe you are after something else than I thought you were.
]]>I know choice means the axiom of choice for the type but as HoTT sits on top of intuitionistic type theory, which as such proves choice (the Per-Martin Löf version I read the paper about) I don’t know what spoils choice on the types (which you welcome), so that losing it again would again spoil gauge theory :)
Regarding the second point, when you say there is no gauge theory you mean there is no gauge theory internal to the theory, right? Otherise I’d think you can do lots of type theory with topoi generally.
]]>I mean the axiom of choice. The higher toposes are needed because otherwise there are no s and hence no gauge theory.
]]>Thank you. Mhm, well I don’t quite get what “a type has choice” means yet, and I mostly view univalence as ’something on the outside is represented by something on the inside’ and don’t quite know -topoi necessarily need that for geometry … but I’ll keep my eyes open to connect the dots.
]]>First of all various classicality axioms will break the synthetic theory. If the 0-types have choice, then no non-trivial topological or smooth structure will be possible anymore. If univalence is broken or otherwise truncation to 0-types is enforced, then all synthetic gauge theory (all differential cohomology) disappears. This is the reason, incidentally, why cohesive -toposes behave very differently from cohesive 1-toposes. There is no comparable synthetic formalization of physics in cohesive 1-toposes.
]]>What are the first concepts one could add to a language like ITT or even HOTT, that would spoil rich semantics of the language in a smooth -topos. I.e. I ask what not to do, if one axiomizes a theory, if one wants to keep the possibility to do this kind of physics. In which way should the language not be restricted/overloaded?
]]>I asked my high school teacher how to tackle the integral and he just told me to shut up and watch this video.
]]>I am not a fan of the “shifted symplectic” terminology. But since it’s fashionable among people around me, I thought I’d take the opportunity to point out that, using different words, we have worked on this all along.
]]>Did you not say somewhere that you though the shifted symplectic language could be put better in other terms? Is that why shifted symplectic structure is rather slight?
]]>Tomorrow I’ll be speaking at MPI Bonn in the Higher Diff Geometry Semniar on
]]>As to counterfactual history on what classical physics could have made of spin fields,
If only they had listened to the Ausdehnungslehre, they could have made it.
]]>I thought I’d start a page then on stability of matter.
As to counterfactual history on what classical physics could have made of spin fields, that’s presumably a very difficult question.
]]>That quote by Bohr is a good example of the distinction that is necessary: the stability of the hydrogen atom is an effect not due to Pauli exclusion, but purely one of quantum ground states. It’s the stability of metals and Neutron stars that is governed by Pauli exclusion.
So it’s subtle. But I think the key point that you were after is true: classical spin fields could have been considered by classical physicists before quantum theory, and it would have revealed at least some effects that are usually attributed to quantum physics.
Odd thing to say given how they couldn’t even explain the most basic property of matter.
My impression is (I may be wrong) that they saw the existence of lumps of matter of various density as an a priori outside of physics. Much like these days we can’t explain the basic properties of fundamental particles, and it’s a heated debate whether physics has to explain these or has to just take them for granted.
]]>Thoughts about the stability of matter would make for an intriguing history.
Supposedly Niels Bohr said:
My starting point (for the development of the Bohr model) was not at all the idea that an atom is a small-scale planetary system and as such governed by the laws of astronomy. I never took things as literally as that. My starting point was rather the stability of matter, a pure miracle when considered from the standpoint of classical physics.
I wonder about the extent to which nineteenth century physicists were troubled by it. There was some sense of near completeness, such as Michelson in 1894:
… it seems probable that most of the grand underlying principles have been firmly established … An eminent physicist remarked that the future truths of physical science are to be looked for in the sixth place of decimals.
(There’s debate about whether this referred to Kelvin.) Odd thing to say given how they couldn’t even explain the most basic property of matter.
]]>Is it really only after quantization that supergeometry, in the guise of Pauli exclusion, can explain it?
That’s a good question. Pauli exclusion is there already for classical spin fields, due to their supergeometric nature. Whether this already gives stability of matter is maybe more subtle, as to have matter in the sense one needs here one needs bound states of fields (protons,neutrons, etc.) and it seems unlikely that this would exist classically. Though these bound states are a notorious subtle issue.
(Thanks to Igor Khavkine, who I had a quick exchange with regarding this question.)
]]>Can we return to that question of whether, with hindsight, the classical physicists of the nineteenth century glimpsed something of this prequantum physics? Put it another way if we could go back and give them your super-slick prequantum geometry, and they understood it, are there some phenomena they could now deal with?
Is there anything they could have done with supergeometry? Clearly a problem for almost all time was the stability of matter. Is it really only after quantization that supergeometry, in the guise of Pauli exclusion, can explain it?
]]>In the preprint, presumably Proposition 3.34, (1) should say rather than .
Ah, no, this is actually a on purpose. is the formal disk bundle of , but for general bundles over instead is the pullback of to the formal disk bundle of . Since that general thing does not seem to have been considered much, the text only mentions the special case that admits comparison to traditional literature.
Then in the slides, slide 6, the Eilenberg-Moore category shouldn’t mention : .
Thanks! Fixed now.
Is there a result along the lines that all of can be recovered as the kernel of for some ? If not, which part of ? And what of two Lagrangians that give the same EL-equations?
That’s exactly the question that Helmholtz asked and answered, way back. The modern incarnation of his result is the Euler-Lagrange complex. Its local exactness says that a PDE given by vanishing of a vertical form is locally variational, hence is locally of the form , precisely if the “Helmholtz form” vanishes.
]]>In the preprint, presumably Proposition 3.34, (1) should say rather than .
Then in the slides, slide 6, the Eilenberg-Moore category shouldn’t mention : .
Is there a result along the lines that all of can be recovered as the kernel of for some ? If not, which part of ? And what of two Lagrangians that give the same EL-equations?
]]>Thanks! Fixed now.
As you may have seen already, I also have talk slides now (pdf).
]]>Typos:
“Regarding such for a moment … we may apply the de Rham differential to it.” (p. 6)
and
(p.7)
and
]]>field theoried
Did you leave any notes anywhere on this issue?
You and David R. left a small trail on the nForum here in discussion with Frédéric Paugam.
]]>I don’t think I did. I was semi planning to write a paper on this with Ray Vozzo, to get the connection version at least over (or even , since we wanted to be quite explicit!)), but I’m not sure we have enough to go on.
]]>@David Roberts,
ah, true, thanks for reminding me, that’s embarrassing for me. Did you leave any notes anywhere on this issue?
I am too busy right this moment with getting something else out of the way, but I do want to get back to the complex analytic story, for various reasons. Thanks to you and David C. for prodding me.
@David Corfield,
thanks! Fixed now.
]]>