Max Zeuner: Towards formalizing affine schemes in univalent foundations
Time: Wed 2021-05-19 10.00 - 12.00
Location: Zoom, meeting ID: 610 2070 5696
Lecturer: Max Zeuner
Formalizing schemes, the fundamental objects of modern algebraic geometry, has become somewhat of a benchmark challenge for modern proof assistants and their mathematical libraries. In this talk we want to discuss some work in progress for constructing affine schemes in Cubical Agda, a relatively new proof assistant that can be used as a constructive foundation for univalent mathematics. Unlike in existing formalizations in other proof assistants we want to work constructively to be able to harness the nice computational properties of Cubical Agda.
The first half of the talk we will thus introduce locales, a point-free analogue of topological spaces, and show how they can be used to define the Zariski spectrum of a ring and its structure sheaf constructively. In the second half we will then discuss how this construction can be formalized in Cubical Agda and look at some of the issues that arise from working in a univalent framework.