Grothendieck's use of equality

DOI10.1007/978-3-031-68934-5_13MaRDI QIDQ6911854zbMATH OpenFDO

Publication date 24 October 2025

Full work available at URL https://doi.org/10.1007/978-3-031-68934-5_13

History of mathematics in the 20th century (01A60) Mechanization of proofs and logical operations (03B35) Langlands-Weil conjectures, nonabelian class field theory (11R39) Generalizations (algebraic spaces, stacks) (14A20) History of category theory (18-03) Foundations, relations to logic and deductive systems (18A15)

Review text

Let's fix a property \(P\) which uniquely characterizes a mathematical object, up to unique isomorphism. Here are three assertions.\N\N\begin{itemize}\N\item[Assertion 1] One can delelop the theory of objects characterized by \(P\) exclusively under the assumption \(P\) without worring about any particular construction of the object.\N\N\item[Assertion 2] Any two mathematical objects abiding by \(P\) may in practice be assumed to be equal.\N\N\item[Assertion 3] If one has two objects which are canonically isomorphic, then these two objects may in practice be assumed to be eqaul.\N\end{itemize}\N\NThis paper argues that the first assertion is false, the second is dangerous, and the third is meaningless. Since the second and third assertions are used in many places in algebraic geometry, the author discusses Grothendieck's usage of the = symbol in some depth. The author argues that there are two holes in arguments in mathematical literature.\N\N\begin{itemize}\N\item[(1)] There is the issue of people making constructions or proving theorems which make essential use of a model of a mathematical object which is defined up to unique isomorphism. The hole here is that it needs to be checked that the argument does not depend on the explicit details of the model. One useful trick is to abuse the equality symbol, making it mean something which it does not mean.\N\N\item[(2)] The second kind of hole is the issue of various maps being regarded as canonical where they are in fact not unique, and there are implicit choices of sign being made. An author does not state precisely which convention they are using when it comes to rhings like the theory of Shimura varieties or homological algebra.\N\end{itemize}\N\NThe author is arguing that many arguments in the literature are often not strictly speaking complete from a formalist point of view. With the advent of the formalization of mathematics around algebraic and arithmetic geometry using computer theorem provers, these things start to matter. The author gives an explicit example of some real trouble which the author ran into when proving a very basic theorem about schemes, and which was only ultimately resolved in a satisfactory way after some new mathematical idea were developed by the Lean community [\textit{D. K. Angdinata} and \textit{J. Xu}, LIPIcs -- Leibniz Int. Proc. Inform. 268, Article 6, 19 p. (2023; Zbl 07949099); \textit{K. Buzzard} et al., ``Formalising perfectoid spaces, Preprint, \url{arXiv:1910.12320}; \textit{M. I. De Frutos-Fernández}, LIPIcs -- Leibniz Int. Proc. Inform. 268, Article 13, 18 p. (2023; Zbl 07949106); \textit{A. Livingston}, LIPIcs -- Leibniz Int. Proc. Inform. 268, Article 22, 17 p. (2023; Zbl 07949115); \textit{J. Zhang}, LIPIcs -- Leibniz Int. Proc. Inform. 268, Article 35, 17 p. (2023; Zbl 07949128)].\N\NFor the entire collection see [Zbl 1562.01004].

Cites work

Cited in

(1)

How to make log structures

This page was built for publication: Grothendieck's use of equality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6911854)