Extensive Coverage

Stream: maths

[Riccardo Brasca]

The following came up In Copenhagen.

We have in mathlib the notion of docs#CategoryTheory.FinitaryExtensive. So let C be a category that is Finitary Extensive. I want to define a docs#CategoryTheory.Coverage as follows

def ExtensiveSieve  (B : C) := { S | ∃ (α : Type) (_ : Fintype α) (X : α → C)
  (π : (a : α) → (X a ⟶ B)),
    S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π) }

def ExtensiveCoverage  : Coverage C where
  covering B :=   ExtensiveSieve B
  pullback := sorry

If I understand the literature the condition "Finitary Extensive" means exactly (or at least implies) that the sorry can be filled. Does anyone know if this correct?

Tagging @Dagur Ásgeirsson @Filippo A. E. Nuccio @David Michael Roberts that may be interested

[Adam Topaz]

I would define it inductively... let me sketch something

[Riccardo Brasca]

Another question is if the definition of ExtensiveSieve looks good: we want to express the idea that coverings are given by disjoint unions.

[Adam Topaz]

import Mathlib.CategoryTheory.Sites.Coverage

open CategoryTheory Limits

variable (C : Type _) [Category C]

inductive extensiveCoverAux : (B : C) → Presieve B → Prop
  | mk (α : Type) [Fintype α] (X : α → C) [HasCoproduct X] :
      extensiveCoverAux (∐ X) (Presieve.ofArrows _ <| Sigma.ι X)

def extensiveCoverage : Coverage C where
  covering := extensiveCoverAux C
  pullback := sorry -- need extensive

[Andrew Yang]

I plan to remove docs#CategoryTheory.Extensive in favour of docs#CategoryTheory.FinitaryExtensive in a WIP PR #7731.

Not 100% sure this change is desired. FinitaryExtensive is stronger than Extensive as
the former requires furthermore that coproducts satisfy some form of descent.
However the former is what the literature uses and has some better properties (e.g. coproducts are disjoint).
Suggestions Welcome!

[Dagur Asgeirsson]

I came to the conclusion that something like this (at least adding the condition that coproducts are disjoint) would be a good idea recently when working on #6877. Our Extensive was enough to define the coverage and prove that finite-product-preserving presheaves are sheaves, but when trying to prove that sheaves preserve finite products I ran into issues.

However, I do think we should keep the old Extensive (perhaps renamed as PreExtensive or something), precisely because that's enough to define the coverage etc. Also, I think the old Extensive + coproducts are disjoint is enough to prove what I want to do in #6877 (sheaves preserve finite products), but I'm not sure.

[Andrew Yang]

Old Extensive + all finite coproducts are disjoint should be precisely FinitaryExtensive.

[Riccardo Brasca]

@Dagur Asgeirsson at the moment there is no relation between docs#CategoryTheory.FinitaryExtensive and docs#CategoryTheory.Extensive, right?

[Andrew Yang]

If the old Extensive is still desired, I would be inclined to redefine it as

class PreExtensive (C : Type u) [Category.{v} C] : Prop where
  [hasFiniteCoproducts : HasFiniteCoproducts C]
  [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f]
  is_universal : ∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsUniversalColimit c

(which should be equivalent to the current one)

[Andrew Yang]

However I don't have any example of "pre-extensive" categories (that aren't extensive).

[Dagur Asgeirsson]

Riccardo Brasca said:

Dagur Asgeirsson at the moment there is no relation between docs#CategoryTheory.FinitaryExtensive and docs#CategoryTheory.Extensive, right?

At the moment, no. But Andrew's PR gives that link, for example FinitaryExtensive.sigma_desc_iso on line 897 in Mathlib/CategoryTheory/Extensive

[Dagur Asgeirsson]

Andrew Yang said:

  is_universal : ∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsUniversalColimit c

Is is_universal really equivalent to the old sigma_desc_iso?

[Riccardo Brasca]

Well, if you think that going down the rabbit hole of finding the right categorical generalization to characterize sheaves is doable this is surely the right approach.

[Riccardo Brasca]

(I am almost sure there must be something like a regular category notion that takes care of covering of the other type, but the math is less clear)

[Dagur Asgeirsson]

I'm pretty sure I just need coproducts to be disjoint to be able to prove that sheaves preserve finite products, which completes the characterisation of sheaves.

[Dagur Asgeirsson]

Our Preregular is the right notion for the other type

[Dagur Asgeirsson]

#6919 now has both directions there

[Andrew Yang]

Dagur Asgeirsson said:

Is is_universal really equivalent to the old sigma_desc_iso?

IsUniversalColimit is just a fancy way of saying "stable under pullbacks".
And the proposed change has the benefits

1. Parity with Extensive.
2. It doesn't mention a particular colimit obtained by choice.
3. It should be easier to show that binary coproducts are stable under pullbacks.

[Riccardo Brasca]

Dagur Asgeirsson said:

Our Preregular is the right notion for the other type

So docs#Stonean.effectiveEpiFamily_tfae is used only to prove an abstract categorical notion and then the proof that a presheaf is a sheaf for the coherent topology iff the two conditions hold (one is automatic in this case of course) is completely general?

[Dagur Asgeirsson]

Yeah my claim is the following:

Let C be a category which is FinitaryExtensive, Preregular and Precoherent (the last one probably follows from the other two, but we haven't proved that).

1. If every object of C is projective (e.g. in C = Stonean) then coherent sheaves are precisely the presheaves that preserve finite products.

2. If C has the relevant pullbacks (e.g. C = CompHaus or C = Profinite), then coherent sheaves are precisely the presheaves that preserve finite products, and satisfy EqualizerCondition.

We already have one direction, but to prove that sheaves preserve finite products, I need coproducts to be disjoint.

[Riccardo Brasca]

Very nice! I thought we still used the explicit description of (effective/regular/whatever) epi in our three examples to prove the final theorem.

[Riccardo Brasca]

BTW I think this deserves a short paper somewhere. It's probably more or less known, but I bet it's not very easy to find someone who's sure about all the details.

[Dagur Asgeirsson]

Riccardo Brasca said:

Very nice! I thought we still used the explicit description of (effective/regular/whatever) epi in our three examples to prove the final theorem.

We did that originally, but I extracted a proof for the more general setting from what we had!

[Dagur Asgeirsson]

I've opened #7804, it's sorry-free but still needs some cleaning up. It's what we need to prove that extensive sheaves preserve finite products. It basically says that if a presheaf isSheafFor the empty presieve and a Presieve.ofArrows, then it preserves the product corresponding to the Presieve.ofArrows.

[Dagur Asgeirsson]

#7949 proves that sheaves for the extensive topology on a category which is Extensive and has disjoint finite coproducts (stated in terms of Sigma.ι, not CoproductsDisjoint, sorry), are precisely the presheaves which preserve finite products

[Dagur Asgeirsson]

@Andrew Yang what's the status of your PR which removes Extensive?

[Andrew Yang]

A prerequisite (#7745) just got merged today. I'll tidy up the PR soon.

[Dagur Asgeirsson]

Ok, how much more work would it be for you to add the other direction of the equivalence of FinitaryExtensive iff old extensive plus disjoint coproducts? The forward direction is already there as I understand?

[Andrew Yang]

Do we need the inverse direction? Also we only know that binary coproducts are disjoint. I'll try to generalize it to finite coproducts.

[Andrew Yang]

I'm still not sure if we need the notion of "pre-extensive" though. I don't think there is any literature on this and I cannot find any examples that are not extensive.
Even if this condition is enough for the extensive coverage to be a coverage, it is only well behaved when the category is extensive.

[Dagur Asgeirsson]

Andrew Yang said:

Do we need the inverse direction? Also we only know that binary coproducts are disjoint. I'll try to generalize it to finite coproducts.

I'm just wondering because I already have proofs at #6731 that CompHaus, Profinite and Stonean are Extensive.

[Dagur Asgeirsson]

Depends what you mean by well-behaved. Pre-extensive is enough to define the coverage, and to prove that all finite-product preserving functors are sheaves (but not the converse)

[Dagur Asgeirsson]

Shouldn't we always define things in the most general way possible in mathlib?

[Ruben Van de Velde]

As general as possible, but no more

[Dagur Asgeirsson]

There is also this annoying thing with binary vs finite products. It seems that basically the only properties of products which mathlib knows is equivalent for binary and empty on the one hand and finite on the other hand is existence and being preserved by functors. And it's pretty difficult to relate them.

In my PRs about preserving finite products (#7949 and the ones it depends on), I always use general products, and specialize to finite ones when I have to. This means that the results can easily be generalised to infinitary extensive categories etc.

Is there a good reason why FinitaryExtensive is defined in terms of binary and not finite coproducts? I don't really see how binary coproducts are "easier" than finite ones, it's just harder to relate them to general products. Because binary products aren't products in mathlib, they're binary products, while finite products are just products with the extra property of being finite.

[Andrew Yang]

The only reason why FinitaryExtensive was defined in terms of binary coproducts is that I only needed binary coproducts back then. If #7731 lands, we will have all the properties for finite coproducts as well and I don't think the definition matters a lot after that?

[Andrew Yang]

Is there any "pre-extensive" category though? If not, this notion is not more general but merely redundant IMO.

[Andrew Yang]

Dagur Asgeirsson said:

I'm just wondering because I already have proofs at #6731 that CompHaus, Profinite and Stonean are Extensive.

If the inverse direction is needed for the proofs I could add them.

[Andrew Yang]

But note that mathlib already knows that TopCat is extensive and reflective subcategories of extensive categories are extensive.

[Dagur Asgeirsson]

Yes, something like that would be much better than the proofs I already have

[Dagur Asgeirsson]

Andrew Yang said:

The only reason why FinitaryExtensive was defined in terms of binary coproducts is that I only needed binary coproducts back then. If #6731 lands, we will have all the properties for finite coproducts as well and I don't think the definition matters a lot after that?

You mean if #7731 lands?

[Andrew Yang]

Andrew Yang said:

But note that mathlib already knows that TopCat is extensive and reflective subcategories of extensive categories are extensive.

Specifically #7721 (it is on bors queue)

[Dagur Asgeirsson]

Ah you need pullbacks in the result about reflective subcategories though. Do you think that could be weakened to what I call HasPullbacksOfInclusions on the target category (i.e. has those pullbacks where one morphism is an iota map into a finite coproduct)?

[Dagur Asgeirsson]

Stonean doesn't have pullbacks but it HasPullbacksOfInclusions

[Dagur Asgeirsson]

Re pre-extensive: I guess I just think about the property of being extensive as two distinct properties (one being pre-extensive, i.e. coproducts are preserved by pullback, and the other being that finite coproducts are disjoint). But I realise this is not the definition of FinitaryExtensive

[Andrew Yang]

Dagur Asgeirsson said:

Ah you need pullbacks in the result about reflective subcategories though. Do you think that could be weakened to what I call HasPullbacksOfInclusions on the target category (i.e. has those pullbacks where one morphism is an iota map into a finite coproduct)?

Should be possible. Will try once #7721 lands in mathlib.

[Dagur Asgeirsson]

If I get disjoint finite coproducts then I'll be very happy to see #7731 merged. I would still argue for keeping what I call Extensive as PreExtensive but I don't feel that strongly about it. It adds a nice symmetry with Precoherent and Preregular which were notions we kind of just invented for mathlib, so I don't see there not being any literature on it as an argument against it.

[Dagur Asgeirsson]

If you don't add disjoint finite coproducts (that's of course fine, I won't make you do anything), just hold off a bit on changing the file CategoryTheory/Sites/RegularExtensive, so I can try to add it in #7949

[Andrew Yang]

Andrew Yang said:

Should be possible. Will try once #7721 lands in mathlib.

I took a quick look and the bare minimum my proof needs is the fact that the left adjoint preserves pullbacks of the form $R(X) \xrightarrow{R(f)} R(L(Y)) \xleftarrow{\eta_Y} Y$ for any $f : X \to L(Y)$. This seems to be an iff per theorem 4 of this preprint so this might be the best one can do.

[Andrew Yang]

#7731 already has disjoint finite coproducts.

[Riccardo Brasca]

I agree with @Dagur Asgeirsson to keep Extensive as PreExtensive, especially since it is already there and it is more general (we have plenty of examples in mathlib where we are much more general that any reasonable literature). Maybe FinitaryExtensive can become Extensive?

[Riccardo Brasca]

What is the mathematical difference between the two?

[Dagur Asgeirsson]

The mathematical difference is that Pre-extensive doesn't require disjoint coproducts

[Dagur Asgeirsson]

Andrew Yang said:

#7731 already has disjoint finite coproducts.

I thought you said only binary?

[Riccardo Brasca]

OK, so I indeed think it is mathematically irrelevant, but who knows, let's keep both of them.

[Andrew Yang]

Dagur Asgeirsson said:

Andrew Yang said:

#7731 already has disjoint finite coproducts.

I thought you said only binary?

Yeah but I added it yesterday.

[Riccardo Brasca]

Where is the fact the CompHaus and friends are Extensive/Preextensive? Is it in a PR?

[Dagur Asgeirsson]

It’s in #6731 (unpolished). But for Comphaus and Profinite, we can now deduce it from abstract nonsense. We might still have to do it directly for Stonean though

[Andrew Yang]

I managed to show Stonean is extensive using abstract nonsense as well. See #8012.

[Riccardo Brasca]

Are you modifying again FinitaryExtensive? Maybe you can split the PR into two, where in the first one you don't touch CompHaus and friends?

[Andrew Yang]

The class it self was not changed. I just pulled a field out into a new definition.

[Andrew Yang]

I've splitted the Extensive part of the PR into #8015.

[Dagur Asgeirsson]

Wow, thanks Andrew! This looks great, I'll take a closer look either in a couple of hours or tomorrow. I'll also update #7949 with the new pre-extensive/extensive definitions. When #7949 and #8012 are merged we basically have the explicit description of condensed sets!

[Riccardo Brasca]

#8015 is merged.

[Riccardo Brasca]

BTW, the docstring of docs#CategoryTheory.FinitaryPreExtensive and docs#CategoryTheory.FinitaryExtensive are identical...

[Andrew Yang]

Riccardo Brasca said:

#8015 is merged.

Great! #8012 is now ready for review.

[Andrew Yang]

Riccardo Brasca said:

BTW, the docstring of docs#CategoryTheory.FinitaryPreExtensive and docs#CategoryTheory.FinitaryExtensive are identical...

Oops. Fixed in #8048.

[Dagur Asgeirsson]

I left some minor comments and suggestions on #8012

[Andrew Yang]

I didn't see them though?

[Riccardo Brasca]

@Dagur Asgeirsson you probably didn't hit "submit review" or something like that.

[Dagur Asgeirsson]

Sorry, done!

[Dagur Asgeirsson]

There was an issue with universes in the proof that Stonean is finitary extensive, it didn't find the instance when I tried to use it in the explicit description of condensed sets (#6731). Fixed in #8131

[Riccardo Brasca]

Thanks!

[Dagur Asgeirsson]

FinitaryPreExtensive (note the "pre") and Preregular together imply Precoherent: #8399.
I'll clean it up tomorrow and maybe use it to refactor the proofs that CompHaus and friends are precoherent.

[Riccardo Brasca]

This is great! The analogue without Pre is clear?

[Dagur Asgeirsson]

We don't have Regular and Coherent in mathlib. But Regular + FinitaryExtensive implies Coherent is well known, I think it's proved e.g. in an appendix of Lurie's Ultracategories paper. The main difference is that without the Pre the existence of many more limits is required.