Documentation

Mathlib.CategoryTheory.Limits.Sifted

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 #

References #

source
@[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
    Instances For
      source
      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.
      Instances
        source
        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

        source
        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

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

        A sifted category is connected.

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

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

        source
        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