Documentation

Mathlib.CategoryTheory.IsomorphismClasses

Objects of a category up to an isomorphism #

IsIsomorphic X Y := Nonempty (X ≅ Y) is an equivalence relation on the objects of a category. The quotient with respect to this relation defines a functor from our category to Type.

An object X is isomorphic to an object Y, if X ≅ Y is not empty.

Equations
Instances For

    IsIsomorphic defines a setoid.

    Equations
    Instances For

      The functor that sends each category to the quotient space of its objects up to an isomorphism.

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