Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I don’t know what’s up, but the page “Join of Simplicial Sets” seems to have been blanked by an anonymous user.
https://ncatlab.org/nlab/show/join+of+simplicial+sets
Is your plan to make use of HoTT to refine Ranta’s picture? I would have thought that would definitely be new.
Now on PhysicsForums-Insights: A first Idea of Quantum Field Theory.
The chapters will be appearing incrementally. The first one is at
In a strict sense, that’s right.
However, in a more relaxed sense, which is more typical of how mathematicians really work, it’s hard to see this as much of a problem. (I don’t claim you’re saying it is a big problem, just explaining our perspective.) Firstly, to what are you comparing a Globular proof - a handwritten proof? Clearly, neither are strictly formal, and the Globular proof has the advantage of being fully explicit. No proof (because proving it by hand is too complicated)? Then Globular wins by default. A HoTT proof in Coq? OK, then maybe HoTT wins, but as we’ve discussed before, there are not that many proofs well-suited to formalization in both Globular and Coq. (Consider the Perko knot isotopy proof, compared to a proof in Coq that uses any sort of non-algebraic structure like a universal property.)
Also, note that handcrafted proofs are often carried out in an informal semistrict style anyway! For example, see a lot of the work of Scott Carter and collaborators on knotted surfaces calculations, which are taking place in a braided monoidal bicategory; they don’t stop to worry too much about the definition of semistrict 4-category, they just let geometry guide them. The same is true for a lot of the Morse-theoretic calculations of people like Chris Douglas, Andre Henriques and Chris Schommer-Pries; for example, Andre Henriques has an explicit sphere eversion proof which takes place formally in a semistrict 6-category.
Also, I would expect that if an expert in some “trusted” definition of 4-category looks at the singularity structure that Globular is using, they would say, “yeah, those rules are in my definition of 4-category, implicitly or explicitly”. And I think often this would be such an easy process, a Globular proof would give them a very good sense of how to construct a proof using their definition. (Of course, it would be nice to talk to some experts (like you Mike!) and see if they agree.) Perhaps more likely would be that they have some proof already in their definition of 4-category, and not see how to write it as a Globular proof. So they might say “hey, your definition of semistrict 4-category is not general enough.” And maybe they would be right (although I don’t think so), time will tell.
Note that even if we had proved that every weak 4-category is equivalent to a semistrict 4-category by our definition, that would only take you half way to fully trusting the Globular formalization: you would also need to prove that the source code of Globular implements the definition correctly. This is far from straightforward; as you know, writing a proof assistant is far more complicated than just “typing in the definition of the logical system”. And Globular is written in Javascript, which does not lend itself to formal verification, to say the least.
(By the way, using Javascript made Globular quite easy (in a relative sense) to write and debug; I don’t think Globular would exist today if we’d tried to write it in a more traditional programming language for computational logic. And if we’d succeeded, you’d have to download some crummy installer to use it, rather than just click on a link in your browser; and it would only exist on some platforms; and nobody would use it. So for many good reasons, being very formal is quite low down our list of priorities at the moment.)
Look at what has been happening at derivator. The entry was erased and various things put there by an Anonymous Coward. Another one has reinstated the original one!! Has anyone noticed this? I was travelling about the time it happened so my usual check did not occur.
At triangle identities something similar had started. I have rolled back.
I added a new preprint of Kontsevich and Soibleman from few days ago at wall crossing and Donaldson-Thomas invariant. The web page of Aarhus lectures cited as the main website at wall crossing in Aarhus. Can somebody correct the link ?
In a collaborative work at Institute Ruđer Bošković in Zagreb, which will come out as a preprint soon, we are working on a certain noncommutative Hopf algebroid over a noncommutative base coming from Lie algebra theory. I gave a seminar talk about it in mathematics department in Zagreb and got a remark that our approach is too much coordinate based and that it would be desirable to have this work done using coordinate free approach. I came to a one month visit at l’IHÉS and soon realized that in dual language I can tell the story geometrically, though I still do not know how to prove some of the claims without algebraic coordinate-involving stuff which we had before.
So, a Hopf algebroid is made out of a left bialgebroid, right bialgebroid and an antipode map between them.The left and right bialgebroid have the same underlying algebra, but are different as bimodules and corings. I will leave the discussion of the antipode for another post and here sketch how I geometrically arrive at a left bialgebroid.
So let be a Lie group with Lie algebra which can be realized as , the Lie algebra of left invariant vector fields or the Lie algebra , the Lie algebra of right invariant vector fields; specialization of those vector fields at the unit element gives the isomorphism of vector spaces with the tangent space . The universal enveloping algebra can be realized also as the algebra of left invariant differential operators and as . Consider now the algebra of formal differential operators at . That means that you allow finite sums of partial derivatives to any finite order with coefficients which are formal functions, i.e. function supported on an infinitesimal neighborhood of unit element. The usual algebra of (global) differential operators (which contains and ) is naturally embedded in , hence it also contains and . furthermore the images of the left and right copy of the mutually commute, what is very important for our story.
Thus we have two maps of into , namely
Here is defined as extension from the vector fields as a homomorphism of associative algebras, while as antihomomorphism of associative algebras.
If we choose a basis in , i.e. we have a frame in , then we can consider two images in , that is a section of the frame bundle of the tangent bundle: every element of the basis goes into the corresponding left or right invariant vector field. Thus there are also two maps
corresponding to the frames by left and right invariant vector fields. Both maps are analytic and the image is the section of a principal -bundle, hence the difference is a matrix of analytic function on . Better to say, if is the translation map of the principal bundle then (for a frame fr) defines some invertible matrix of analytic functions on . Of course, by the functoriality, this translation matrix does not depend on the choice of frame. We can compute this matrix in a neighborhood of unit element, and I will explain some concrete formula in a later post.
To be continued…