Documentation

Mathlib.CategoryTheory.FinCategory.Basic

Finite categories #

A category is finite in this sense if it has finitely many objects, and finitely many morphisms.

Implementation #

Prior to #14046, FinCategory required a DecidableEq instance on the object and morphism types. This does not seem to have had any practical payoff (i.e. making some definition constructive) so we have removed these requirements to avoid having to supply instances or delay with non-defeq conflicts between instances.

Equations
  • CategoryTheory.discreteFintype = Fintype.ofEquiv α CategoryTheory.discreteEquiv.symm

A category with a Fintype of objects, and a Fintype for each morphism space.

Instances
    Equations

    The opposite of a finite category is finite.

    Equations
    • One or more equations did not get rendered due to their size.

    Applying ULift to morphisms and objects of a category preserves finiteness.

    Equations
    • One or more equations did not get rendered due to their size.