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 (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
- category_theory.thin_category = {to_category_struct := _inst_1, id_comp' := _, comp_id' := _, assoc' := _}
If C is a thin category, then D ⥤ C is a thin category.
To show X ≅ Y in a thin category, it suffices to just give any morphism in each direction.
Equations
- category_theory.iso_of_both_ways f g = {hom := f, inv := g, hom_inv_id' := _, inv_hom_id' := _}