Sifted categories

A category C is sifted if C is nonempty and the diagonal functor C ⥤ C × C is final. Sifted categories can be characterized as those such that the colimit functor (C ⥤ Type) ⥤ Type preserves finite products. We achieve this characterization in this file.

Main results

• isSifted_of_hasBinaryCoproducts_and_nonempty: A nonempty category with binary coproducts is sifted.
• IsSifted.colimPreservesFiniteProductsOfIsSifted: The Type-valued colimit functor for sifted diagrams preserves finite products.
• IsSifted.of_colimit_preservesFiniteProducts: The converse: if the Type-valued colimit functor preserves finite producs, the category is sifted.
• IsSifted.of_final_functor_from_sifted: A category admitting a final functor from a sifted category is itself sifted.

References

• nLab, Sifted category
• Algebraic Theories, Chapter 2.

@[reducible, inline]

abbrev CategoryTheory.IsSiftedOrEmpty (C : Type u) [Category.{v, u} C] : Prop

A category C IsSiftedOrEmpty if the diagonal functor C ⥤ C × C is final.

Equations

• CategoryTheory.IsSiftedOrEmpty C = (CategoryTheory.Functor.diag C).Final

class CategoryTheory.IsSifted (C : Type u) [Category.{v, u} C] extends (CategoryTheory.Functor.diag C).Final : Prop

A category C IsSifted if

1. the diagonal functor C ⥤ C × C is final.
2. there exists some object.

• out (d : C × C) : IsConnected (StructuredArrow d (diag C))
• nonempty : Nonempty C

theorem CategoryTheory.IsSifted.isSifted_of_equiv {C : Type u} [Category.{v, u} C] [IsSifted C] {D : Type u₁} [Category.{v₁, u₁} D] (e : D ≌ C) : IsSifted D

Being sifted is preserved by equivalences of categories

theorem CategoryTheory.IsSifted.isSifted_iff_asSmallIsSifted {C : Type u} [Category.{v, u} C] : IsSifted C ↔ IsSifted (AsSmall C)

In particular a category is sifted iff and only if it is so when viewed as a small category

instance CategoryTheory.IsSifted.instIsConnected {C : Type u} [Category.{v, u} C] [IsSifted C] : IsConnected C

A sifted category is connected.

instance CategoryTheory.IsSifted.instIsSiftedOrEmptyOfHasBinaryCoproducts {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] : IsSiftedOrEmpty C

A category with binary coproducts is sifted or empty.

instance CategoryTheory.IsSifted.isSifted_of_hasBinaryCoproducts_and_nonempty {C : Type u} [Category.{v, u} C] [Nonempty C] [Limits.HasBinaryCoproducts C] : IsSifted C

A nonempty category with binary coproducts is sifted.

instance CategoryTheory.instFinalProdProd' {C : Type u} [Category.{v, u} C] [IsSiftedOrEmpty C] {D : Type u₁} [Category.{v₁, u₁} D] {D' : Type u₂} [Category.{v₂, u₂} D'] (F : Functor C D) (G : Functor C D') [F.Final] [G.Final] : (F.prod' G).Final

theorem CategoryTheory.IsSifted.factorization_prodComparison_colim {C : Type u} [SmallCategory C] (X Y : Functor C (Type u)) : CategoryStruct.comp (Limits.HasColimit.isoOfNatIso ((MonoidalCategory.externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom (CategoryStruct.comp (Limits.colimit.pre (MonoidalCategory.externalProduct X Y) (Functor.diag C)) (Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (MonoidalCategory.curriedTensor (Type u))).hom) = CartesianMonoidalCategory.prodComparison Limits.colim X Y

Through the isomorphisms PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ and externalProductCompDiagIso, the comparison map colimit.pre (X ⊠ Y) (diag C) identifies with the product comparison map for the colimit functor.

instance CategoryTheory.IsSifted.instIsIsoObjFunctorTypeColimTensorObjProdComparison {C : Type u} [SmallCategory C] (X Y : Functor C (Type u)) [IsSifted C] : IsIso (CartesianMonoidalCategory.prodComparison Limits.colim X Y)

If C is sifted, the canonical product comparison map for the colim functor (C ⥤ Type) ⥤ Type is an isomorphism.

instance CategoryTheory.IsSifted.colim_preservesLimits_pair_of_sSifted {C : Type u} [SmallCategory C] [IsSifted C] {X Y : Functor C (Type u)} : Limits.PreservesLimit (Limits.pair X Y) Limits.colim

instance CategoryTheory.IsSifted.colim_preservesBinaryProducts_of_isSifted {C : Type u} [SmallCategory C] [IsSifted C] : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) Limits.colim

Sifted colimits commute with binary products

instance CategoryTheory.IsSifted.colim_preservesTerminal_of_isSifted {C : Type u} [SmallCategory C] [IsSifted C] : Limits.PreservesLimit (Functor.empty (Functor C (Type u))) Limits.colim

If C is sifted, the colimit functor (C ⥤ Type) ⥤ Type preserves terminal objects

instance CategoryTheory.IsSifted.colim_preservesLimitsOfShape_pempty_of_isSifted {C : Type u} [SmallCategory C] [IsSifted C] : Limits.PreservesLimitsOfShape (Discrete PEmpty.{1}) Limits.colim

instance CategoryTheory.IsSifted.colim_preservesFiniteProducts_of_isSifted {C : Type u} [SmallCategory C] [IsSifted C] : Limits.PreservesFiniteProducts Limits.colim

If C is sifted, the colim functor (C ⥤ Type) ⥤ Type preserves finite products.

theorem CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesBinaryProducts (C : Type u) [SmallCategory C] [Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) Limits.colim] : IsSiftedOrEmpty C

If the colim functor (C ⥤ Type) ⥤ Type preserves binary products, then C is sifted or empty.

theorem CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesFiniteProducts (C : Type u) [SmallCategory C] [h : Limits.PreservesFiniteProducts Limits.colim] : IsSiftedOrEmpty C

theorem CategoryTheory.IsSifted.nonempty_of_colim_preservesLimitsOfShapeFinZero (C : Type u) [SmallCategory C] [Limits.PreservesLimitsOfShape (Discrete (Fin 0)) Limits.colim] : Nonempty C

theorem CategoryTheory.IsSifted.of_colim_preservesFiniteProducts (C : Type u) [SmallCategory C] [h : Limits.PreservesFiniteProducts Limits.colim] : IsSifted C

If the colim functor (C ⥤ Type) ⥤ Type preserves finite products, then C is sifted.

theorem CategoryTheory.IsSifted.of_final_functor_from_sifted' {C : Type u} [SmallCategory C] {D : Type u} [SmallCategory D] [IsSifted C] (F : Functor C D) [F.Final] : IsSifted D

Auxiliary version of IsSifted.of_final_functor_from_sifted where everything is a small category.

theorem CategoryTheory.IsSifted.of_final_functor_from_sifted {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] [h₁ : IsSifted C] (F : Functor C D) [F.Final] : IsSifted D

A functor admitting a final functor from a sifted category is sifted.