University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Formalising the Multigraded Proj Construction in Lean 4

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Formalising the Multigraded Proj Construction in Lean 4

Download to your calendar using vCal

If you have a question about this talk, please contact Anand Rao Tadipatri .

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

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Humanitarian Centre The Maypole Pub (upstairs), Portugal Place, Cambridge CB5 8AF in person & via zoom

Other talks

Title to be confirmed Carrollian momenta from anti de Sitter External Seminar - Hilde Nelissen TBC Harnessing Radical Reactivity for Molecular Innovation Title to be confirmed Dr Dinis Calado, Senior Group Leader, Immunity and Cancer Laboratory, the Francis Crick Institute
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity