(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".

[Junyan Xu]

I think the following is a valid equivalent statement of Mordell conjecture: let A be a finitely type Q-algebra of trdeg=1 over Q which is an integral domain after base change to Qbar, whose FractionRing is not isomorphic to the FractionRing of Q[X,Y]/⟨f⟩ with f.totalDegree ≤ 3. Then the number of Q-homomorphisms from A to Q is finite. We could have this in Formal Conjectures today :)

[Damiano Testa]

I am not sure if I like or I am horrified by how you side-step the "genus at least 2" hypothesis!

[Damiano Testa]

By the way, your statement is not completely equivalent to the Mordell conjecture: all genus one curves without rational points are included in yours, but not in Mordell's.

[Damiano Testa]

You could of course say that it is not a cubic (or a conic!) geometrically, again.

[Kenny Lau]

Damiano Testa said:

You could of course say that it is not a cubic (or a conic!) geometrically, again.

i think that was the point of <= 3

[Kevin Buzzard]

If you have a smooth proj curve of genus 1 over a field k (even of char 0) with no k-points then you can't always realise it as a plane cubic.

[Kevin Buzzard]

The usual elliptic curve algorithm basically starts "choose a point and put it at infinity by writing down functions which have poles at this point"

[Kevin Buzzard]

I agree that Junyan's statement looks ok but probably the goal here should be to define genus (and curve!) rather than sidestepping it

[Junyan Xu]

By the way, your statement is not completely equivalent to the Mordell conjecture: all genus one curves without rational points are included in yours, but not in Mordell's.

This is a good point, but if you aim to prove there are finitely many rational points you can of course assume there's at least one. Also I think FractionRings of Q[X,Y]/⟨f⟩ with deg f ≤ 3 also covers some genus 1 curves of index 3 rather than 1 (⇔ existence of rational point) ($f=3X^3+4Y^3-5$ should be an example, and this paper shows that the index of a genus 1 curve over Q can be arbitrary).

[Michael Stoll]

Is it easy to use your suggested formal statement to deduce that the set of pairs $(\xi, \eta)$ of rational numbers such that $\eta^2 = \xi^5 + 37$ is finite?

(I.e., we not only want some statement of the result, but one that can be used to deduce other facts that might be of interest.)

[Kevin Buzzard]

Surely that's very hard, because we don't have a definition of genus :-)

[Michael Stoll]

That's the point! :slight_smile:

[Kevin Buzzard]

Angdinata and Xu faced a similar problem when proving associativity of the group law on a plane cubic -- injectivity of the map from the points to the class group boiled down to showing that there was no isomorphism between the function field and $K(t)$. They solved this problem in a low-level way, perhaps their ideas generalise?

[Michael Stoll]

We really will need a definition of the genus of a curve / function field with good API (so that we can for example show that the genus of a hyperelliptic curve $y^2 = f(x)$ with $f$ squarefree of degree $d$ is $\lfloor(d-1)/2\rfloor$).

[Kenny Lau]

A bit relevant is the Picard group, which is Xu's PR #21776 (a draft), and for the "correct" definition to work I also made #25249 to show that the category of finitely generated R-modules is essentially small (so please review!)

[Kenny Lau]

I know technically you can sidestep the Picard group since cl(A^1)=0, but I think it would still be nice to be able to state it formally in Lean

[Junyan Xu]

Starting from a function field, you can define g as d/2+1 where d is the degree of any canonical divisor, and it will be clearly invariant under isomorphisms of function fields.
Not sure how easy it is to compute it: we need to compute the order of a differential (KaehlerDifferential K K(C)) at each point (valuation) of the function field. For hyperelliptic curves we can probably prove and use Riemann--Hurwitz for the double cover.
Still have to show for deg f ≤ 3 we get genus 0 or 1.

[Andrew Yang]

I was about to ask if there is a proof without Riemann Hurwitz?

[Junyan Xu]

I think Riemann Hurwitz isn't too bad; the proof on Silverman is basically choosing a differential and compute.
image.png

[Kenny Lau]

It's also a bit subtler here (I just checked Silvermann), actually y^2 = x^5 + 37 here is singular at the point at infinity, so the correct curve doesn't actually live in P^2!

[Junyan Xu]

Angdinata and Xu faced a similar problem when proving associativity of the group law on a plane cubic -- injectivity of the map from the points to the class group boiled down to showing that there was no isomorphism between the function field and $K(t)$. They solved this problem in a low-level way, perhaps their ideas generalise?

It's interesting to note that the proof still works for singular Weierstrass curves whose function fields are isomorphic to $K(t)$. But here we are really defining the (geometric) genus as an invariant of the function field.

[Junyan Xu]

Actually Exercise 2.14 computes the genus of hyperelliptic curves :)

[Andrew Yang]

I am reading the first line of the statement and I (or lean) already cannot follow. Is there an easy proof (without some Zariski main-like argument) that all nonconstant maps between curves are finite? (or we could just assume this)

[Junyan Xu]

I think we probably don't need Hurwitz here after all. There are either one or two points at infinity on the hyperelliptic curve $y^2=f(x)$ depending on whether the degree of f is odd or even, and we'd just find appropriate uniformizers at the point(s) to compute the order of $dx/y$. On the affine plane the order is only nonzero at the roots of f.

[Junyan Xu]

all nonconstant maps between curves are finite

Do you mean the fibers are finite? I think in general one proves the sum of ramification indices equals the degree of the function field extension, so fibers have cardinality at most the degree.

[Kenny Lau]

@Junyan Xu I think you're still missing the fact that it's singular at the point(s) of infinity and so you have to embed it to P^(g+2) (which Exercise 2.14 did)

[Kenny Lau]

Junyan Xu said:

all nonconstant maps between curves are finite

Do you mean the fibers are finite? I think in general one proves the sum of ramification indices equals the degree of the function field extension, so fibers have cardinality at most the degree.

it's an equivalent statement, but I believe here it meant finite in the algebra sense where A -> B is "finite" := B is a finitely generated A-module, and then this definition can be generalised to schemes.

[Junyan Xu]

I'm hoping we can work with the function field without using an embedding, though the embedding probably helps you figure out what the uniformizers are.
There is always only one point at infinity if you don't resolve the singularity.

[Andrew Yang]

finite as in "affine + affine locally comes from finite ring homs", which is equivalent to "proper + finite fibers" under (some version of) zariski main.

[Kenny Lau]

Does the smooth curve still have function field Frac(Q[x,y]/(y^2-f(x)))?

[Junyan Xu]

I am reading the first line of the statement and I (or lean) already cannot follow.

Sorry, I should have asked what statement you're reading. The book excerpt I posted doesn't mention this finiteness notion apparently.

[Junyan Xu]

Does the smooth curve still have function field Frac(Q[x,y]/(y^2-f(x)))?

Yeah, resolution of singularities means finding a smooth projective variety with the same function field.

[Damiano Testa]

My comment above was simply intended to point out that I would not call that statement "the Mordell conjecture". I know that any two true statements are equivalent, so they are certainly equivalent and I also know that if a curve of genus 1 has a point, then it is isomorphic to a plane cubic. However, the (easy) argument that a curve not admitting points certainly has finitely many is "extra".

[Damiano Testa]

So, I was simply pointing out that I expected that in a repository called "Formal conjectures", the statement of the Mordell conjecture would be "strictly equivalent" to the Mordell conjecture, not "equivalent up to filling in a couple of extra easy steps".

[Junyan Xu]

So you are saying if I replace "whose FractionRing is not isomorphic to the FractionRing of Q[X,Y]/⟨f⟩ with deg f ≤ 3" by "whose FractionRing after base change to Qbar is not isomorphic to the FractionRing of Qbar[X,Y]/⟨f⟩ with deg f ≤ 3", then you would consider the statement the Mordell conjecture? There are harder "extra"s (like "if a curve of genus 1 has a point then it's isomorphic to a plane cubic" you pointed out) to show this is equivalent to the usual statement on Wikipedia, and it would be weird if we are free to use them but are not allowed to use simple logic. I think we could allow these arguments which are well known before the proof (or even formulation) of the Mordell conjecture, and still think the statement (an elementary form of) the Mordell conjecture. We just need appropriate docstrings documenting the non-obvious steps to show it's equivalent to the usual formulation.

[Damiano Testa]

I agree that eventually it becomes a matter of taste, but then why not also include all curves that have no points in your statement, instead of just some genus one curves with no points?

[Damiano Testa]

It really seems to me that the issue is that there is no definition of genus and, one way or another, this statement exposes the lack of this definition.

[Damiano Testa]

So, you could also say "If a smooth projective curve over Q has a point and it is not isomorphic to a plane curve of degree at most 3, then it only has finitely many points". This is another "variant" of the Mordell conjecture.

[Kevin Buzzard]

(connected)