IsomorphismClasses.lean

/-
Copyright (c) 2019 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
module

public import Mathlib.CategoryTheory.Category.Cat
public import Mathlib.CategoryTheory.Groupoid
public import Mathlib.CategoryTheory.Types.Basic

/-!
# 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`.
-/

@[expose] public section


universe v u

namespace CategoryTheory

section Category

variable {C : Type u} [Category.{v} C]

/-- An object `X` is isomorphic to an object `Y` if `X ≅ Y` is nonempty. -/
def IsIsomorphic : C → C → Prop := fun X Y => Nonempty (X ≅ Y)

variable (C)

/-- `IsIsomorphic` defines a setoid. -/
@[instance_reducible]
def isIsomorphicSetoid : Setoid C where
  r := IsIsomorphic
  iseqv := ⟨fun X => ⟨Iso.refl X⟩, fun ⟨α⟩ => ⟨α.symm⟩, fun ⟨α⟩ ⟨β⟩ => ⟨α.trans β⟩⟩

end Category

/-- The functor that sends each category to the quotient space of its objects up to an isomorphism.
-/
def isomorphismClasses : Cat.{v, u} ⥤ Type u where
  obj C := Quotient (isIsomorphicSetoid C.α)
  map {_ _} F := Quot.map F.toFunctor.obj fun _ _ ⟨f⟩ => ⟨F.toFunctor.mapIso f⟩
  map_id {C} := by  -- Porting note: this used to be `tidy`
    apply funext; intro x
    apply @Quot.recOn _ _ _ x
    · intro _ _ p
      simp only [types_id_apply]
    · intro _
      rfl
  map_comp {C D E} f g := by -- Porting note(s): idem
    apply funext; intro x
    apply @Quot.recOn _ _ _ x
    · intro _ _ _
      simp only
    · intro _
      rfl

theorem Groupoid.isIsomorphic_iff_nonempty_hom {C : Type u} [Groupoid.{v} C] {X Y : C} :
    IsIsomorphic X Y ↔ Nonempty (X ⟶ Y) :=
  (Groupoid.isoEquivHom X Y).nonempty_congr

end CategoryTheory