Mathlib.CategoryTheory.IsomorphismClasses

Module docstring

{"# 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. "}

CategoryTheory.IsIsomorphic definition

: C → C → Prop

Full source

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

Isomorphism of objects in a category

Informal description

Two objects $X$ and $Y$ in a category $\mathcal{C}$ are called isomorphic, denoted $X \cong Y$, if there exists an isomorphism between them, i.e., a pair of morphisms $f: X \to Y$ and $g: Y \to X$ such that $f \circ g = \text{id}_Y$ and $g \circ f = \text{id}_X$.

CategoryTheory.isIsomorphicSetoid definition

: Setoid C

Full source

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

Setoid of isomorphic objects in a category

Informal description

The setoid structure on the objects of a category $\mathcal{C}$, where two objects $X$ and $Y$ are related if and only if they are isomorphic, i.e., there exists an isomorphism between them. The relation is reflexive (via identity isomorphisms), symmetric (via inverse isomorphisms), and transitive (via composition of isomorphisms).

CategoryTheory.isomorphismClasses definition

: Cat.{v, u} ⥤ Type u

Full source

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

Isomorphism Classes Functor

Informal description

The functor that maps a category $\mathcal{C}$ to the quotient space of its objects under the equivalence relation of isomorphism. Specifically, for a category $\mathcal{C}$, the functor sends each object to its equivalence class in the quotient $\mathrm{Quotient}(\mathrm{isIsomorphicSetoid}\, \mathcal{C})$, and each morphism $F$ between categories to the induced map on the quotient spaces, defined by lifting isomorphisms through $F$.

CategoryTheory.Groupoid.isIsomorphic_iff_nonempty_hom theorem

{C : Type u} [Groupoid.{v} C] {X Y : C} : IsIsomorphic X Y ↔ Nonempty (X ⟶ Y)

Full source

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

Isomorphism in Groupoid Equivalent to Nonempty Hom-Set

Informal description

For any objects $X$ and $Y$ in a groupoid $\mathcal{C}$, the objects $X$ and $Y$ are isomorphic if and only if there exists a morphism from $X$ to $Y$. In other words, $X \cong Y \leftrightarrow \text{Nonempty}(X \to Y)$.