feat(CategoryTheory/Limits): Sifted categories

[robin-carlier]

Introduce the class of sifted categories. A category IsSifted if it is nonempty and the diagonal functor is a final functor.

• Show that sifted categories are stable under equivalences of categories.
• Characterize sifted categories as those for which the Type-valued colimit functor preserves finite products.
• Show that filtered categories are sifted.
• Show that categories admitting a final functor from sifted categories are also sifted.

---

The proof of the main part (showing the characterization in term of the colimit functor) relies on a computation that rewrites the colimit-to-limit comparison for the product as a composite of "Fubini"-type isomorphisms and of colimit.pre for the diagonal functor. I marked the definition and lemmas for this computation as private, because I don’t think they would be useful as standalone lemmas.

I also went with the "Monoidal" notations coming from ChosenFiniteProduct instances for the computation, because it seemed to work better for the back-and-forth between presheaves and types, but this require introducing an isomorphism that compares it to the usual product, that I also marked as private since it is auxiliary to the computation here.

Sadly, I had to prove by hand that tensoring on the left/right preserves colimits (also marked private). This should normally come from the fact that the monoidal structure on types is cartesian closed, but the CartesianClosed instance defined in CategoryTheory/Closed/Types is actually about a different monoidal structure than the one defined in CategoryTheory/Monoidal/Types/Basic (the former is the one coming from monoidalOfHasFiniteProducts, while the latter is the one from monoidalOChosenFiniteProducts). If this gets changed then this should trim a bit of noise from the proof.

[github-actions]

PR summary 5f9bb4611b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Limits.Sifted	616

---

Declarations diff

+ IsSifted
+ IsSifted.IsSiftedOfFinalFunctorFromSifted
+ IsSiftedOfColimitPreservesFiniteProducts
+ IsSiftedOfEquiv
+ IsSiftedOfFinalFunctorFromSifted'
+ IsSiftedOfHasBinaryCoproductsAndNonempty
+ IsSiftedOfIsFiltered
+ IsSiftedOrEmpty
+ IsSiftedOrEmptyOfColimitPreservesBinaryProducts
+ IsSiftedOrEmptyOfColimitPreservesFiniteProducts
+ IsSifted_iff_asSmallIsSifted
+ NonemptyOfColimitPreservesLimitsOfShapeFinZero
+ colimPreservesBinaryProductsOfIsSifted
+ colimPreservesFiniteProductsOfIsSifted
+ colimPreservesLimitsOfPairsOfIsSifted
+ colimPreservesLimitsOfShapePEmtyOfIsSifted
+ colimPreservesTerminalObjectOfIsSifted
+ instance : IsIso (prodComparison colim X Y) := by
+ instance [HasBinaryCoproducts C] : IsSiftedOrEmpty C := by
+ instance [IsSifted C]: IsConnected C

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[joelriou]

Could you add a ## References section to the docstring of the file?

[robin-carlier]

Could you add a ## References section to the docstring of the file?

I added the n-lab as well as Adámek-Rosický-Vitale’s Algebraic theories. Note that both references take preservations of finite products for the colimit functor as the definition.