(Nice) algebraic curves

Stream: Is there code for X?

[Michael Stoll]

How close are we to be able to state "Let $C$ be a nice (= smooth, projective and geometrically irreducible) curve over the field $K$"?

Background: I'm planning to give another talk (at the Swiss Number Theory Days) similar to the one I gave at the Mordell Conference earlier this year (here are the slides), and I'd like to check on the status quo regarding being able to state Mordell's Conjecture/Faltings' Theorem based on Mathlib.

As far as I can remember, there were some encouraging developments at and after the AIM workshop on formalizing algebraic geometry, but I haven't followed this in detail since then. So any updates are appreciated.

Grepping through Mathlib for "Curve" gives lots of hits for "EllipticCurve", "WeierstrassCurve" and "IntegralCurve" (which is not an integral curve in the sense of alg. geom.), but apparently nothing else, so it looks like there is no direct definition available. But perhaps this is easy to add with what is available?

[Christian Merten]

• For smooth (of rel. dimension 1), you can have a look at #16890 for an overview. There is more in the pipeline, but I am hesitant to create long sequences of dependent PRs.
• If you are happy to replace "projective" with "proper", then it is there, but you have to piece docs#AlgebraicGeometry.UniversallyClosed, docs#AlgebraicGeometry.IsSeparated, docs#AlgebraicGeometry.LocallyOfFiniteType and docs#AlgebraicGeometry.QuasiCompact together (for progress towards proper being usable, see e.g. #15038).
• no geometrically irreducible, but you can piece it together from docs#CategoryTheory.MorphismProperty.universally and docs#IrreducibleSpace

[Michael Stoll]

@Christian Merten Thanks! I'll have a look.

[Michael Stoll]

OK, I guess for the purposes of my talk, the point is that we can, with some work, define a notion of "nice curve" already now (modulo projective vs. proper), but some more work needs to be done to make this nice (pun intended) and usable. (Before seriously embarking on a project along the lines described in the talk, it is certainly better to wait until algebraic curves are in Mathlib. But it looks like this will not be very far away.)

[David Ang]

If you're willing to restrict to genus 2 hyperelliptics, Mordell's conjecture can arguably be stated today :)

[Michael Stoll]

This will be true for hyperelliptic curves in general, but I consider that cheating :smile:

[Kevin Buzzard]

How close are we to being able to talk about H^0(Omega^1)? That'll give genus but I don't know if we've glued together the one-forms on the affine pieces yet

[Michael Stoll]

I didn't dare to ask for the genus yet...

[Kevin Buzzard]

Oh I thought the goal was stating Faltings' theorem!

[Christian Merten]

Kevin Buzzard said:

How close are we to being able to talk about H^0(Omega^1)? That'll give genus but I don't know if we've glued together the one-forms on the affine pieces yet

I think we are close to having $\Omega^1$ as a presheaf, but I don't know if there is more. Maybe @Joël Riou wants to comment?

[Antoine Chambert-Loir]

Maybe $H^1(X, \mathcal O_X)$ will be accessible first.

[Michael Stoll]

Kevin Buzzard said:

Oh I thought the goal was stating Faltings' theorem!

Sure. But before we talk about the genus, we need the curves... :smile:

[Joël Riou]

Christian Merten said:

I think we are close to having $\Omega^1$ as a presheaf, but I don't know if there is more. Maybe Joël Riou wants to comment?

We have the "absolute" presheaf of differentials of presheaf of rings (over the integers). With some more work about sheafification and pullbacks of (pre)sheaves of modules, the relative (pre)sheaf of differentials could be defined. With some more work, we could show it is quasi-coherent...

[Joël Riou]

I am currently thinking about making some progress about pullbacks of (pre)sheaves of modules.

[Christian Merten]

Joël Riou said:

Christian Merten said:

I think we are close to having $\Omega^1$ as a presheaf, but I don't know if there is more. Maybe Joël Riou wants to comment?

We have the "absolute" presheaf of differentials of presheaf of rings (over the integers). With some more work about sheafification and pullbacks of (pre)sheaves of modules, the relative (pre)sheaf of differentials could be defined. With some more work, we could show it is quasi-coherent...

Do I understand correctly, that this is needed to allow arbitrary F in docs#PresheafOfModules.DifferentialsConstruction.relativeDifferentials' ?

[Joël Riou]

Yes, the idea is to construct the relative differential of $f : X \to S$ by using the cokernel of $f^* \Omega^1_{S/\mathbf{Z}}\to \Omega^1_{X/\mathbf{Z}}$

[David Loeffler]

Assuming we can define the genus as a cardinal (as the dimension of $H^0(X, \Omega^1)$), how do we get from there to defining it as a Nat? That amounts to proving that $H^0(X, \Omega^1)$ is finite-dimensional, which sounds like serious work.

[Adam Topaz]

There is always docs#Cardinal.toNat

[David Loeffler]

"This function sends finite cardinals to the corresponding natural, and infinite cardinals to 0." :vomit:

[Kevin Buzzard]

You don't need to prove finite-dimensionality if all you want to do is to state Faltings' theorem. And if you want to prove it then there are an awful lot of far more serious problems :-)

[Kevin Buzzard]

David Loeffler said:

"This function sends finite cardinals to the corresponding natural, and infinite cardinals to 0." :vomit:

When I define Nat.pred in front of the undergrads I always have pred 0 = 37, maybe you'd like this convention better?

[Joël Riou]

Joël Riou said:

I am currently thinking about making some progress about pullbacks of (pre)sheaves of modules.

The pullback of presheaves of modules is constructed in a series of PR #16755, #17389, #17388 and #17366. It needs some cleaning up, but #16755 and #17389 are ready for review.

[Joël Riou]

I now have very draft code for the sheaf of differentials of a morphism of schemes:
https://github.com/leanprover-community/mathlib4/pull/17471/files#diff-aee684e69be0f996df67f2d837d4531650486ecce319817b462cf7caa97e62e2R12-R15
(It follows from the construction of the relative differentials as a presheaf #17469 and the sheafification #17471.)

[Christian Merten]

@Michael Stoll, unfortunately a week to late for your last talk, but maybe in time for the next one:

import Mathlib

universe u

open CategoryTheory Limits AlgebraicGeometry

/-- A scheme `X` over a field `K` is geometrically irreducible, if it remains irreducible
after base changing along arbitrary field extensions of `K`. -/
class IsGeometricallyIrreducible {K : Type u} [Field K] (f : X ⟶ Spec (.of K)) : Prop where
  pullback_irreducibleSpace_of_field {L : Type u} [Field L] (i : CommRingCat.of K ⟶ .of L) :
    IrreducibleSpace ↑(pullback f (Spec.map i))

class IsNiceCurve [Field K] (f : X ⟶ Spec (.of K)) extends
  IsGeometricallyIrreducible f, IsProper f, IsSmoothOfRelativeDimension 1 f

compiles in Mathlib now.

[Michael Stoll]

Nice! (Pun intended...)

[Kevin Buzzard]

Great! I'll do curves at this workshop then!

[Kevin Buzzard]

Any ideas for projects greatly appreciated!

[Christian Merten]

I think a fun project would be developing the notion of IsGeometrically P where P is a morphism property with target Spec K, where of course the main examples of P should be the source is irreducible, connected or reduced. In particular to show that it suffices to check these on one algebraically closed extension following e.g. EGA IV.2, 4.3-4.6 first restricting to the affine case.

[Michael Stoll]

Kevin Buzzard said:

Any ideas for projects greatly appreciated!

Not sure how much work this still is, but defining the genus of a (nice) curve would be a worth while target.

[Michael Stoll]

What is the idiomatic way of defining the type of ($K$-)points on a nice curve over $K$? I.e., how to fill the second sorry below?

import Mathlib

open CategoryTheory Limits AlgebraicGeometry

/-- A scheme `X` over a field `K` is geometrically irreducible, if it remains irreducible
after base changing along arbitrary field extensions of `K`. -/
class IsGeometricallyIrreducible {K : Type u} [Field K] (f : X ⟶ Spec (.of K)) : Prop where
  pullback_irreducibleSpace_of_field {L : Type u} [Field L] (i : CommRingCat.of K ⟶ .of L) :
    IrreducibleSpace ↑(pullback f (Spec.map i))

class IsNiceCurve {K : Type u} [Field K] (f : X ⟶ Spec (.of K)) extends
  IsGeometricallyIrreducible f, IsProper f, IsSmoothOfRelativeDimension 1 f

structure NiceCurve (K : Type u) [Field K] where
  X : Scheme
  f : X ⟶ Spec (.of K)
  nice : IsNiceCurve f

lemma NiceCurve.isSmooth {K : Type u} [Field K] (X : NiceCurve K) : IsSmoothOfRelativeDimension 1 X.f :=
  X.nice.toIsSmoothOfRelativeDimension
-- etc.

def NiceCurve.genus {K} [Field K] (X : NiceCurve K) : ℕ := sorry

def NiceCurve.Points {K} [Field K] (X : NiceCurve K) : Type* := sorry

open NiceCurve

theorem Mordell {k X : Type} [Field k] [NumberField k] (X : NiceCurve k) (h : genus X ≥ 2) :
    Finite (Points X) := sorry

[Andrew Yang]

Maybe { f : Spec (.of K) ⟶ X // f ≫ X.f = 𝟙 _ } for now but in #18321 there is an attempt to add a thin wrapper around this.

[Kevin Buzzard]

So it looks like $H^0(X,\Omega^1)$ won't be ready by 16th Nov when the workshop starts. But what about $H^1(X,\mathcal{O}_X)$?

[Matteo Cipollina]

what about:

def NiceCurve.Points {K} [Field K] (X : NiceCurve K) : Type* :=
  { pt : Spec (.of K) ⟶ X.X // pt ≫ X.f = 𝟙 (Spec (.of K)) }

?

A K-point of a scheme X over K is a map from the "point" Spec K to X that respects the structure of X being defined over K. The commuting condition pt ≫ X.f = 𝟙 (Spec (.of K)) formalizes this "respecting the structure".