Speaker: Jujian Zhang, Imperial College London

Inviter: 支丽红研究员

Title: Towards a Formalisation of Sheaf Cohomology in Lean4

Language: Chinese

Time & Venue: 2024.09.06 10:00-11:00 南楼N202

Abstract: Sheaf cohomology is an indispensable tool in algebraic geometry: without it, it is impossible to even state important theorems like the RiemannRoch theorem, Serre’s GAGA. In this talk, I will present a complete formalisation of enough injectiveness in the category of sheaves of modules over a scheme in the Lean4 proof assistant. The talk would consist of the two parts: an overview of the proof employed in the formalisation; followed by a discussion surrounding design choices that made the formalisation. Given the immaturity of modern algebraic geometry in mathlib4, enough injectiveness is a favourable addition, it would be a necessary ingredient for many branches of algebraic geometry, albeit far more and far more diﬃcult results are required: coupled with the recent development of M˜ sheaf, a natural project would be deﬁning the quasi-coherent sheaves of modules and Čech cohomology and show that it agrees with the derived functor cohomology, opening the door to compute sheaf cohomology for Proj and large scale formalisation projects of the Riemann-Roch theorem or Serre’s GAGA mentioned before; develop the derived category, deformation theory and intersection theory to study the Grothendieck Duality Theorem in Lean4; deﬁne the Hilbert polynomial of a coherent sheaf and relate it to Serre’s vanishing theorems.