Thin categories: induced categories

A category is thin (Quiver.IsThin) when there is at most one morphism between any two objects. Mathlib records that functor categories into a thin category are thin, that the opposite of a thin category is thin, and that every functor out of a thin category is faithful. This file records one further closure property: a category induced along a map into a thin category is thin.

The motivating instance is the category of members of a family B of opens of a topological space, InducedCategory (Opens X) (Subtype.val : B → Opens X), which indexes the limits describing a presheaf adapted to B. Thinness makes the functor laws of functors between such index categories instances of Subsingleton.elim, and it makes their faithfulness automatic. It does not by itself make such a functor full: a preimage must still be constructed, although thinness then discharges the equation the preimage has to satisfy.

Main results

• TauCeti.CategoryTheory.instIsThinInducedCategory: a category induced along a map into a thin category is thin.

instance TauCeti.CategoryTheory.instIsThinInducedCategory {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [Quiver.IsThin D] (F : C → D) : Quiver.IsThin (CategoryTheory.InducedCategory D F)

A category induced along a map into a thin category is thin.