Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types

Abstract

Church’s simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a challenge was issued. Schemes are sophisticated mathematical objects in algebraic geometry introduced by Alexander Grothendieck in 1960. In this article we report on a successful formalization of schemes in the simple type theory of the proof assistant Isabelle/HOL, and we discuss the design choices which make this work possible. We show in the particular case of schemes how the powerful dependent types of Coq or Lean can be traded for a minimalist apparatus called locales.

Keywords:

• Logic and verification
• higher order logic
• type theory
• algebraic geometry
• sheaves
• schemes

2010 MSC::

• 14A15
• 14-04
• 03B35
• 68V20

Acknowledgments

We thank Kevin Buzzard for his stimulating wit and his communicative energy and André Hirschowitz who commented on a draft of this document. We also thank the reviewers, one of whom noticed an inaccuracy (fortunately easy to correct) in the formal translation into Isabelle of Definition 3.21.

Notes

1 https://github.com/leanprover-community/mathlib/issues/26

2 https://github.com/leanprover-community/mathlib/issues/26

3 https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

4 https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/.SeethesectionentitledIsabelle/HOLusers.

5 Not to be confused with the locales of point-free topology!

6 https://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/

7 https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/

8 https://www.isa-afp.org/

9 https://isabelle.in.tum.de/dist/library/HOL/HOL/Topological_Spaces.html

10 https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Abstract_Topology.html

11 It is also called the ring of fractions of R by S or the localization of R at S. No confusion with the factor ring should be possible, since S is not an ideal of R but a multiplicative submonoid.

12 In more modern parlance it is called a colimit.

13 https://xenaproject.wordpress.com/2020/06/05/the-sphere-eversion-project/

Additional information

Funding

This work was supported by the ERC Advanced Grant ALEXANDRIA (Project GA 742178).