Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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…
I have this information from Vladimir Guletskii. Maybe somebody could post/advertise it on nCafe as well. The deadlines are really soon so it is an urgent information.
The Department of Mathematical Sciences of the University of Liverpool has one EPSRC DTG studentship award for research leading to a PhD starting on 1 October 2012. Dr Jon Woolf proposes the following PhD research programme for this vacancy to work under his supervision:
Directed homotopy theory and (infinity,1)-categories
Directed homotopy theory studies spaces equipped with some notion of direction or ordering of points; there are several variants but the most relevant one for this project is locally pre-ordered spaces. These are spaces such that the points of each open subset are pre-ordered (suitably compatibly with the topology, and with the other local pre-orders). There are many natural examples: stratified spaces (points in higher codimension strata are deeper), space-time (ordered by causality), geometric simplices (points have the same ‘level’ as the highest vertex in the closure of the face in which they lie), and more generally geometric realisations of simplicial sets.
The initial aim of this project is to study an analogue of Grothendieck’s homotopy hypothesis
‘homotopy-types are infinity-groupoids, i.e. (infinity,0)-categories’;
namely that ‘directed homotopy types are (infinity,1)-categories’.
(Here, by a directed homotopy type we mean a directed space up to equivalence under an undirected notion of homotopy. Working with directed homotopies is also interesting, but leads to a different theory.) To be more precise, the aim is to set up a model structure on the category of locally pre-ordered spaces which is Quillen equivalent, via directed analogues of the singular simplicial set and geometric realisation functors, to the Joyal model structure on simplicial sets. The fibrant objects of the latter are precisely the quasi-categories, i.e. the simplicial models of (infinity,1)-categories.
The conjectural model structure on locally pre-ordered spaces should have a close connection with well-studied notions in the homotopy theory of stratified spaces (and from this it would derive much of its interest). In particular, the fibrant objects should include Quinn’s homotopically stratified sets, and for these weak equivalence should specialise to stratum-preserving homotopy equivalence.
The Initial applications (CV and Personal Statement on Research) can be emailed to [email protected]
Vladimir Guletskii is asking me to post the links
http://www.liv.ac.uk/working/job_vacancies/studentships/EPSRC_PhD_Studentshi.htm
http://www.jobs.ac.uk/job/ADL026/epsrc-phd-studentship
http://homotopical.wordpress.com/2011/10/26/phd-position-in-motivic-homotopy-theory
on a PhD vacancy i motive algebraic geometry at Liverpool. Categorification and stable model categories (with tensor products) are very relevant for the project. One might also want to compare ideas about noncommutative motives which are, according to Volodya, also relevant.
He adds:
There is some difference between the overseas fees and the home fees, but (a) citizens of EU do not have to pay it, and (b) our department here can sort out the difference between fees anyway.
Volodya also calls our attention to the closeness of some relevant content to ideas in John’s presentation
Anyone’s who’s been caught by the IP check will know that it’s quite annoying. There are a few possibilities as to how to make it possible for genuine editors to circumvent it. The simplest, and so the one we’re trying first, is simply to turn it off.
In the last two weeks, on average it’s been activated once a day. That gives us a baseline against which we can compare the next two weeks.
To be clear, it hasn’t quite been turned off. It’s simply been disengaged. So it still does the check, but (if I’ve done it right), the check doesn’t actually do anything other than log its results. So by comparing the logs with the old logs, and by seeing how many genuine edits would have been blocked, we can get an estimate of how effective it’s been versus how annoying it’s been.
If we discover that the spam content has increased significantly then we can turn it back on. If we also discover that the number of genuine edits that would have been blocked is similarly high, then we can figure out another way around it. So even if it turns out to be a bad idea, it will still garner us useful data on how much of a problem it is.
To be absolutely clear: this is the block that checks your IP address to see if it’s on the “naughty list”. It is not the spam filter that checks that you aren’t using any Bad Words (such as evil). That filter is doing sterling work and is not under consideration (for comparison, the spam filter has been activated about 15 times a day over the last two weeks).
So, if you’ve been getting blocked by the IP, or know that you do from a particular computer, you should now be able to edit freely (and please inform us here of your success or failure). Also, please be a little extra vigilant about possible spam (and remember to flag it “Possible Spam” or something like that when reporting it here).
I am interested for many years in using localizations (typically having fully faithful right adjoint) as replacements for open sets in noncommutative algebraic geometry. There are some interesting Čech-like cohomologies lurking there as well (for abelian case known for about 20 years, for nonabelian wait for another paper of mine).
Now I am trying to do, with some ideas from correspondence with colleagues some more new cases, some of which to my surprise are not known. In particular there is lots of issues about descent for functors where both the domain and codomain categories are given by covers by localizations, that is families of localizations such that the induced inverse image functor to the product of the localizations is comonadic. Before tackling that case properly, I am trying to fix some holes in my understanding of the case of endofunctors.
A localization having fully faithful right adjoint is equivalent to a Eilenberg-Moore category over an idempotent monad. For any localization functor, there is a notion of localization compatible endofunctor, which Lunts and Rosenberg introduced in unpublished but available Max Planck Preprint in 1996, in order to study the differential operators on geometries given by “categories of quasicoherent sheaves”. Their notion of compatibility does not involve coherences, and I prefer to work with coherences. I have shown that the coherences actually follow, if one takes for compatibility a distributive law between the idempotent monad and the endofunctor , of the form . More precise statement is at distributive law for idempotent monad (zoranskoda) (cf. also new entry compatible localization with some background references, some on different notions of compatibilities).
The compatibility which is a property in Lunts-Rosenberg becomes a distributive law in my work, what is in general a structure; but a (seamingly new) theorem says that the coherent version is also just a property, namely the distributive law is unique when it exists (“strict compatibility” Edit: It seems to me that the existence of a distributive law is a bit stronger than Lunts-Rosenberg compatibility.) The law is then also invertible what means that its inverse is the other type distributive law . But what I don’t know is if every other type distributive law for an idempotent monad is invertible and hence coming from the inverse of a unique distributive law or there are genuine non-invertible counterexamples ? Any ideas ?
to my surprise I notice that with current nominal count of 3930 nLab entries we are quite close to number 4001. So maybe, to establish a tradition we might want to post a followup to 3000 and One Things to Think About but in the style of David Corfield’s nLab Digest last time (see there to get an impression for what I mean).
So, I invite everyone to post here within the next weeks a little blurb in this style, if desired, which we can then all collect together into a blog post.