BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising the Multigraded Proj Construction in Lean 4 - Jujian Z
 hang (Imperial College London) and Arnaud Mayeux (The Hebrew University of
  Jerusalem)
DTSTART:20250619T160000Z
DTEND:20250619T170000Z
UID:TALK229684@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Brenner-Schröer Proj construction\, also known as multigraded
  Proj construction generalizes the ℕ-graded Proj construction to rings g
 raded by arbitrary finitely generated abelian groups. It is a generalizati
 on in the sense that it also has twisting sheaves\, blowups\, and quasi-co
 herent sheaf\; moreover\, it is fully functorial and compatible with tenso
 r product. We formalized the Brenner-Schröer Proj construction and its fu
 nctorality in Lean4. In this talk\, we will go through the relevant mathem
 atical background of the multigraded Proj construction and explain how to 
 work with graded objects and glueing of schemes in Lean4.\n\n=== Hybrid ta
 lk ===\n\nJoin Zoom Meeting\nhttps://cam-ac-uk.zoom.us/j/89856091954?pwd=B
 ba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954\nPasscode: IT
 Ptalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR