14th edition: Charmey January 13 -17, 2025
Tentative Schedule
Monday January 13 |
Tuesday January 14 |
Wednesday January 15 |
Thursday January 16 |
Friday January 17 |
|
breakfast |
8:45-9:45 mini-course |
8:45-9:45 mini-course |
8:45-9:45 mini-course |
8:45-9:45 mini-course |
10:15-11:15 mini-course |
10:15-11:15 mini-course |
10:15-11:15 mini-course |
10:00-11:00 mini-course |
12:30 welcome |
11:45-12:45 mini-course |
11:45-12:45 mini-course |
11:45-12:45 mini-course |
11:15-12:15 mini-course |
lunch |
bus at 12:40 |
14:30-15:30 mini-course |
time for discussion / enjoying the mountain side |
|
16:00-17:00 mini-course |
17:20-18:10 talk |
17:20-18:20 talk |
17:20-18:10 talk |
17:30-18:30 mini-course |
18:30-19:20 talk |
18:30-19:20 talk |
18:30-19:20 talk |
19h dinner |
19:30 dinner |
Mini-courses
-
Formalising arithmetic and geometry in Lean: an introduction
David Loeffler (UniDistance Suisse)
Abstract
This mini-course is an introduction to the Lean Theorem Prover, a computer program for formally checking the validity of mathematical proofs. The course will mostly focus on how to use the software in practice (rather than going too deep into the logical foundations). In particular, we'll see a tour of some of the theorems in number theory and algebraic geometry that have already been formalised in the huge "Mathlib" library, and try out formalising a few more lemmas for ourselves.
There will be lots of examples and exercises to try out, so you should bring a computer of your own that you can install Lean on. The software runs fine on Windows, Mac, and most Linux distributions (but is unlikely to work well on phones or tablets). Installing Lean on your computer yourself before arriving in Charmey is not obligatory, but might be a good idea if you want to get the most out of the course; see docs.lean-lang.org/lean4/doc/quickstart.html for instructions.
-
Derived categories of coherent sheaves
Evgeny Shinder (University of Sheffield)
Abstract
We will start with a review of standard homological algebra, such as injective and projective resolutions and Ext-groups. Then we discuss derived functors, mostly focussing on coherent sheaves, and in particular review the coherent sheaf cohomology. Finally we go into the construction of the derived category of coherent sheaves and study its properties.
-
Different cones of divisors: from Mori Dream Spaces to K-trivial varieties
Zhixin Xie (Université de Lorraine)
Abstract
Given a variety, we consider the real vector space spanned by Cartier divisors modulo numerical equivalence. From the point of view of birational geometry, we are interested in the shape of the nef cone and the movable cone in this vector space.
For a Fano variety, i.e. a variety with ample anticanonical class, it follows from the Mori’s cone theorem that the nef cone is rational polyhedral. More generally for a Mori Dream Space, both the nef cone and the movable cone are rational polyhedral. However, these cones can be very wild in general: when we turn to K-trivial varieties, i.e. varieties with numerically trivial canonical class, they behave less well than Fano varieties. For instance, we can construct examples of K-trivial varieties for which the nef or the movable cone is round. Nevertheless, the Kawamata-Morrison cone conjecture predicts that the nef and the movable cones on a K-trivial variety are rational polyhedral up to the action of natural groups acting on them.
In this course, we will introduce basic notions and techniques related to the description of different cones of divisors and we will illustrate them on many examples. In particular, we present tools from the Minimal Model Program and their application to connect different cones. We will introduce the Kawamata-Morrison conjecture and explain some known results. We will also discuss the cones of divisors of varieties with nef anticanonical class, which interpolate between Fano varieties and K-trivial varieties.
Talks
Participants
Organizers
Andrea Fanelli (Bordeaux)
Philipp Habegger (Basel)
Julia Schneider (Sheffield)
Logistic support: Adrien Dubouloz (Poitiers)
Support
ANR Fracasso
Swiss Mathematical Society
Swiss Academy of Sciences
University of Basel