mathlib documentation

category_theory.isomorphism_classes

Objects of a category up to an isomorphism

is_isomorphic 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.

def category_theory.is_isomorphic {C : Type u} [category_theory.category C] :
C → C → Prop

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

Equations

is_isomorphic defines a setoid.

Equations

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

Equations