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

[Calle Sönne]

Joël Riou said:

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.)

How would one show that the category is fibered here, given that there is a clivage such that the composition morphisms are isos? I don't see how this notion of HasClivage contains any information about morphisms between different fibers.

Also, thank you so much for the help with this so far! Me and @Paul Lezeau have now got a working notion of HasFibers like you suggested :)

[Joël Riou]

Let me give more details. According to SGA I VI 6.1, a functor is a "catégorie préfibrée" if the pullback functor exists for all morphisms in the base category. This can be formulated as a property of F (this could be phrased as a typeclass F.IsPrefibered : Prop).

Then, assuming F.IsPrefibered, one may extend [F.HasFibers] to define [F.HasClivage], which would be the data of such functors pullback f : Fib b ⥤ Fib b' for all morphisms f. Then, the pullback by an identity morphism is isomorphic to the identity functor, and the pullback functor by a composition of morphisms has a natural transformation from the composition of the pullback functors. These natural transformations satisfy certain coherence properties.

Then, one may define F.IsFibered : Prop by extending F.IsPrefibered and requesting that the composition of two cartesian morphisms is cartesian. Finally, one may prove that if we have F.HasClivage, then F.IsFibered iff the natural transformations which relate the composition of two pullback functors and the pullback by the composition for the given clivage are isomorphisms (this is SGA I VI 7.2).

[Calle Sönne]

Joël Riou said:

Let me give more details. According to SGA I VI 6.1, a functor is a "catégorie préfibrée" if the pullback functor exists for all morphisms in the base category. This can be formulated as a property of F (this could be phrased as a typeclass F.IsPrefibered : Prop).

Then, assuming F.IsPrefibered, one may extend [F.HasFibers] to define [F.HasClivage], which would be the data of such functors pullback f : Fib b ⥤ Fib b' for all morphisms f. Then, the pullback by an identity morphism is isomorphic to the identity functor, and the pullback functor by a composition of morphisms has a natural transformation from the composition of the pullback functors. These natural transformations satisfy certain coherence properties.

Then, one may define F.IsFibered : Prop by extending F.IsPrefibered and requesting that the composition of two cartesian morphisms is cartesian. Finally, one may prove that if we have F.HasClivage, then F.IsFibered iff the natural transformations which relate the composition of two pullback functors and the pullback by the composition for the given clivage are isomorphisms (this is SGA I VI 7.2).

Oh this is perfect, thanks a lot! I seem to have had the wrong impression of what IsPrefibered should mean, now it all makes sense.

[Calle Sönne]

Joël Riou said:

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

How did you deal with functoriality for t.HasHeart? Did you additionally require your functors to preserve the HasHeart structure, or was there some way to get around that? I looked around in mathlib for t-structures but I couldn't seem to find it, I guess you have the code in some separate repository somewhere?

[Calle Sönne]

Calle Sönne said:

Joël Riou said:

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

How did you deal with functoriality for t.HasHeart? Did you additionally require your functors to preserve the HasHeart structure, or was there some way to get around that? I looked around in mathlib for t-structures but I couldn't seem to find it, I guess you have the code in some separate repository somewhere?

(I should add that I know very little about t-structures, so maybe what I am saying about functoriality makes no sense.)

[Joël Riou]

I plan to PR t-structures to mathlib, but it will take a certain time... My draft code is in a mathlib branch https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
(In general, triangulated functors do not respect the heart of t-structures.)

[Calle Sönne]

Joël Riou said:

I plan to PR t-structures to mathlib, but it will take a certain time... My draft code is in a mathlib branch https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
(In general, triangulated functors do not respect the heart of t-structures.)

Thanks a lot!

[Calle Sönne]

Do anyone have any advice on how to define functoriality for this HasFibers class?

To recap what was said before, if we have a fibered category p : X ⥤ S (or just a functor) then p.HasFibers is defined as a collection of categories Fib s for each s : S equiped with functors ι s : Fib s ⥤ X such that the composition ι s ⋙ p is the constant functor mapping to S + the induced map to the normal fibers is an equivalence. So the point is that often there is a natural choice of fiber categories, e.g. for the fibered category of modules over the category of rings we would like the fiber over a ring R to be the category Mod R.

So far I have defined functors between different fibered categories p, q with p.HasFibers and q.HasFibers as a normal functor of fibered categories + functors between all the fiber categories p.Fib S and q.Fib S such that these are compatible with the functor on underlying fibered categories. Now this works decently, and I've managed to show that a functor is full resp. faithful iff all the functors between the fiber categories are. I've almost showed that this is true for equivalences of fibered categories as well.

The problem is that I feel its a bit annoying to have to define the functors on the fibers, as these are completely determined by the underlying functor on the fibered category anyways. Another alternative would be to define functors between p and q to be a functor of fibered categories + the condition that any element in the image of some p.Fib s gets mapped to something in the image of q.Fib s. From this one could reconstruct the functors on the fibers. This feels more convenient to verify when defining the functors, but I guess then the problem would be that the functor on the fiber categories would be quite inexplicit.

Does anyone have any ideas one what would be a good approach here? I think my problem is that I don't have enough experience with lean to tell if what I'm doing is unnecessarily complicated or not.

[Adam Topaz]

I would imagine you could phrase something in terms of docs#CategoryTheory.Pseudofunctor and morphisms of pseudofunctors. I don't really know much about the API for the (bi)category of pseudofunctors, assuming it even exists! I think @Yuma Mizuno is the correct person to ask.

[Calle Sönne]

Yeah, I feel HasFibers is really something in between fibered categories and pseudofunctors.

[Calle Sönne]

So maybe I should not define functors for the HasFibers class, but wait until I have HasClivage as well and in that setting associate a pseudofunctor for which its a lot more convenient to define functors in terms of the fibers

[Adam Topaz]

Can you define a pseudofunctor associated to an instance of HasFibers?

[Joël Riou]

I my understanding the data of a "functor" between two fibered categories (over the same base category) should not involve the data of HasFibers. But, when the source and target categories both have a clivage, it should make sense to state that the "global" functor is compatible with the extra data of a bunch of functors on the fibers (+ many compatibilities).

[Adam Topaz]

Oh I see, yeah I agree.

[Adam Topaz]

I honestly wasn’t sure what Calle meant about “functoriality” until I saw Joël’s message

[Adam Topaz]

BTW, it’s not clear to me that we should use the type class system for things like HasFibers. Why not just make a structure that bundles all the stuff for a fibred category over a given category C?

[Joël Riou]

Usually, we do not introduce two different cleavages for the same fibered category, so that using a class makes sense. Using structures would presumably be equally ok.

[Adam Topaz]

IIUC, a cleavage still contains data, and presumably one could talk about isomorphisms of such data, which could still be useful to talk about in the context of formalization.

[Johan Commelin]

@Sina 𓃵 You probably are interested in this thread

[Joël Riou]

Sure, but in a similar situation (actually a special case), a category C may be equipped with a shift by a monoid [HasShift C M] (the data of the shift functors can be understood as the cleavage for a fibered category), but we have not defined the notion of isomorphism between two shifts on the same category.

However, when we have a functor F : C ⥤ D between two categories equipped with a shift by M, I have formalized the type class F.CommShift M which expresses that F "commutes" with the shift (data of isomorphisms + compatibilites). This is an important notion (and what I suggest is a kind of generalization of this). Still, if we absolutely need to do that, we may say that two HasShift C M are isomorphic by constructing a F.CommShift M term for F the identity functor (with different shifts on the source and target).

[Calle Sönne]

Joël Riou said:

I my understanding the data of a "functor" between two fibered categories (over the same base category) should not involve the data of HasFibers. But, when the source and target categories both have a clivage, it should make sense to state that the "global" functor is compatible with the extra data of a bunch of functors on the fibers (+ many compatibilities).

Okay I agree that this would make more sense, but wouldnt you still want theorems about these global functors that says that its faithfull/full/an equivalence iff it is so on all the fibers? I guess maybe then I should just prove these statements in terms of the "canonical" fibers, and leave the HasFibers stuff for whenever I have a clivage also.

[Calle Sönne]

Because I guess its unnecessary to fix a clivage in order to prove these statements.

[Joël Riou]

Ok, there are three layers: 1) the fibered categories (as a functor), 2) the data of categories which are the fibers, 3) cleavages (the additional data of functors between the fibers).
The notion of functor F between two fibered categories (over the same base category) makes sense without any reference to 2) or 3), but when we have 2) + a compatibility of F and 2) [indeed 3) should not be necessary here], then there should be theorems like you mention.

[Paul Lezeau]

Re clivages, I will hopefully start working on these soon so we can start incorporating them in this stuff

[David Michael Roberts]

BTW, I've seen the phrase "cleaving" in place of the older "cleavage", which to my mind us a better term to use, for hopefully obvious reasons.

[Antoine Chambert-Loir]

They are only obvious to people who are enough fluent in non-mathematical English.

[Joël Riou]

And they are not present at all in the French word "clivage".

[Antoine Chambert-Loir]

Indeed.

[David Michael Roberts]

This is true, and yet the word 'cleavage' is a word for a part of female anatomy. Like the conference NeurIPS is no longer called NIPS, it is possible to change our terms of art.

Cleaving is a perfectly good synomym to my mind that carries no baggage whatsoever. :-)

[Antoine Chambert-Loir]

The Coq/Rocq change is another example of such a desirable move.

[Dean Young]

I'd like to post here about a few questions I have about stacks, maybe ones that can be answered from the work here:

• Bhatt-Scholze established a "pro-étale" site, but is there a "pro-flat" site? Is there a unification of the two different flat sites via the notion of pro (finite - presentation)?
• Faithfully flat maps are effective descent morphisms. Faithfully flat is equivalent to flat and flat-locally surjective. Do we have proofs of these?

[Scott Carnahan]

On the level of affine schemes, what ring-theoretic morphisms would a pro-flat site have that faithfully flat does not have? I would naively guess that flat is the same as pro-flat.

[Joël Riou]

The covers in the pro-étale site of X are defined as fpqc covers (involving weakly-étale schemes over X). Then, I do not think that there is a thing called "pro-flat".