Thin categories

A thin category (also known as a sparse category) is a category with at most one morphism between each pair of objects. Examples include posets, but also some indexing categories (diagrams) for special shapes of (co)limits. To construct a category instance one only needs to specify the category_struct part, as the axioms hold for free. If C is thin, then the category of functors to C is also thin. Further, to show two objects are isomorphic in a thin category, it suffices only to give a morphism in each direction.

def CategoryTheory.thin_category {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] [Quiver.IsThin C] : CategoryTheory.Category.{v₁, u₁} C

Construct a category instance from a category_struct, using the fact that hom spaces are subsingletons to prove the axioms.

Equations

• CategoryTheory.thin_category = CategoryTheory.Category.mk

instance CategoryTheory.functor_thin {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [Quiver.IsThin C] : Quiver.IsThin (CategoryTheory.Functor D C)

If C is a thin category, then D ⥤ C is a thin category.

Equations

• (_ : Subsingleton (x✝ ⟶ x)) = (_ : Subsingleton (x✝ ⟶ x))

def CategoryTheory.iso_of_both_ways {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {X : C} {Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : X ≅ Y

To show X ≅ Y in a thin category, it suffices to just give any morphism in each direction.

Equations

• CategoryTheory.iso_of_both_ways f g = CategoryTheory.Iso.mk f g

instance CategoryTheory.subsingleton_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {X : C} {Y : C} : Subsingleton (X ≅ Y)

Equations

• (_ : Subsingleton (X ≅ Y)) = (_ : Subsingleton (X ≅ Y))