mathlib3 documentation

category_theory.limits.small_complete

Any small complete category is a preorder #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We show that any small category which has all (small) limits is a preorder: In particular, we show that if a small category C in universe u has products of size u, then for any X Y : C there is at most one morphism X ⟶ Y. Note that in Lean, a preorder category is strictly one where the morphisms are in Prop, so we instead show that the homsets are subsingleton.

References #

Tags #

small complete, preorder, Freyd

source
@[protected, instance]
def category_theory.quiver.is_thin {C : Type u} [category_theory.small_category C] [category_theory.limits.has_products C] :
quiver.is_thin C

A small category with products is a thin category.

in Lean, a preorder category is one where the morphisms are in Prop, which is weaker than the usual notion of a preorder/thin category which says that each homset is subsingleton; we show the latter rather than providing a preorder C instance.