## Equality part 3: canonical isomorphism.

I hadn’t planned on writing a third equality post, but my talk at Big Proof 2019 (see slides here) ended up having a huge section about “mathematician’s equality”, and I realised I had more to say about it. Here are some more detailed thoughts about the issue.

## Examples of canonical isomorphisms.

Canonical isomorphism is a magic kind of equality, apparently accessible to mathematicians who are “thinking about things in the right way”. It has several definitions; it has no definition. However, we know it when we see it, we are almost universally in agreement on the notion, and hence we don’t seem to really challenge each other on it. The isomorphism between a finite dimensional vector space and its double dual is canonical — we all know that. The class field theory isomorphism is canonical (at least up to sign) — we know that too. Even the Langlands correspondence is supposed to be canonical — it is for that reason that we believe in the Langlands group. On a more mundane note, $R[1/fg]$ is canonically isomorphic to $R[1/f][1/g]$. Do we even stop to think what these things mean? Formalisation has forced me to think about one of these, and it led me to a surprising conclusion.

Wikipedia defines a canonical map as — well, why don’t you just take a look. There is no formal definition there at all. The page is tagged with the “mathematical terminology” tag but one could argue that this is stretching the point, unless you regard “the map which preserves the widest amount of structure” or “conventionally agreed upon to be the most useful for further analysis” to have some sort of mathematical meaning.

But what am I saying here? Is there no space in mathematics for guiding principles, and not-completely-formed ideas about how things should fit together? Can we not experiment with concepts and worry about dotting the i’s and crossing the t’s later? Of course we can do these things! That is exactly the art of mathematics! In fact, it’s more than just allowed — it is essential that mathematicians are allowed to be creative, and come up with brilliant ideas of maps between apparently unrelated objects such as Galois representations and automorphic representations, and then suggest that these constructions are in some way canonical and begin to find out exactly what other observations such an idea might lead us to. This way of thinking is essential for mathematics to proceed.

One thing I understood recently is that there are two independent subtleties here, so in this post I will separate them out. The first is well-known, the second I think less so.

## Issue 1: Mission creep.

The first issue is the many contexts where the word “canonical” is used. Sometimes people use it in a situation where it can be easily rigorously formalised. In category theory there is a perfectly rigorous definition of a natural isomorphism. For example, in the category of finite dimensional complex vector spaces, we could consider the functor sending a vector space $V$ to itself, and we could consider a second functor sending a vector space $V$ to its double dual. There is a natural isomorphism between these two functors, sending a vector space to its double dual. One can look up the definition of natural isomorphism on Wikipedia; it is the statement that a precise collection of diagrams all commute. People say that the obvious map from a vector space to its double dual is “canonical” but they could instead say that it is a natural transformation. Another example would be where two objects both satisfy a certain universal property. Then a piece of abstract nonsense proves that there are are unique isomorphisms in both directions between these two objects, again both making a bunch of diagrams commute. Again a mathematician might say that isomorphisms arising in this way are “canonical”, and again there is an equivalent category-theoretic language which they could use instead to say precisely what they mean.

However there are times in mathematics where the word is being used beyond this remit. Some number theorists would say that the isomorphisms of global class field theory are “canonical”. This is, I believe, a different usage of the word. There might not be some formal category-theoretic framework which one can hide behind here (although people attempting to categorify the Langlands program might well believe that such a framework exists). What is going on here is that Artin made some construction, an isomorphism between two abelian groups attached to a number field (one using adeles and one using Galois groups), and this map he constructed obeyed a nice long list of properties which have been explicitly written down (for example the behaviour of the map when you change from one field to a finite extension), and it is not hard to show that that there can be at most one construction with these properties. Such a construction does exist (a hard theorem), and this construction then gets the name “canonical”, which here seems to be a specialised and different use of the word. Note however that Artin’s construction gives an isomorphism between two abelian groups, and one can compose this isomorphism with the map sending an element of an abelian group to its inverse, giving us a second canonical isomorphism between these two groups, which satisfies a similar-but-not-exactly-the-same nice long list of properties, arguably indistinguishable from the first list in the sense that it is not clear (at least to me) which list is “better”. However the two lists are distinguishable in the sense that they are different, and can be told apart. In this situation it is hence difficult to say which of the constructions is the “most canonical”. The constructions have got different names, and both are used in the literature. One is called “class field theory normalised the classical way, sending uniformisers to arithmetic Frobenii” and the other is called “class field theory normalised the Deligne/Langlands/Carayol way, sending uniformisers to geometric Frobenii”. A geometric Frobenius is simply the inverse of an arithmetic Frobenius. This example is quite jarring, read within the context of Wikipedia’s definition of a canonical map at least, because both maps are useful (the classical normalisation when doing concrete things like Heegner points, the more modern normalisation when doing the cohomology of Shimura varieties), and there is no particular agreement within the number theory community as to which choice is “best” — it simply depends on what you are doing.

Andre Weil once jokingly wrote “I can assure you, at any rate, that my intentions are honourable and my results invariant, probably canonical, perhaps even functorial”, perhaps parodying the usage of the word in mathematics at that time (the 1950s). I think this sums up rather well the way the word is sometimes used nowadays.

## Issue 2: canonicality beyond the universal property.

There is however a second issue, which I began thinking about when preparing my Big Proof talk, and this is when mathematicians see an isomorphism which is “canonical” in a sense which can definitely be made completely precise, and then decides that the isomorphism is so completely canonically canonical that it will not cause any problem to simply use the notation $=$ for it. J. S. Milne, in his book “Etale cohomology“, even explains in his notational conventions that canonical isomorphisms will be denoted by $=$. [What, all of them? Even the two distinct canonical isomorphisms of class field theory? It is not hard to come up with a very plausible-looking proof that $x=x^{-1}$ for $x$ in the abelianisation of the absolute Galois group of the rationals using this convention; of course, this is not what Milne means to say (although it would be interesting to hear his definition of “canonical” in this context, if indeed he had one)]. Milne is of course a professional mathematician who knows what he is talking about, and so uses this convention sensibly. He is not the only one. Even Grothendieck adopts this convention in EGA (EGA I, section 1.3.3), although he does not seem to be so explicit about it. The context here is that if $R$ is a ring, and $f$ and $g$ are two elements of $R$ with the property that a prime ideal of $R$ contains $f$ if and only if it contains $g$ (for example we could have $g=f^2$ or $g^3=f^2$), then one can check that there are unique $R$-algebra isomorphisms $R[1/f]\to R[1/g]$ and $R[1/g]\to R[1/f]$ whose composite in both directions is the identity. Grothendieck himself uses the French word “canoniquement” in the link above when talking about this identification, and five lines later is using $=$ as its notation, when claiming $M_f = M_g$, a claim of the same nature as the claim $R[1/f] = R[1/g]$. If $R$ is an integral domain then one can build $R[1/f]$ and $R[1/g]$ as explicit subsets of the field of fractions of $R$ and then they really are equal subsets. However in the general case one does not have this luxury. What does it even mean to say $R[1/f]=R[1/g]$? Grothendieck explicitly wrote $M_f = M_g$. What does this even mean? They are not equal in the formal sense at all, as we are about to see — but they are most definitely canonically isomorphic — any mathematician who knows the area would tell you that.

This is a serious issue for formalisers. This notion of equality here is most definitely not definitional equality or syntactic equality. In dependent type theory one could attempt to interpret it an equality of two types, however in this context it is not really reasonable to argue that the types are equal. Anyone who has seen the usual construction of $R[1/f]$ knows that it is equivalence classes of pairs $(r,n)$ with $r\in R$ and $n\in\mathbb{Z}_{\geq0}$, where $(r,n)$ is initially interpreted informally as $r/f^n$, even though at this point these symbols make no sense. The equivalence relation is then defined, informed via this interpretation, and then the informal interpretation is forgotten about, and a ring structure is put on the equivalence classes. The ring $R[1/f]$ is proved to have a universal property, namely that any ring homomorphism $R\to A$ sending $f$ to a unit extends uniquely to an $R$-algebra homomorphism $R[1/f]\to A$ (did I mention that all rings are commutative and have a 1, and all morphisms send 1 to 1?). This is the universal property. In this optic, the two equivalence relations on $R\times\mathbb{Z}_{\geq0}$ really are not equal in general, and it’s quite messy writing down the canonical map on equivalence classes here; it’s much easier to prove a theorem once and for all saying that $g$ is invertible in $R[1/f]$ and vice versa, and then we can use the universal property to define the maps which give us the canonical isomorphisms.

Here is my objection to this usage. The moment two mathematical objects are equal, it is apparently possible to replace one by the other in any argument whatsoever, without giving any justification. Here is an explicit example, which bit me hard a year or so ago. It is a standard argument in basic graduate level algebraic geometry which I have now read many treatments of, and I am not really satisfied with any of them. For simplicity, I will talk about the treatment in the stacks project, because it is the easiest to cite. In tag 01HR, it says (a little before definition 25.5.3) “Thus we may apply Algebra, Lemma 10.23.1 to the module $M_f$ over $R_f$ and the elements $g_1, g_2, \ldots, g_n$”. But actually this is not strictly speaking possible, from a formalist perspective. Bear with me here, this is not a picky pedantic point, there is a little more to it than that. The lemma being cited is in tag 00EK, which is some statement about an exact sequence of modules. There are unfortunately two modules $M$ here, one in 01HR and one in 00EK, and they’re not the same. For simplicity let’s assume that $M=R$ in 01HR, which then means that $M=R[1/f]$ in 00EK. To make things even simpler, let’s assume that the elements $f_i\in R[1/f]$ are actually elements of $R$, and let’s call them $g_i$ to coincide with the notation in 01HR, so $D(g_i)\subseteq D(f)$ using the usual notation for open sets attached to elements of $R$. Even with these simplifications, there is still a subtle, almost invisible, problem, which formalisation is about to show us.

The problem is now that 00EK is a statement about an exact sequence relating $R[1/f]$, $R[1/f][1/g_i]$ and $R[1/f][1/g_ig_j]$. We now want to apply this to prove a result relating $R[1/f]$, $R[1/g_i]$ and $R[1/g_ig_j]$. Now because of the assumptions we know that $R[1/f][1/g_i]$ and $R[1/g_i]$ are canonically isomorphic. If we now just assume that they are equal, and we furthermore just assume that the maps $R[1/g_i]\to R[1/g_ig_j]$ are equal to the maps $R[1/f][1/g_i]\to R[1/f][1/g_ig_j]$ (i.e. the diagrams all commute), then there is no problem at all! This is precisely what the stacks project is doing, it is what Grothendieck does in EGA, it is what Hartshorne does, it is what everyone does.

The authors here are smart people, so let’s step back and just check that their intuition is correct. Of course, any one of these authors, when challenged, will say that they know that $R[1/f][1/g_i]$ is not literally equal to $R[1/g_i]$, however both maps satisfy the same universal property, and so they are canonically isomorphic. So now we have a diagram — a sequence we’ve shown to be exact, and a sequence of canonically isomorphic objects which we want to show is exact. So now we draw in all the canonical isomorphisms and now we just have to prove that all the resulting squares commute. But all the isomorphisms are natural, coming from a universal property, so all the diagrams will commute because of this, and everything will work out fine. Right?

But guess what — the map $\beta$ in 00EK is not a morphism of rings. It cannot be defined via the universal property directly. The universal property really does not tell us immediately that the diagram commutes! We are kind of cheating here; there is a diagram, we can’t see it because of this trick of using $=$ to mean an isomorphism, the isomorphism is natural, but the naturality does not immediately imply that the diagram we need to commute, commutes. We have slightly over-stepped the mark. We need two applications of the universal property and then we need to take their difference and observe something of the following form: if two squares involving four abelian groups commute, and the vertical maps are the same in each square, then subtracting the horizontal maps gives rise to a a third diagram which also commutes. There is some little missing argument here. I never spotted this argument until I tried to formalise it. Once I’d realised that from a formalist point of view 00EK was actually too weak to use in 01HR, I had to then prove a bunch of lemmas showing that 00EK (whose proof was a lot of work, done by Chris Hughes) plus a horrible diagram chase whose proof is omitted here but which could not be omitted in Lean, was enough to deduce 01HR. It concerned me that at some point I had to go “beyond the universal property”. Not only that, it made this part of the code base much harder to follow. I had got us into this mess by telling Chris Hughes to prove 00EK without checking beforehand that it would suffice in applications — I naturally assumed that the literature didn’t have subtle holes in. Ramon Fernandez Mir has rewritten the entire code base from scratch, and did not prove 00EK by hand but instead proved a more invariant version, using rings isomorphic to $R[1/g_i]$ etc instead of the actual rings themselves. Instead of using the universal property (which might have caused issues with universes) he used a predicate introduced by Strickland which characterises precisely when a ring homomorphism $R\to A$ makes $A$ into an $R$-algebra isomorphic to $R[1/S]$ as an $R$-algebra. Everything works much more nicely — but we do not prove 00EK as it stands; we prove something slightly more general. We prove the thing that we actually need.

## Conclusions.

What I would hence like to argue is that this lazy usage of $=$ to mean “canonical isomorphism” actually blinds some mathematicians. Equality is such a powerful thing. If two canonically isomorphic objects are now deemed to be equal because they both obey some universal property, then all of a sudden we can manipulate them as if they are equal regardless of whether we are using the universal property or not. This is a very useful trick, because it enables us to cheat effectively without our peers noticing. By “cheat” here I mean that it enables us to leave out tedious arguments. No mathematician cares about these tedious arguments, as long as they do actually exist. In the case of schemes, they do exist. Of course they exist! If there was some fundamental problem with structure sheaves, people would have obviously spotted it decades ago. But what about all the other uses of $=$ to mean canonical isomorphism? Are we really checking them? Would we definitely know if some subtlety came up?

Imagine the following situation. Say there are two objects $X$ and $Y$ in your argument. Say that it is well-known that they are canonically isomorphic. Now maybe there are some constructions that one can make easily using $X$. And maybe there are some other constructions that one can make easily using $Y$. The constructions do involve the hands-on construction of $X$ and $Y$ and in particular go “beyond” the functoriality or universality of the isomorphism $X\to Y$, however they “have the same feel to them”, so they are clearly “equal” — at least, they feel as “equal” as $X$ and $Y$ are “equal”. Wouldn’t it be easy just to pass off the assertion that these constructions are also “equal”, even though this cannot be formally deduced from the functorial properties that one knows which give rise to the isomorphism $X\to Y$? Could that happen in the literature or is this just abstract navel-gazing?

It absolutely happens! And here is a very important time where a mathematician very nearly got away with it! In Dick Gross’ seminal 1990 paper on companion forms (“A tameness criterion for Galois representations associated to modular forms (mod p)”, Duke Math Journal Vol 61 no 2, Oct 1990) Gross canonically identifies several cohomology theories of modular curves, and then claims without any justification whatsoever that the Hecke operators defined on these cohomology groups are also identified. The cohomology groups were known to be “canonically isomorphic”, however this was one of those “canonical isomorphisms” which was of the form “look at this neat map; now everything works, except it takes many pages to justify this”. The canonical isomorphism was not even known to be functorial or natural, it was just “canonical” in this vague sense. In particular it was not known to commute with correspondences and hence with Hecke operators, in 1990. The anonymous referee picked up on this subtlety, but rather than rejecting the paper they just demanded that Gross explicitly flag that there was a gap in the argument. The paper was still published, with a comment about this in the introduction. Four years later, with the gap still not filled, Wiles and Taylor-Wiles used the paper in their proof of Fermat’s Last Theorem. Nobody batted an eyelid. I asked Taylor about this in 1995 and he assured me that he had checked that in the application of Gross’ results to the FLT proof, one could get around this issue. Most other people did not care becuase the results were “obviously true anyway” — at least that was my impression. There are a few people out there who care though; Taylor is one, and another one of them is Brian Conrad. It was not until 2007, seventeen years after Gross’ paper was published, that Bryden Cais, a student of Brian’s, resolved these issues in his PhD thesis. Nobody ever worried about this issue — because everyone knew that the results were going to be true. But with Gross thinking about canonical isomorphism as equality, we almost missed that there was even an issue to be checked.

How many other times has this happened in mathematics, and how many times have we, the community, not noticed? The referee of Gross’ paper was rumoured to be Serre, an extremely careful mathematician. Not all of us are as careful as him. Sloppy use of $=$ can cause trouble.

## About xenaproject

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in Uncategorized and tagged , . Bookmark the permalink.

### 14 Responses to Equality part 3: canonical isomorphism.

1. See for instance this post by Jim Dolan from 1993:

https://groups.google.com/forum/#!msg/sci.math/n1ypbcGpWto/Jb8lwVkOeREJ

and its sequel immediately following.

See also an extensive discussion here about ‘canonical’:

https://nforum.ncatlab.org/discussion/654/canonical-transformations/

around the nLab page

https://ncatlab.org/nlab/show/core-natural+transformation

(apologies for multiple links!)

Like

• xenaproject says:

I think it is clear that different mathematicians use the word “canonical” differently. Given that it has no definition, this is unsurprising. I guess the point of my post is not this, it’s that *even* in a situation where an isomorphism between two objects really is canonical in a precise sense, e.g. natural, if you then argue that the two objects are *equal* then this gives you the chance to pull the wool over people’s eyes, because equality gives you the right to replace one object with the other in any argument at all.

Like

2. Jules Jacobs says:

Doesn’t this issue already arise with simple quotients? We have Z and Z/5Z. Instead of working with the quotient Z/5Z we could work exclusively with Z and use ~ for equivalence mod 5. Then you’d have the issue that if you define a function f : Z -> A you can’t assume that f(n) = f(m) if n ~ m. We could now confuse the situation by using the symbol = for ~.

This would create a mess and a minefield of incorrect proofs. Quotients get us out of the mess by using a different type for Z and Z/5Z. If the function f is a ~ respecting function we write f : Z/5Z -> A. We can then freely use the symbol = for equivalence mod 5, and compose functions and proofs that use numbers mod 5, and this never leads to problems because the types ensure that the functions respect ~ whenever we depend on them respecting ~. For instance if g : Z/5Z -> Z/5Z then we can compose h = f . g and then h : Z/5Z -> A respects ~ too.

We can bridge between the Z world and the Z/5Z world: we may define a function f : Z/5Z -> A by first giving a function g : Z -> A and then supplying a proof that g(n) = g(m) when n ~ m.

Is the ring situation is analogous to this? We have the type Ring of rings, which is analogous to Z. A particular ring is analogous to a number n in Z. We have two notions of equality of rings: equality of their carrier set, and ring isomorphism. Hence we could have two Ring types, Ring and Ring/~, the latter being analogous to Z/5Z.

In this language, a simplified version of the problem seems to be that there is some property P : Ring -> Prop and a proof of P(R) for some particular ring R, and a ring R’ ~ R for which we also want P(R’), which is not automatically true. If P was Ring/~ -> Prop and R : Ring/~ then P(R) would automatically give P(R’).

Like

• xenaproject says:

The situation is analogous, but it’s like going from sets to categories — you’re “going one level up”. Groups have elements, but elements are atoms, you can’t really get any lower whilst remaining mathematically meaningful. Congruence mod 5 is an equivalence relation on the integers, one group. Here we’re talking about this vague notion of canonical isomorphism between two rings. The fact that there’s a category of rings in the background adds an extra layer of complexity to the situation. The problem is that the equivalence relation of “canonical isomorphism” is not well-defined, because it is context-dependent, and that context is coming from what else you are doing with the category. The analogy is fair but because we’re one level up, the details are much harder to deal with. Another issue is that you talk about predicates on the category of rings, but in Grothendieck’s example we are talking about actual data; explicit maps from ring A to ring B, and then A’ is canonically isomorphic to A and B’ is canonically isomorphic to B and we now want some sort of assurance that what we did to get the map A -> B is “the same” as what we did to get the map from A’ to B’. With Grothendieck’s example you can check this by hand, although it does *not* follow _immediately_ from an application of the universal property, one needs epsilon more (only epsilon, but it is not “by the universal property”). With Gross’ example you needed a 200 page PhD thesis.

Like

• Jules Jacobs says:

Certainly the proofs can be arbitrarily complicated, after all, proving that f : Z -> A only depends on its input mod 5 can already be arbitrarily complicated. Quotients only help keep track of which equivalence relation is used where, so that it is clear when such an additional argument is needed, and so that it is clear when treating ~ as = is kosher. The notion of canonical isomorphism is context dependent, but equivalence relations on Z are also context dependent: you have Z/5Z but also Z/6Z. Maybe I’m missing the point?

HoTT is supposed to extend quotients to one (or more) levels up isn’t it?

Like

3. xenaproject says:

There are several issues. Firstly, “being congruent mod 5” is a well-defined notion. “Being canonically isomorphic” is not. “Being isomorphic” is. HoTT is a way of dealing with the equivalence relation of “being isomorphic”. I am talking about something slightly different.

Mathematicians are arguing in the following way. “Here is a theorem about some objects. Here are some canonically isomorphic objects. Do these canonically isomorphic objects satisfy some analogous theorem? Well, let’s write canonical isomorphism as equals. Now I guess we’re done because there doesn’t seem to be anything left to prove!”. There’s some implicit stuff that needs checking here. Hiding behind = makes it easy to forget to check that every diagram commutes. The implicit proof that all the diagrams commute is “come on, these things are canonically isomorphic”. For canonical ring isomorphisms like R[1/f][1/g]=R[1/fg] my point is that there’s an explicit example early on in EGA where the “canonical isomorphism” is in fact a functorial isomorphism, which gives you for free a whole bunch of diagrams which commute. However de Jong then says there’s nothing left, however the map beta is *not* part of the package that one gets from the universal property, at least if you’re talking about R-algebras and R-algebra morphisms. One can no doubt reformulate everything in terms of equalizers and then maybe it is — I am simply pointing out that this reformulation is not there, we are just doing it in our heads somehow. The EGA example is a very simple one and it’s very easy to work around it. It’s just interesting to see it happens.

Another issue is this: when formalising theorems which are going to be used later in a theorem prover, it is possible to formalise them for (a) the objects you’re interested in, or (b) objects isomorphic to the objects you’re interested in. However it is *not* possible to formalise the theorem so that it applies to objects canonically isomorphic to the objects you’re interested in, because this notion is intrinisically not formalisable in the full generality which mathematicians may want.

Like

4. Andrej Bauer says:

Thank for a very interesting writeup, especially the examples of shady uses of “equality” in real life. You are aware of the fact that these precise issues with equality are addressed by Voevodsky’s Univalence axiom? Whether or not you subscribe to homotopy type theory and univalent mathematics, I think the moral of the story is clear. There are many ways in which structures can be equivalent (a better concept than “isomorphic” from the HoTT point of view). If one wants to pretend that equivalence is equality (for some notion of “is”), then one has to admit the fact that structures can be equal in many ways. The punch line: we cannot ignore proofs of equality anymore, but then we cannot ignore proofs in general. By this I mean that proofs must enter mathematics as first-class citizens (which they are not in normal mathematics).

Like

• xenaproject says:

Hi Andrej. My experience using Lean absolutely makes me buy into the notion that proofs are first-class citizens. I have no experience using UniMath, or HoTT in Lean (it is possible to do HoTT in Lean 3 as I’m sure you know, maybe it’s time I tried it). But my impression, based on this position of relative ignorance, is that HoTT only lets you define things invariant under *all* isomorphisms. There is some sort of weird half-way house here where mathematicians are defining equality to mean “canonical isomorphism”, which is neither DTT’s equality nor HoTT’s — indeed, from a formalist point of view, it isn’t really anything at all. It’s either a short-cut to save us having to do some tedious checks, or mathematics being done in a dangerous way, depending on whether you believe that mathematicians are trustworthy or not.

Like

• Andrej Bauer says:

HoTT is not as trivial as you make it sound. What is magical about it is that the Univalence axiom induces the “correct” notin of equality in all situations so far studied: caregories are equal when equivalent, groups are equal when isomorphic, equality on subgroups can be controlled depending on how exactly you define subgroups, etc.

But I wouldn’t necessarily recommend dropping everything you’re doing and diving into HoTT. It’s a pretty radical move.

Like

• Timothy Chow says:

Andrej, I think it would be valuable if you would spell out in some detail (with someone like Kevin in mind as an audience) exactly what kind of tradeoff would be involved if one were to formalize this particular example in HoTT. I’m guessing that HoTT would reduce the chances of being blindsided by the need for an unexpected diagram chase or rewrite of a lemma. But what exactly would “proofs entering mathematics as first-class citizens” entail?

Like

• xenaproject says:

Basically I decided that I would not take HoTT systems seriously for “mainstream mathematics” until they show me that they can do some basic algebraic geometry, eg to define the presheaf of rings on an affine scheme and show it’s a sheaf. I personally think that Voevodsky got stuck here. In a lecture in Singapore he talks about localisation of rings in HoTT and then makes a cryptic comment about how then things start to get interesting. Now we have schemes in Lean’s official maths library, and we’ve worked our way through transferring stuff along isomorphisms by hand, I see that this approach works. I’ve heard many people saying that HoTT would do this better but I’m yet to see anything approaching the Grothendieck setup to alg geom in any HoTT system, all I’ve heard is excuses or claims that “we should use locales” (ie answer a different question). Dependent type theory without univalence is at this point the only system which has successfully managed to make schemes, and over on the lean chat we’re currently involved in the experiment of finding out if they’re usable by proving theorems from the stacks project. This is the acid test.

Like

5. Everything you say here sounds very well reasoned. I do find it a little shocking, however, to read some of the responses to this post on twitter. It does make me feel a little along the lines of “these people have no conception of what mathematics actually is” where by “mathematics” I mean to refer to something that me or Michael Harris or you (historically and probably still now) would consider mathematics. (Let me not try to define in a comment what this means exactly.)

To be critical of myself, I think part of my past hostility (perhaps a too accusatory word…) towards some of these projects is the [possibly entirely baseless] feeling that some of the people involved might not recognize “real mathematics” (scare quotes) if it slapped them across the face with a pair of smoked kippers. That is not supposed to imply that there are not some very smart people involved, just the suspicion that they are not even studying the same subject as I am. What I like about your involvement is that I have some trust in your taste — that makes it much easier to take these things seriously (Fabstracts also sounds intriguing).

Like

• xenaproject says:

I would like to reconfirm here that my understanding of what mathematics is, has not changed, and still very much coincides with the sort of mathematics I see on the Persiflage blog.

I guess I could make two further comments about this. Firstly, I now actually do have some *understanding* of what constructivism means in practice; I would say that this understanding was largely obtained by (a) reading Andrej Bauer’s paper on constructivism in Bull AMS https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/ (although Bauer has pointed out in his blog that he is not himself a constructivist) and (b) attempting to formalise things like perfectoid spaces in a constructivist way and then realising that occasionally it’s just too hard (or perhaps not even possible, although that assertion requires proof and I’m not sure I’m the right kind of person to come up with such a proof).

The second comment is that I don’t think it can be taken for granted that my opinions on mathematics have not changed. It’s true that mine stayed the same, but my impression is that Voevodsky’s opinions changed dramatically once his eyes were opened to doing maths on computers, and I believe that his views on what was interesting mathematics became far more constructivist. My beliefs stem from his 2017 Newton Institute talk https://www.newton.ac.uk/seminar/20170710113012301 and in particular the part from 43:40 to 46:40. Voevodsky describes a failed attempt to convince Suslin to remove the axiom of choice from an intermediate result and makes it clear that he wants a constructive proof of the Milnor conjecture.

Like