MathOverflow question seeking answer, offering bounty

Last year I asked a question titled Direct comparison zig-zag between cochain theories on MathOverflow, and it has still no good answer. I’ve offered a bounty, and no takers yet. The satisfaction is yours for the taking! To quote from the end of the question:

…my hope is to show that the class of cochain theories is connected, assuming one exists, and then exhibit one. This may well be singular cohomology, or it might be something else. In particular I want to remove from the proof of uniqueness the privileged position that any one construction has. The only caveat is that I won’t be able to use any super-sophisticated machinery as this is a first course in algebraic topology. I’m happy to have an outline of how to unwind a sophisticated proof.

Teaching Algebraic Topology at the Australian Mathematical Sciences Institute Summer School

I’m pleased to finally announce that I’m teaching an Algebraic Topology course for the 2021 AMSI summer school in January and February! It will be an adaptation of the course I taught last year, omitting the material on covering spaces and fundamental groups. Instead, I aim to cover simplicial sets as well as -sets, and cover the Eilenberg–Steenrod material in more detail.

More excitingly, I aim to stream the lectures on Twitch. I haven’t set all this up yet, but I will hopefully be practicing streaming some of my own work process, maybe even developing some of the course notes, before January.

Want to see the real secrets of set theory in YouTube format?

tl;dr Set theorist Asaf Karagila is looking for YouTubers to collaborate.

My colleague and sometime rival Asaf is a top notch young set theorist who works a lot on pushing the frontier of the method of forcing. At one point we were in competition to construct, without using large cardinal assumptions, the first model of set theory where the axiom WISC failed. Asaf won, but as I was working in a different formalism, I still had the satisfaction of arriving at my own solution. This was right at the start of his academic career, and he’s only gone from strength to strength, recently being awarded a prestigious UK Future Leaders Fellowship.

The upshot is, he included explicitly in his Fellowship application that he would produce outreach videos about set theory, and is looking to collaborate with YouTubers with wide reach to achieve this. As he writes:

“There is a clear lack of good videos addressing set theoretic ideas, which I honestly believe that I can make at least somewhat accessible. And hopefully this will make set theory more accessible to the public, or at the very least, to other people interested in mathematics.”

He has set up a contact email if you are a YouTuber:

At the moment I’ve set up an email address, youtube2020@karagila.org, where you can email me. Let me know about your channel, what kind of content you want to make, etc. I cannot make any promises about money, but I’m always happy to advise with regards to content, should the need ever arise.

And if you are not a YouTuber, but want to see some more nitty gritty about what it is that set theorists do nowadays, point them to Asaf’s blog post! Asaf tells me that Numberphile and Tibees have already made contact, but if you are super keen to support the idea, it would help if viewers promoted the idea.

Now, if YouTubers want to make videos about category theory, on the other hand, then, ahem, I don’t mind having a chat 🙂 But they should talk to Asaf first, I don’t want to intercept his efforts!

MathOverflow links in referee reports

Just a public service announcement: if you are using a MathOverflow “share” link in your referee report, remember that the URL includes your user number, and whoever has that link can tell who put it in your report. If you wish to preserve your anonymity, remove that number after the last slash!

Initiality conjecture for full Martin-Löf type theory

Next Thursday, 10th September, Guillaume Brunerie and Peter LeFanu Lumsdaine are going to present a talk Initiality for Martin-Löf type theory in the HoTT electronic seminar … with a proof of the initiality conjecture!

Here’s the abstract:

“Initiality” is the principle that the term model of some type theory should be an initial object in the category of models of that type theory.  Thomas Streicher gave a careful proof of initiality for the Calculus of Constructions in 1991.  Since then, initiality for more complex type theories (such as Martin-Löf type theory) has often been treated as established, as a straightforward extension of Streicher’s result, but never written up carefully for a larger theory.
Around 2010, various researchers (notably Voevodsky) raised the question of whether these extensions really were sufficiently straightforward to consider them established without further proof.  Since then, views on the status of initiality have varied within the field; but the issue has been, at least, a frustrating unresolved point.
In this talk, we present a proof of initiality for a full-featured Martin-Löf type theory.  The proof is formalised in Agda, to dispel any question of thoroughness (and also partly formalised in Coq), and is carefully designed for extensibility to other type theories.  The proof is based on Streicher’s, using some improvements of Hofmann and further refinements by the present authors.  The two formalisations present slightly different versions of the statement — using contextual categories in Agda, categories with attributes in Coq — but the core of the proof is parallel.

Joint work with Menno de Boer and Anders Mörtberg.

This was a big concern of Vladimir Voevodsky and it’s good to finally have it sorted out, with a formalised proof, as it should have.

Unfortunately it’s live at 1am, so I’ll have to grab the recording…

She is asking the right questions

@gracie.ham

this video makes sense in my head but like WHY DID WE CREATE THIS STUFF

♬ original sound – gracie.ham

Gracie, I can’t reach out to you online, but this is my response as a mathematician. I hope it helps someone.

These kinds of questions you are asking are what drive us as a profession. It doesn’t matter if your example is Pythagoras or whoever. At some point, for every piece of mathematics that we know, someone asked “how?”, or “why?”, or “why not?” and then just let the ideas take them where they would. Literally some of the things that make a stack of technology work came from someone saying “what happens in 3d instead of in 2d?” and then he ended up graffitiing the answer on a bridge when he finally figured it out. No one asked him that question, he asked it himself. No one told him the answer either. It took some hard work, he tried a lot of things, he failed a lot, but he persisted. People had arguments for decades over whether that was the right way to do it. This was 150 years ago. Today I’m pretty sure most 3d animations you see today use that little idea. But he just wanted to know “why?” He wanted to know “can I do it?”

Sometimes it was people just thinking about walking around a town and across bridges. Sometimes it was a fun puzzle. Sometimes it was bets and duels. Sometimes it was a guy who did maths in prison. Sometimes it was a girl who did maths at night when her parents didn’t know and didn’t want her to. But everything we know in maths started with someone asking “why is it like this?”

Please keep asking “how?” and don’t take any nonsense when people don’t realise they don’t know either and never even thought about it.

(Via Jordan Ellenberg via David Butler on Twitter.)

Another good maths journal, this time in analysis

Just as Tim Gowers and co. started the free-to-read and free-to-published journals Discrete Analysis and Advances in Combinatorics, the same platform (Scholastica) has now been used to introduce another such journal: Ars Inveniendi Analytica. Its focus is analysis, and I hope it attracts some big names quickly, to establish its street cred. To quote from the linked annoucement post:

The title of this new journal refers to the term ars inveniendi, coined by Leibnitz to identify the art of discovering new mathematical statements, methods and arguments. This reference aims at highlighting a blooming time for exciting mathematical discoveries in the field of Analysis, and at celebrating the creativity of researchers.

We hope that this editorial enterprise, undertaken in full service of our community, will add up to similar efforts and will encourage the launch of similar operations. Scholars need not only new lines of investigation and new methodologies, but also new and reliable forms for communicating their work. Creating top quality journals, founded and managed by academics, freely accessible to authors and readers, and with minimal management costs entirely sustainable by academic institutions, is the main constructive step that scientist can take to help shaping the future landscape of scientific publishing into something that is more true to the spirit of scientific discovery.

(Apologies if the formatting of this post is weird, I need to get used to the new WordPress online editor.)

Solving restricted quadratic equations for natural number solutions is NP-complete

TIL the following amazing result, due to Kenneth L. Manders and Leonard Adleman:

Theorem: The following problem is NP-complete: given natural numbers expressed in binary, determine whether has a solution in natural numbers.

The original paper gave a slightly different form, the version above is given in this lovely paper of Jeřábek.

Translations of technical words and phrases into French

(UPDATED, SEE AT BOTTOM OF PAGE) With our recent accepted paper, we need to supply a French translation of the title (done), abstract (kinda, with help from DeepL) and the key words. This last one is where I would like any suggestions from francophone mathematicians.

Here’s the list of key words/phrases we need translations of: Whitney extension theorem, smooth functions on closed domain, Whitney jet, polynomial cusps, Fréchet space, submersion, manifolds with corners, manifolds with rough boundary, manifold of mappings, exponential law.

Also, for amusement purposes, here’s the DeepL+ε translation of the abstract:

Cet article examine une version globale et non linéaire du problème de l’extension Whitney pour les fonctions lisses à valeur variété sur des domaines fermés , avec une frontière non lisse, dans des variétés éventuellement non compacts.
En supposant que est une sous-variété avec des sommets, ou est localement convexe avec une frontière rugueuse et compacte, nous prouvons que la carte de restriction des fonctions définies partout est une submersion de multiples localement convexes et admet donc des clivages linéaires locaux sur les cartes.
Pour ce faire, nous considérons la carte de restriction correspondante pour les espaces localement convexes de sections de faisceaux de vecteurs à support compact, nous autorisons le cas encore plus général où ne présente que des restrictions légères sur les cuspides intérieures et extérieures, et nous prouvons l’existence d’un opérateur d’extension.

I have fixed a few things, like using variété for ‘manifold’, rather than the vernacular translation. I would be grateful for suggestions on how to improve it. The original English text is as follows

This article considers a global, nonlinear version of the Whitney extension problem for manifold-valued smooth functions on closed domains , with non-smooth boundary, in possibly non-compact manifolds.
Assuming is a submanifold with corners, or is locally convex with rough boundary and compact, we prove that the restriction map from everywhere-defined functions is a submersion of locally convex manifolds and so admits local linear splittings on charts.
This is achieved by considering the corresponding restriction map for locally convex spaces of compactly-supported sections of vector bundles, allowing the even more general case where only has mild restrictions on inward and outward cusps, and proving the existence of an extension operator.

---

I’ve had a bit of feedback from various people who know some French and who know how to Google for advice (though no actual French mathematicians—where are you all?), and here’s an updated version:

Nous considérons une version du problème de l’extension Whitney, globale et non linéaire, pour les fonctions lisses à valeur de variétés et définies sur des domaines fermés à bords non-lisses dans des variétés probablement non compactes.
Supposons que est une sous-variété à bord anguleux, ou elle est compacte et localement convexe à bords non-lisses, nous montrons que l’application de restriction, à partir des fonctions définies partout, est une submersion de variétés localement convexes, et donc permet des scindage linéaires locaux sur les cartes.
Nous considérons à cet effet l’application de restriction correspondante pour les espaces localement convexes de sections de fibrés vectoriels à support compactes, permettant aussi le cas plus général où n’a que des restrictions légères sur les cuspides vers l’intérieur et l’extérieur, et montrons l’existence d’un opérateur de prolongement.

And here’s our list of key words:

théorème de l’extension de Whitney, fonctions lisses sur des domaines fermés, jet de Whitney, cuspides polynomiales, espace de Fréchet, submersion, variétés à bord anguleux, variétés à bords non-lisses, variétés d’applications, loi de l’exponentielle

Happy to get more comments!

I feel accepted

Now, after multiple rejections and two and a half years of doing the rounds of journals, my joint paper Extending Whitney’s extension theorem: nonlinear function spaces with Alexander Schmeding (arXiv:1801.04126) has been accepted to appear in the Annales de l’Institut Fourier. I wrote a little bit about something from it here. This paper provides the proof that is needed for another joint paper of mine (this one with Raymond Vozzo), on mapping stacks of differentiable stacks (the title just mentions orbifolds, but it works for any differentiable stack as codomain).