Thin categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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
To construct a category instance one only needs to specify the
as the axioms hold for free.
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.
C is a thin category, then
D ⥤ C is a thin category.
X ≅ Y in a thin category, it suffices to just give any morphism in each direction.