October 24: Max Zeuner, Univalent foundations of constructive algebraic geometry
Angiuli, Carlo
This week in HoTTEST we are excited to host Max Zeuner, who will speak about the "Univalent foundations of constructive algebraic geometry". (Abstract at the end of this email.)
The talk is at 11:30am EDT = 15:30 UTC on Thursday, October 24, and will be 60 minutes long followed by up to 30 minutes of discussion.
The Zoom link is https://zoom.us/j/994874377
Further information, including videos and slides from past talks, is available at:
https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html
Carlo
(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.)
--
Max Zeuner
Univalent foundations of constructive algebraic geometry
HoTT/UF aims not only to be framework for synthetic homotopy theory, but also a suitable foundation for "set-level" constructive mathematics. In this talk we want to support this claim by discussing how the basic theory of schemes, the fundamental notion of modern algebraic geometry, can be set up in HoTT/UF. The classical literature contains two different approaches to schemes: schemes as locally ringed spaces and schemes as functors. We will show how both of these can be made constructive and predicative and discuss what kind of issues arise when defining qcqs-schemes using either approach in HoTT/UF. Finally, we give a sketch of a univalent proof that the two constructive definitions coincide.