Formalizing stacks

Stream: maths

[Calle Sönne]

Me and @Paul Lezeau are going to try to formalize stacks. We are wondering in what generality to write things. Is there any point in proving things about fibered categories in general? Or can we just immediately prove things (like 2-Yoneda lemma) about categories fibered in groupoids. I don't have too much experience with these things, but I have only ever seen fibered categories being used to talk about stacks, and then one only needs categories fibered in groupoids anyways. If anyone has more experience with these things, it would be great to hear your opinion.

For example, in these notes: https://sites.math.washington.edu/~jarod/moduli.pdf they never introduces fibered categories, and instead only works with categories fibered in groupoids (which are called prestacks there).

[Ruben Van de Velde]

Adding something to mathlib often teaches you generalisations you might never have heard of otherwise :)

[Joël Riou]

I think it is important to formalize fibered categories in general! The notions of descent of morphisms (for a covering family for a certain topology) and effectiveness of descent make sense in this context, and having this in general would be very useful eventually (e.g. in order to formulate and obtain faithfully flat descent).

[Adam Topaz]

@Calle Sönne what level of generality are you aiming for? What sort of stacks are you planning on constructing? Will you try to construct any examples?

[Adam Topaz]

For example, do you want to go down the following rabbit hole? https://ncatlab.org/nlab/show/stack

[Calle Sönne]

Adam Topaz said:

Calle Sönne what level of generality are you aiming for? What sort of stacks are you planning on constructing? Will you try to construct any examples?

I don't really plan to do any higher categorical stuff (because I don't know so much about it), so only 1-stacks. I also haven't thought of any good examples yet, since they are all feel quite complicated to formalize, apart from the empty stack.

[Reid Barton]

Are you planning to use Grothendieck fibrations? I think they will not keep some of their advantages when formalized because they involve equalities of objects

[Reid Barton]

There's also the notion of "displayed category" that would be appropriate here, but I don't think mathlib has it
https://ncatlab.org/nlab/show/displayed+category

[Adam Topaz]

I thought someone was working on displayed categories... Maybe @Junyan Xu ?

[Junyan Xu]

Mathlib currently has docs#CategoryTheory.OplaxFunctor because I urged @Yuma Mizuno to generalize pseudofunctors that he already had. My original motivation to work on the Grothendieck construction is to show the category of schemes has all small limits, and I later thought about connections with "dependent functors" (which sheaves of modules are). I was able to show the existence of colimits in the total category from the existence in the base and fiber categories, but I haven't touched these for a long time, and there are only various abandoned mathlib3 branches that haven't been ported to Lean 4. I know near to nothing about stacks, so these are probably all that I can help for now!

[Paul Lezeau]

Reid Barton said:

Are you planning to use Grothendieck fibrations? I think they will not keep some of their advantages when formalized because they involve equalities of objects

Calle and I have already had a few annoying encounters with equalities of objects actually so if there are ways to avoid those, I'd be quite interested!

[Joël Riou]

In order to formalize fibered categories, I think that part of the API should be focused on functors F : E ⥤ B and properties of morphisms (cartesian maps, etc.), and some Prop typeclasses could be introduced like F.IsPrefibered, F.IsFibered, etc.

[Joël Riou]

Then, when we want to introduce the "fibres" of F, instead of relying only on equalities, I think that we should allow the user to provide a bunch of categories Fib b for all b : B equipped with functors Fib b ⥤ E satisfying suitable conditions (we may not necessarily require that the composition Fib b ⥤ E ⥤ B is equal to the constant functor, but we may instead require that there is an iso, etc.). This could be part of a type class [F.HasFibres], for which the API should also provide a constructor which would just take the inverse image by F of the identity of b.

[Joël Riou]

Assuming [F.HasFibres], one may introduce a typeclass containing the data of the inverse image functors Fib b ⥤ Fib b' and the data of the composition morphisms satisfying the expected cocycle conditions: this would be [F.HasClivage]. Then, one may show F.IsFibered iff the composition morphisms are isos. (Here again, given a prefibered category such that [F.HasFibres], we should provide a constructor for F.HasClivage.)

[Joël Riou]

Then, for the applications, e. g., the fibered category of modules over various commutative rings, we could declare an instance of HasFibres for which, by definition, the fibres would be the category of R-modules for a given commutative ring R. The base change functors that we already have for the categories of R-modules could be made part of a HasClivage instance, etc. Doing so, we could easily relate the abstract results and their more concrete applications. Otherwise, transfering properties via equivalence of categories could be painful...

[Joël Riou]

(Similarly, in my formalization of t-structures on triangulated categories, I have defined a type class t.HasHeart where the user may provide a category and an embedding into the triangulated category. Doing so, I may ensure that the heart of the derived category of an abelian category A is the category A, by definition! Otherwise, I would have to compose with equivalences of categories... I think we could do similar things for fibered categories.)

[Reid Barton]

Paul Lezeau said:

Reid Barton said:

Are you planning to use Grothendieck fibrations? I think they will not keep some of their advantages when formalized because they involve equalities of objects

Calle and I have already had a few annoying encounters with equalities of objects actually so if there are ways to avoid those, I'd be quite interested!

I guess options that come to mind are

1. Grothendieck fibrations, and just live with eqToHom annoyances that arise from writing down the definition in intensional type theory.
2. Street fibrations, which will have the same definition except that an eqToHom is replaced by an arbitrary isomorphism.
3. Displayed categories, which I am now realizing will probably also be inconvenient in Lean because they involve dependent equalities/"pathovers" in the axioms (e.g. associativity).

The "real" definition is that a prestack is a pseudofunctor to the 2-category of groupoids (or of categories, or ...). I'm not sure why the definition in terms of fibrations stuck in algebraic geometry, but in any case, both will be needed at some point.

[Reid Barton]

I feel like the Street fibration approach shouldn't be too bad, even though the nLab describes them as "fairly cumbersome", and it seems strictly(?) better than using Grothendieck fibrations, in the context of Lean.

[Paul Lezeau]

Fair enough! I think what we've done so far falls under the 1st option - we've managed to figure out how to deal with some of the eqToHom annoyance - but later something else would be better

[Calle Sönne]

Joël Riou said:

Then, when we want to introduce the "fibres" of F, instead of relying only on equalities, I think that we should allow the user to provide a bunch of categories Fib b for all b : B equipped with functors Fib b ⥤ E satisfying suitable conditions (we may not necessarily require that the composition Fib b ⥤ E ⥤ B is equal to the constant functor, but we may instead require that there is an iso, etc.). This could be part of a type class [F.HasFibres], for which the API should also provide a constructor which would just take the inverse image by F of the identity of b.

Thanks a lot for these replies!! I'm still quite new to making APIs in lean, so these suggestions really help. If I understand correctly, HasFibers should essentially substitute fibered categories? So I state most of my theorems in terms of HasFibers instead ?

[Joël Riou]

I am not so sure this is what I meant. If F : E ⥤ B, we may be tempted to define for each b : B a category F.fibre' b by taking those object X : E such that F.obj X = b (or with the data of an iso, whichever design choice you prefer), and then formalise the definition of functors F.fibre' b ⥤ F.fibre' b' when F is a fibered category. I am suggesting a different design where the user may provide the data of such fiber categories F.fibre b for a given functor F, and would be the [F.HasFibers] typeclass. (Of course, we should have equivalences between F.fibre b and F.fibre' b.

My concern is that if we take typical examples: B the category of rings (or its opposite category) and E the category of modules over rings, as a category over B, then we already have natural candidates for the "fiber" categories: for each ring R, this is the category ModuleCat R. Then, the fibered category should be able to work directly with these ModuleCat R without the mediation of an equivalence of categories.

What I suggest is to define a typeclass Is(Pre)FiberedCategory, construct a HasFibers as a definition (not an instance), and for the subsequent constructions, add an [F.HasFibers], provide a HasClivage definition, and subsequently add the [F.HasClivage] assumption.

[Calle Sönne]

Joël Riou said:

I am not so sure this is what I meant. If F : E ⥤ B, we may be tempted to define for each b : B a category F.fibre' b by taking those object X : E such that F.obj X = b (or with the data of an iso, whichever design choice you prefer), and then formalise the definition of functors F.fibre' b ⥤ F.fibre' b' when F is a fibered category. I am suggesting a different design where the user may provide the data of such fiber categories F.fibre b for a given functor F, and would be the [F.HasFibers] typeclass. (Of course, we should have equivalences between F.fibre b and F.fibre' b.

My concern is that if we take typical examples: B the category of rings (or its opposite category) and E the category of modules over rings, as a category over B, then we already have natural candidates for the "fiber" categories: for each ring R, this is the category ModuleCat R. Then, the fibered category should be able to work directly with these ModuleCat R without the mediation of an equivalence of categories.

What I suggest is to define a typeclass Is(Pre)FiberedCategory, construct a HasFibers as a definition (not an instance), and for the subsequent constructions, add an [F.HasFibers], provide a HasClivage definition, and subsequently add the [F.HasClivage] assumption.

Oh okay, but in such examples wouldn't one want to consider the pseudo-functor instead?

[Joël Riou]

I think we would like to be able to relate fibered categories and clivages.

[Calle Sönne]

Yeah but shouldn't I then prove some theorems about relating fibered category + clivage to a pseudo-functor?

[Joël Riou]

Absolutely. Results which can be phrased purely in terms of the fibered category F can be stated and proved this way, and statement involving the inverse image functor for this fibered category should be phrased under F.HasFibers or F.HasClivage.

[Calle Sönne]

Joël Riou said:

Absolutely. Results which can be phrased purely in terms of the fibered category F can be stated and proved this way, and statement involving the inverse image functor for this fibered category should be phrased under F.HasFibers or F.HasClivage.

Oh okay I might understand more what you're saying now. So F.HasFibers should basically be a category F.fiber b for every b, and these should come with equivalences to F.preimagefiber b? And basically I just need to prove all my statements about the inverse image functor pass through equivalences, so the user doesn't have to do that each time. Or is the equivalence with the preimage fiber already too cumbersome somehow? And I should phrase it some other way?

[Joël Riou]

That is essentially what I suggest. Instead of the data of an equivalence of categories, the data for each F.fiber b might be implemented as the data of a functor i b : F.fiber b ⥤ E with an isomophism i b ⋙ F with the constant functor b, and the property that the induced functor to F.preimagefiber b is an equivalence. Then, all you subsequent constructions could be done as much directly with F.fiber b rather than F.preimagefiber b so that you would not even need to pass through equivalences!

[Calle Sönne]

Joël Riou said:

That is essentially what I suggest. Instead of the data of an equivalence of categories, the data for each F.fiber b might be implemented as the data of a functor i b : F.fiber b ⥤ E with an isomophism i b ⋙ F with the constant functor b, and the property that the induced functor to F.preimagefiber b is an equivalence. Then, all you subsequent constructions could be done as much directly with F.fiber b rather than F.preimagefiber b so that you would not even need to pass through equivalences!

Ohhhh okay. Thank you so much! I will try to implement this :)

[Calle Sönne]

Joël Riou said:

That is essentially what I suggest. Instead of the data of an equivalence of categories, the data for each F.fiber b might be implemented as the data of a functor i b : F.fiber b ⥤ E with an isomophism i b ⋙ F with the constant functor b, and the property that the induced functor to F.preimagefiber b is an equivalence. Then, all you subsequent constructions could be done as much directly with F.fiber b rather than F.preimagefiber b so that you would not even need to pass through equivalences!

Sorry, I actually still don't understand this. What is this induced morphism to F.preimagefiber b you are thinking of? I see a non-canonical morphism given by taking pullbacks over the natural isomorphism to the constant functor, but this involves a lot of choices. Also, wouldn't requiring the user to show that this induced morphism is an equivalence also just be the same amount of work as forcing the user to supply an equivalence with F.preimagefiber b in the first place?

Maybe I should try to "axiomatize" the properties that a Fib b should satisfy without mentioning the preimage fiber. So for example, as you suggested it would be the data of a functor i b : Fib b ⥤ E with an isomorphism i b ⋙ F to the constant functor b. I would then also demand that one can choose pullbacks compatible with Fib in a suitable way, that the functors are faithful, jointly surjective and possible some more axioms as I need them. But again I don't know how much less work this would be than just forcing the user to just supply the equivalence in the first place.

[Joël Riou]

If F.preimagefiber b consists of X : E equipped with an iso between F.obj X and b, then with the data I suggest, we have a canonical functor Fib b ⥤ F.preimagefiber b.

[Paul Lezeau]

@Calle Sönne and now have set up a basic theory of fibered categories and we now have a definition of Stacks here if anyone is interested in having a look!

We're hoping to eventually PR some of this stuff to mathlib so any feedback would be more than welcome!

At the moment, stating the stack condition is quite cumbersome (notably because of a lot of canonical isomorphism having to be used to identify various objects), so there's probably a lot of room for improvement. One idea Calle and I have been discussing is defining a data type descent data and constructing some API about it.

[Paul Lezeau]

For instance we could have a predicate saying when the descent data is effective, which would correspond to the objects_glue condition in our definition

[Junyan Xu]

Note that #8661 introduces SheafDescentData
and there are docs#AlgebraicGeometry.SheafedSpace.GlueData etc. too, which might be unified under the same framework.

[Joël Riou]

About descent data, in a draft PR #8661 I formalize the fact that sheaves can be glued: if (C, J) is a site and Y : I → C are objects which "cover the final object", then there is an equivalence of categories between the category of sheaves over C and a category SheafDescentData whose objects consists of families of sheaves over each of the sites Over (Y i) equipped with a descent data (i.e. isomorphisms which satisfy some compatibilites...), see https://github.com/leanprover-community/mathlib4/pull/8661/files#diff-fdd776e556488ad2ff22be948bb4fbccc55fbb4c7871ba7be6f82eab205f3a4aR74-R94 . With some modifications, similar definitions could be done for general fibered categories.

[Paul Lezeau]

Oh that sounds great! I was hoping someone had come up with a neater way to package this type of information!

[Paul Lezeau]

Calle and I will try and adapt our stuff to the framework you've set up