Table Of Links
Abstract
- 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
More On “Canonical” Maps
The previous remarks have been mostly the flagging of a technical point involving mathematicians “cheating” by considering that various nonequal but uniquely isomorphic things are equal, and a theorem prover pointing out the gap. Whilst I find this subtlety interesting, I do not believe that this slightly dangerous convention is actually hiding any errors in algebraic geometry; all it means is that in practice people wishing to formalise algebraic geometry in theorem provers are going to have to do some work thinking hard about universal properties, and possibly generate some new mathematics in order to make the formalisation of modern algebraic geometry a manageable task.
Section 1.2 of Conrad’s book [Con00] gives me hope; his variant of the convention is summarised there by the following remark: “We sometimes write A = B to denote the fact that A is canonically isomorphic to B (via an isomorphism which is always clear from the context).” Even though we still do not have a definition of “canonical”, we are assured that, throughout Conrad’s work at least, it will be clear which identification is being talked about. In the work of Grothendieck we highlighted, the rings he calls “canonically isomorphic” are in fact uniquely isomorphic as R-algebras. However when it comes to the Langlands Program, “mission creep” for the word “canonical” is beginning to take over. Before I discuss an example from the literature let me talk about a far more innocuous use of the word.
Consider the following claim:
Theorem (The first isomorphism theorem). If φ : G → H is a group homomorphism, then G/ ker(φ) and im(φ) are canonically isomorphic.
I think that we would all agree that the first isomorphism theorem does say strictly more than the claim that G/ ker(φ) and im(φ) are isomorphic – the theorem is attempting to make the stronger claim that there is a “special” map from one group to the other (namely the one sending g ker(φ) to φ(g)) and that it is this map which is an isomorphism. In fact this is the claim which is used in practice when applying the first isomorphism theorem – the mere existence of an isomorphism is often not enough; we need the formula for it. We conclude
Theorem. The first isomorphism “theorem” as stated above is not a theorem.
Indeed, the first isomorphism “theorem” is a pair consisting of the definition of a group homomorphism c : G/ ker(φ) → im(φ), and a proof that c is an isomorphism of groups. In contrast to earlier sections, uniqueness of the isomorphism is now not true in general. For example, if H is abelian, then the map c ∗ sending g ∈ G/ ker(φ) to c(g) −1 is also an isomorphism of groups, however this isomorphism is not “canonical”: an informal reason for this might be “because it contains a spurious −1”, but here a better reason would be because it does not commute with the canonical maps from G to G/ ker(φ) and H.
What is actually going on here is an implicit construction, as well as a theorem. The claim implicit in the “theorem” is that we can write down a formula for the isomorphism – we have made it, rather than just deduced its existence from a nonconstructive mathematical fact such as the axiom of choice or the law of the excluded middle. My belief is that some mathematicians have lost sight of this point, and hence are confusing constructions (definitions) with claims of “canonical”ness (attempts to state theorems). The currency of the mathematician is the theorem, so theorems we will state.
:::info
Author: KEVIN BUZZARD
:::
:::info
This paper is available on arxiv under CC BY 4.0 DEED license.
:::
