mathlib documentation

category_theory.thin

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.

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

Equations
@[instance]
def category_theory.functor_thin {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [∀ (X Y : C), subsingleton (X Y)] (F₁ F₂ : D C) :
subsingleton (F₁ F₂)

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

def category_theory.iso_of_both_ways {C : Type u₁} [category_theory.category C] [∀ (X Y : C), subsingleton (X Y)] {X Y : C} :
(X Y)(Y X)(X Y)

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

Equations
@[instance]
def category_theory.subsingleton_iso {C : Type u₁} [category_theory.category C] [∀ (X Y : C), subsingleton (X Y)] {X Y : C} :