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.
An object X is isomorphic to an object Y, if X ≅ Y is not empty.
Equations
- category_theory.is_isomorphic = λ (X Y : C), nonempty (X ≅ Y)
is_isomorphic defines a setoid.
Equations
- category_theory.is_isomorphic_setoid C = {r := category_theory.is_isomorphic _inst_1, iseqv := _}
The functor that sends each category to the quotient space of its objects up to an isomorphism.
Equations
- category_theory.isomorphism_classes = {obj := λ (C : category_theory.Cat), quotient (category_theory.is_isomorphic_setoid C.α), map := λ (C D : category_theory.Cat) (F : C ⟶ D), quot.map F.obj _, map_id' := category_theory.isomorphism_classes._proof_2, map_comp' := category_theory.isomorphism_classes._proof_3}
theorem
category_theory.groupoid.is_isomorphic_iff_nonempty_hom
{C : Type u}
[category_theory.groupoid C]
{X Y : C} :
category_theory.is_isomorphic X Y ↔ nonempty (X ⟶ Y)