Riemann-Roch

Stream: Is there code for X?

[Chris Henson]

Daniel Litt (a mathematician working in AG) asked on Twitter

Challenge to autoformalization companies: formalize the Riemann-Roch theorem (say for curves over an algebraically closed field) in Lean.

Not being too familiar with that area of Mathlib, I was curious how much additional work is needed to get to the statement of this.

[Ruben Van de Velde]

I would search for the numerous threads about that theorem/those theorems on this zulip

[Johan Commelin]

I would be quite sad if this happens. It would scoop the work of Raphael Douglas Giles, who is aiming to finish this project as part of his PhD work.

I'm not on Twitter, but if someone wants to pass this on, please do.

[Chris Henson]

This is part of why I asked. I did search beforehand, but it was not immediately clear to me what the most recent activity was.

[Johan Commelin]

cc @Daniel Litt

[Kevin Buzzard]

Daniel's response to the Atiyah-Singer index theorem claim isn't quite true I don't think -- even over $\mathbb{C}$ the A-S index theorem would only give you a statement in differential geometry about compact Riemann surfaces; proving that this implies the corresponding statement in algebraic geometry would be quite a lot of work -- probably more work than just formalizing the alg geom theorem from scratch.

[Andrew Yang]

If you are happy with $h^0(X, \mathcal{L}_D) - h^1(X, \mathcal{L}_D) = 1 − g + deg(D)$, then we are already able to write down a statement: https://gist.github.com/erdOne/a2f89628ddfbc7da57a1e2a087f2f40a

This is the excerpt of the final statement:

theorem RiemannRoch
    {X : Scheme.{u}} {k : Type u} [Field k] (f : X ⟶ Spec (.of k)) -- let `X` be a `k`-scheme
    [IsSmoothOfRelativeDimension 1 f] [IsIntegral X] -- that is integral and smooth of dim 1
    (n : Type) [Finite n] (ι : X ⟶ Proj (MvPolynomial.homogeneousSubmodule n k))
    [IsClosedImmersion ι] -- and `ι` is a closed embedding of `X` to `ℙₖⁿ`.
    (hι : ι ≫ Proj.toSpecZero _ ≫ Spec.map (CommRingCat.ofHom <| algebraMap k _) = f)
    {σ : Type*} (D : CartierDivisor X σ) :
    Module.finrank k (D.sheafOfModules.H (R := .of k) f 0) -
      Module.finrank k (D.sheafOfModules.H (R := .of k) f 1) = D.deg - X.genus f + 1 := sorry

This is just a combination of work by Joël Riou Raphael Douglas Giles and some leftover stuff in the last AIM workshop on algebraic geometry.

[Kevin Buzzard]

Wooah we have .genus? Is this defined as dimension of space of H^1(\O) or something? I thought we didn't have sheaf of differential 1-forms yet.

[Kevin Buzzard]

What is the role of sigma?

[Andrew Yang]

We can write down a sheaf that is isomorphic to the sheaf of relative differentials. This was done in AIM. And then we take the dimension of the global sections. But we could also have written $h^1(\mathcal{O}_X)$ thanks to Joel.

sigma is an indexing set of the ad-hoc definition of Cartier divisors.

[Daniel Litt]

Hi all, thanks for the heads-up on this! Certainly don't mean to step on anyone's toes.