Chow's Lemma

Stream: Is there code for X?

[Aniruddh Venkatesan]

I have the ambitious goal of formalizing GAGA, and as a first step I'd like to first formalize Chow's lemma. Has this been done yet? And if it has, has any further progress been made towards formalizing GAGA?

[Edward van de Meent]

iirc @Raphael Douglas Giles is doing things in that direction

[Raphael Douglas Giles]

I haven’t worked on formalizing Chow’s lemma (I was doing some stuff on Chow groups/rings a little while ago which might be what you’re thinking of). I think a couple of people have talked about formalizing GAGA, but I’m not sure anyone is actively working on it. Afaik nobody’s done Chow’s lemma yet, and it would be great to have if you’re keen to work on it :)

[Edward van de Meent]

Ah, thanks for correcting! :+1:

[Aniruddh Venkatesan]

Sounds good, thanks! Seems like some standard facts about morphisms of schemes are missing from mathlib too, (e.g valuative criteria), is there anyone working on these? Otherwise I'm happy to start with these more basic facts as well.

[Andrew Yang]

Valuative criteria is docs#AlgebraicGeometry.IsProper.eq_valuativeCriterion

[Andrew Yang]

I'm not entirely sure if Chow's lemma is the right thing to start on if you want GAGA though. IMHO you could first prove it for projective varieties and then worry about relaxing the hypothesis later.

[Antoine Chambert-Loir]

In the direction of GAGA theorem, there seems to be several major preliminary work to do. How far is mathlib from defining analytic spaces, proving Cartan's theorems A and B, and proving finiteness of coherent cohomology on projective schemes?

[Andrew Yang]

I don't think there is any big obstacle on defining complex analytic spaces -- unless they are not the mathlib-correct definition and one should work with something more general (e.g. works for nonarchimedean fields) that I am not aware about.

[Andrew Yang]

And after this I think a good first target would be to define the analytification functor. There shouldn't be any big obstacle here as well.

[Andrew Yang]

... and then we might be able to state GAGA (depending on your formulation)
We are quite far from proving it though. In particular we don't have a working theory of Cech cohomology on schemes let alone complex analytic spaces. We also don't have a working theory of projective spaces (e.g. we don't even have $\mathcal{O}(1)$).

[Aniruddh Venkatesan]

Hmm, I guess I can start with complex analytic spaces and the analytification functor then. Is there anyone currently working on projective spaces and/or cohomology? Would be happy to contribute there as well if necessary.