Grothendieck, Equality, and the Trouble with Formalising Mathematical Arguments

:::info Author: KEVIN BUZZARD

:::

Table Of Links

Abstract

1. Acknowledgements & Introduction

2. Universal properties

3. Products in practice

4. Universal properties in algebraic geometry

5. The problem with Grothendieck’s use of equality.

6. More on “canonical” maps

7. Canonical isomorphisms in more advanced mathematics

8. Summary And References

Abstract

We discuss how the concept of equality is used by mathematicians (including Grothendieck), and what effect this has when trying to formalise mathematics. We challenge various reasonable-sounding slogans about equality.

Overview

Many mathematical objects and constructions are uniquely characterised by some kind of defining property. For example the real numbers are the unique complete Archimedean ordered field, and many constructions in algebra (localisations, tensor products,. . . ) and topology (product of topological spaces, completion of a metric or uniform space,. . . ) are characterised uniquely by a universal property. To be more precise, I would like to discuss properties which define a mathematical object up to unique isomorphism. This is a very strong statement: to give a non-example, we could consider the property of being a group of order 5.

\ There is only one such group, up to isomorphism, however this group has automorphisms (for example the map sending an element to its square), meaning that it is unique but only up to non-unique isomorphism, and hence the property of being a group of order 5 is not the kind of property that this paper is about. Let us now fix a property P which uniquely characterises a mathematical object, up to unique isomorphism. Here are three assertions.

\ Assertion 1. You can (and probably should) develop the theory of objects characterised by P using only the assumption P, and you do not need to worry about any particular construction of the object (beyond knowing that some construction exists which satisfies P, and hence that your theory is not vacuous).

Assertion 2. Any two mathematical objects satisfying P may in practice be assumed to be equal, because any mathematically meaningful assertion satisfied by one is also satisfied by the other.

Assertion 3. More generally, if you have two objects which are canonically isomorphic, then these objects may in practice be assumed to be equal.

\ Let us consider an example. Whilst there are several different constructions of the real numbers from the rationals (Cauchy sequences, Dedekind cuts, Bourbaki uniform space completion,. . . ), all of the basic analysis taught in a first undergraduate course is developed using only the Archimedean and completeness axioms satisfied by the reals. A mathematician would not dream of saying which definition of the real numbers they were using – this would be absurd. Indeed Newton, Euler and Gauss were happily using “the” real numbers long before Cauchy, Dedekind and Bourbaki came along with their different models: each of their definitions of the ordered field R is uniquely isomophic to the others, so which one we are actually using doesn’t matter in practice.

\ I will say more about localisations later, but there are also several different constructions of the localisation R[1/S] of a commutative ring at a multiplicative subset (a quotient of R×S, a quotient of a multivariable polynomial ring. . . ) and a mathematician would never state precisely which construction they are using when they write R[1/S]; we know that this is irrelevant.

\ In this paper I argue that the first assertion above is false, the second is dangerous, and the third is meaningless. Assertions 2 and 3 seem to be used in many places in the algebraic geometry literature – indeed we will discuss Grothendieck’s usage of the = symbol in some depth later. However, as a working mathematician I am also aware that there is something deeper going on here, which I find it difficult to put my finger on. Even though the word “canonical” has no formal meeting, mathematicians are certainly not being mindless in their use of the idea.

\ The concept that two objects are canonically isomorphic and can hence be identified is an extremely important one in practice; it is a useful organisational principle, it reduces cognitive load, and it does not in practice introduce errors in arguments, at least if the author knows what they are doing. Similarly, making definitions and proving theorems about objects by using an explicit construction rather than the universal property is a practical tool which is used across mathematics (for example, picking a basis of a vector space to make a definition and then observing that the definition is independent of the choice).

\ What is frustrating about the situation is the following. Let’s say that one is attempting to formalise some mathematics on a computer (that is, translating the mathematics from the paper literature into the language of an interactive theorem prover – a computer program which knows the axioms of mathematics and the rules of logic). Right now this process involves writing down many of the details of one’s arguments.

\ When one is forced to write down what one actually means and cannot hide behind such ill-defined words as “canonical”, or claims that unequal things are equal, one sometimes finds that one has to do extra work, or even rethink how certain ideas should be presented. Indeed, sometimes the most painless way to do this work involves having to create new mathematical ideas which are not present in the paper arguments. I am certainly not arguing that the literature is incorrect, but I am arguing that many arguments in the literature are often not strictly speaking complete from a formalist point of view.

\ With the advent of the formalisation of the mathematics around algebraic and arithmetic geometry using computer theorem provers, for example the work coming out of the Lean prover community ([BCM20], [Liv23], [dFF23], [AX23], [Zha23],. . . ) and related work in Isabelle ([BPL21]) and cubical Agda ([ZM23]), these things will start to matter. In section 5 below I give an explicit example of some real trouble which we ran into when proving a very basic theorem about schemes, and which was only ultimately resolved in a satisfactory way after some new mathematical ideas were developed by the Lean community.

:::info This paper is available on arxiv under CC BY 4.0 DEED license.

:::

\