skip to content

Department of Computer Science and Technology

Date: 
Thursday, 19 June, 2025 - 17:00 to 18:00
Speaker: 
Jujian Zhang (Imperial College London) and Arnaud Mayeux (The Hebrew University of Jerusalem)
Venue: 
MR14 Centre for Mathematical Sciences

Brenner-Schröer Proj construction, also known as multigraded Proj construction generalizes the ℕ-graded Proj construction to rings graded by arbitrary finitely generated abelian groups. It is a generalization in the sense that it also has twisting sheaves, blowups, and quasi-coherent sheaf; moreover, it is fully functorial and compatible with tensor product. We formalized the Brenner-Schröer Proj construction and its functorality in Lean4. In this talk, we will go through the relevant mathematical background of the multigraded Proj construction and explain how to work with graded objects and glueing of schemes in Lean4.

=== Hybrid talk ===

Join Zoom Meeting
https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954
Passcode: ITPtalk

Seminar series: 
Formalisation of mathematics with interactive theorem provers

Upcoming seminars