Fibered category, stacks in mathlib?

Stream: mathlib4

[Ma, Jia-Jun]

Is anyone planning to define the Fibered category in Mathlib4? The ultimate goal could be defining stacks and sheaves on stacks. BTW: Current mathlib4 already have enough preliminaries to define the notion.

[Paul Lezeau]

Hey @Ma, Jia-Jun ! @Calle Sönne and I have actually already defined stacks and some basic theory about fibered categories. There was some discussion here (https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Formalizing.20stacks) about this. We're currently working towards improving our definitions and API following suggestions that were made in that topic, and proving a version of the 2-Yoneda lemma. We do plan on PRing that stuff to mathlib once we think it's ready.

[Paul Lezeau]

Here's a link to the GitHub repo if you want to have a look: https://github.com/Paul-Lez/Stacks-project

[Paul Lezeau]

Once this is done, our plan is to formalize some deformation theory (Schlessinger, etc) following the exposition in the Stacks project (one of the goals is to get enough stuff about Galois deformations for @Kevin Buzzard's FLT project)

[Ma, Jia-Jun]

I am learning the basics about stacks now and found that reading code helps to clarify some subtle points compared to reading a book/notes. Thanks for sharing the repo @Paul Lezeau. I am looking forward to seeing your codes merging into Mathlib. :+1:

[Paul Lezeau]

@Ma, Jia-Jun glad that the code was helpful! If you're interested in participating in the deformation theory project (there should be a bit of (co)fibered stuff there too), let me know and I can ping you when we get started :)

[Ma, Jia-Jun]

Paul Lezeau said:

Ma, Jia-Jun glad that the code was helpful! If you're interested in participating in the deformation theory project (there should be a bit of (co)fibered stuff there too), let me know and I can ping you when we get started :)

That's cool. I am currently recruiting students to study lean. This could be suitable for some graduate students to work on. Please keep me updated. Thanks.

[Adam Topaz]

Ping @Calle Sönne

[Adam Topaz]

Oh, sorry I see that Calle was already pinged above. Sorry for the noise :-/