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


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.)

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 C, avec une frontière non lisse, dans des variétés éventuellement non compacts.
En supposant que C 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ù C 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 C, with non-smooth boundary, in possibly non-compact manifolds.
Assuming C 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 C 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 C à bords non-lisses dans des variétés probablement non compactes.
Supposons que C 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ù C 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).

Small observations on fields in Lean

This started out at a comment on Kevin Buzzard’s recent blog post on division by zero in Lean, but I got caught up in my own thoughts, and was turning into one of those “I have a question but it’s more of a mini-talk about my own ideas” non-questions at seminars. So I moved it here.

The background is this: in the proof assistant Lean, fields are defined so that inverse is an everywhere-defined function, with the inverse of zero being zero. Kevin points out that this doesn’t actually change anything, since the axioms on fields explicitly demand that you can only get a\cdot a^{-1} = 1 if you know a \neq 0. In Lean, this means you have to supply a proof that this is the case. So one cannot abuse 0^{-1}=0 in incorrect proofs that would use actual division by zero. There is no mathematical difference between defining inversion as a total function, and only defining axioms in ‘guarded’ situations, and only defining inversion as a partial function. The fact that 0^{-1}:=0 is, from a programming point of view, fairly arbitrary; the output (i.e. the right hand side of the :=) could be any “junk” value. In other languages one might specify it to be ‘NaN', and have rules about how that interacts via addition and multiplication.

Continue reading “Small observations on fields in Lean”

Thank you, kind referee! :-)

Got a referee report back on a paper that took a long time to get right, but which I thought for a long time wasn’t worth even submitting for publication. My favourite remark from the report:

The proofs are clear and easy to follow, but the end results are non-trivial, and with clear applications.

There has been online discussion recently, which I have glimpsed but not followed in-depth, on who we as mathematicians write papers for. The stereotype of a genius mathematician whose papers are inscrutable to all but those on the inside circle who have access to the great man is not one that I find appealing. Yes, mathematics has prerequisites on knowledge, but it can also make sense when explained well. I am flattered that my proofs, which I struggled to write in an elementary way as possible, are seen by at least one person as clear, while also appreciating the scope of the theorem. There are of course things to fix and further clarify, and so this is refereeing at its best: seeing the worth of a paper (I am clearly no great judge of my own work), but finding ways to improve and suggest extra useful context. The scrutiny was very close, to the point of identifying an object that was written in a canonically isomorphic form, and in context, this was not correct. Had this paper been rejected from the journal, but I had gotten the same report, the blow would have been very much softened. So I repeat: thank you, kind referee!

Two recent research theses from my department

One is in complex analytic geometry, and the other is in number theory, with a dash of differential geometry. I had the pleasure of seeing both Haripriya and Ben develop from their first forays into research to producing two excellent theses, both of which won a commendation.

Abstract: Let M be an open Riemann surface. A recent result due to Forstnerič and Lárusson [8] says that, for a closed conical subvariety A \subset \mathbb{C}^n such that A \setminus \{0\} is an Oka manifold, the weak homotopy type of the space of non-degenerate holomorphic A-immersions of M into \mathbb{C}^n is the same as that of the space of holomorphic (or equivalently, continuous) maps from M into A\setminus \{0\}. In their paper, the authors sketch the proof of this theorem through claiming analogy with a related result, and invoking advanced results from complex and differential geometry, including seminal theorems from Oka theory. The work contained in this thesis was motivated by the absence of a self-contained proof for the special case where A = \mathbb{C} – as, perhaps, the first geometrically interesting case that one would consider. We remedy the absence by providing a fully detailed, self-contained proof of this case; namely, the parametric h-principle for holomorphic immersions of open Riemann surfaces into \mathbb{C}. We outline this more precisely as follows. Take a holomorphic 1-form \theta on M which vanishes nowhere. We denote by \mathcal{I}(M, \mathbb{C}) the space of holomorphic immersions of M into \mathbb{C}, and denote by \mathcal{O}(M, \mathbb{C}^*) the space of nonvanishing holomorphic functions on M. We prove, in all detail, that the continuous map

\mathcal{I}(M, \mathbb{C}) \to \mathcal{O}(M, \mathbb{C}^*), f \mapsto df/\theta,

is a weak homotopy equivalence. This gives a full description of the weak homotopy type of \mathcal{I}(M, \mathbb{C}), as the target space \mathcal{O}(M, \mathbb{C}^*) is known by algebraic topology (Remark 5.2.3).

Abstract: We present some results related to the areas of theta functions, modular forms, Gauss sums and reciprocity. After a review of background material, we recount the elementary theory of modular forms on congruence subgroups and provide a proof of the transformation law for Jacobi’s theta function using special values of zeta functions. We present a new proof, obtained during work with Michael Eastwood, of Jacobi’s theorem that every integer is a sum of four squares. Our proof is based on theta functions but emphasises the geometry of the thrice-punctured sphere.

Next, we detail some investigations into quadratic Gauss sums. We include a new proof of the Landsberg–Schaar relation by elementary methods, together with a second based on evaluations of Gauss sums. We give elementary proofs of generalised and twisted Landsberg–Schaar relations, and use these results to answer a research problem posed by Berndt, Evans and Williams. We conclude by proving some sextic and octic local analogues of the Landsberg–Schaar relation.

Finally, we give yet another proof of the Landsberg–Schaar relation based on the relationship between Mellin transforms and asymptotic expansions. This proof makes clear the relationship between the Landsberg–Schaar relation and the existence of a metaplectic Eisenstein series with certain properties. We note that one may promote this correspondence to the setting of number fields, and furthermore, that the higher theta functions constructed by Banks, Bump and Lieman are ideal candidates for future investigations of such correspondences.