Mathlib.CategoryTheory.Thin

Module docstring

{"# 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. "}

CategoryTheory.thin_category definition

: Category C

Full source

/-- Construct a category instance from a category_struct, using the fact that
    hom spaces are subsingletons to prove the axioms. -/
def thin_category : Category C where

Thin Category Construction

Informal description

Given a category structure on a type `C` where the hom-sets (morphism spaces) are subsingletons (i.e., there is at most one morphism between any two objects), this constructs a valid category instance on `C`. The category axioms hold automatically due to the thinness condition.

CategoryTheory.functor_thin instance

: Quiver.IsThin (D ⥤ C)

Full source

/-- If `C` is a thin category, then `D ⥤ C` is a thin category. -/
instance functor_thin : Quiver.IsThin (D ⥤ C) := fun _ _ =>
  ⟨fun α β => NatTrans.ext (by subsingleton)⟩

Functors into a Thin Category Form a Thin Category

Informal description

For any thin category $C$ and any category $D$, the category of functors from $D$ to $C$ is also thin. That is, there is at most one natural transformation between any two functors $F, G : D \to C$.

CategoryTheory.iso_of_both_ways definition

{X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) : X ≅ Y

Full source

/-- To show `X ≅ Y` in a thin category, it suffices to just give any morphism in each direction. -/
def iso_of_both_ways {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X) :
    X ≅ Y where
  hom := f
  inv := g

Isomorphism construction in thin categories

Informal description

In a thin category $\mathcal{C}$, to construct an isomorphism between objects $X$ and $Y$, it suffices to provide any morphism $f : X \to Y$ and any morphism $g : Y \to X$. The composition conditions $f \circ g = \text{id}_Y$ and $g \circ f = \text{id}_X$ hold automatically due to the thinness of the category.

CategoryTheory.subsingleton_iso instance

{X Y : C} : Subsingleton (X ≅ Y)

Full source

instance subsingleton_iso {X Y : C} : Subsingleton (X ≅ Y) :=
  ⟨by
    intro i₁ i₂
    ext1
    subsingleton⟩

Uniqueness of Isomorphisms in Thin Categories

Informal description

For any two objects $X$ and $Y$ in a thin category $\mathcal{C}$, the set of isomorphisms between $X$ and $Y$ is a subsingleton (i.e., it has at most one element).