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.

Main results

• isSifted_of_hasBinaryCoproducts_and_nonempty: A nonempty category with binary coproducts is sifted.

References

• nLab, Sifted category
• [Algebraic Theories, Chapter 2.][Adamek_Rosicky_Vitale_2010]

@[reducible, inline]

abbrev CategoryTheory.IsSiftedOrEmpty (C : Type u) [CategoryTheory.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) [CategoryTheory.Category.{v, u} C] extends CategoryTheory.Functor.Final : Prop

A category C IsSfited if

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

• out : ∀ (d : C × C), CategoryTheory.IsConnected (CategoryTheory.StructuredArrow d (CategoryTheory.Functor.diag C))
• nonempty : Nonempty C

theorem CategoryTheory.IsSifted.nonempty {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsSifted C], Nonempty C

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

Being sifted is preserved by equivalences of categories

theorem CategoryTheory.IsSifted.isSifted_iff_asSmallIsSifted {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.IsSifted C ↔ CategoryTheory.IsSifted (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsSifted C] : CategoryTheory.IsConnected C

A sifted category is connected.

Equations

• ⋯ = ⋯

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

A category with binary coproducts is sifted or empty.

Equations

• ⋯ = ⋯

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

A nonempty category with binary coproducts is sifted.

Equations

• ⋯ = ⋯