geometric representation theory

Stream: Is there code for X?

[Andrea Bourque]

Is there code for perverse sheaves, or other geometric representation theory topics like the affine Grassmannian and affine flag variety of an algebraic group?

[Scott Morrison]

Sadly not!

[Andrea Bourque]

Scott Morrison are you interested in developing it? Or know anyone else who is interested in developing it?

And/or do you know what kinds of things would need to be developed first? I.e. one would need derived categories and the notions of constructibility for perverse sheaves. And I don't know how much of algebraic groups have been developed, but the affine Gr and Fl are ind-varieties, so that might pose a challenge.

[Scott Morrison]

I'm certainly not going to be doing this. But it would be fun. :-)

@Joël Riou is the one to say how much of derived categories we have. (I think: we don't have them yet, but should be very close.)

Sadly algebraic groups have not even been defined, and ind-varieties I think have many steps missing before even the definition.

[Kevin Buzzard]

I think we need varieties before ind-varieties. We have schemes but nobody ever specialised to schemes of finite type over a field

[Joël Riou]

The triangulated structure on the homotopy category of cochain complexes shall soon be in mathlib (#9032). It will take slightly more time to PR my code for the derived category. On a branch, I have code for t-structures (including the fact that the heart of a t-structure is an abelian category).

In order to obtain the derived category, I will need the more general localization theorem for triangulated categories. One of the technical steps will be that the localization of an additive category C with respect to a suitable class of morphism is still additive, and for that I shall incidentaly use notions of "(abelian) group objects" in a category, which would also be useful in order to define group schemes as group objects in the category of schemes.

[Kevin Buzzard]

Algebraic groups are something we're going to have to come to terms with at some point but I still don't know the best way to define them, or more generally how best to do group schemes. There are several different ways of thinking about them but we'll need to choose one. I need finite flat group schemes for Fermat so this will come up sooner rather than later

[Andrea Bourque]

Kevin Buzzard said:

I think we need varieties before ind-varieties. We have schemes but nobody ever specialised to schemes of finite type over a field

Surprising

[Kevin Buzzard]

It's just a matter of getting someone to do it. Natural targets would be a basic theory of curves (including relations to valuations on the function field) and a theory of dimension of a variety. But nobody needed these for any project so far so nobody did them. I have PhD students working on dimension theory

[Andrea Bourque]

Fair enough. If I was more comfortable with AG and had more time on my hands, I would try it.

[Junyan Xu]

Mathlib recently got docs#Coalgebra and people has tried Hopf algebras before. So I guess we are not that far from affine algebraic groups?

[Kevin Buzzard]

Well we're not that far from some definition which is equivalent to affine group schemes, but there will still be some glue to get the word scheme involved, and some finiteness issues before we have affine algebraic groups. And then it will still be a challenge to construct the algebraic group associated to an elliptic curve. For Fermat I was going to just deal with all of this in an ad hoc way because I only need results for inner forms of GL(2) and for finite (hence affine) group schemes