Objects of a category up to an isomorphism #

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

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.

source

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

category_theory.is_isomorphic = λ (X Y : C), nonempty (X ≅ Y)

source

def category_theory.is_isomorphic_setoid (C : Type u) [category_theory.category C] :

setoid C

is_isomorphic defines a setoid.

Equations

category_theory.is_isomorphic_setoid C = {r := category_theory.is_isomorphic _inst_1, iseqv := _}

source

def category_theory.isomorphism_classes :

category_theory.Cat ⥤ Type u

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}

source

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)