Isomorphisms of categories

An IsoCat C D is an isomorphism of categories: a pair of functors C ⥤ D and D ⥤ C whose composites are equal (not merely naturally isomorphic) to the identity functors. This is a strict notion, stronger than an equivalence of categories C ≌ D. We also define Functor.IsIso as a property saying that a functor is fully faithful and bijective on objects. We develop basic api for these two concepts.

Unless the application explicitly demands an isomorphism, the equivalence of categories is to be preferred.

Main definitions

• CategoryTheory.IsoCat: the type of isomorphisms between categories C and D.
• CategoryTheory.Functor.IsIso: a typeclass expressing that a functor is full, faithful and bijective on objects, hence underlies an isomorphism of categories.

structure CategoryTheory.IsoCat (C : Type u_1) (D : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] : Type (max (max (max u_1 u_2) v_1) v_2)

An isomorphism of categories: a pair of functors whose composites are equal to the identity functors.

• functor : Functor C D

  The forward functor of an isomorphism of categories.

• inverse : Functor D C

  The inverse functor of an isomorphism of categories.

• unit_eq : Functor.id C = self.functor.comp self.inverse

  The composition functor ⋙ inverse is equal to the identity.

• counit_eq : self.inverse.comp self.functor = Functor.id D

  The composition inverse ⋙ functor is equal to the identity.

@[implicit_reducible]

def CategoryTheory.IsoCat.refl (C : Type u_1) [Category.{v_1, u_1} C] : IsoCat C C

The identity isomorphism of categories.

Equations

• CategoryTheory.IsoCat.refl C = { functor := CategoryTheory.Functor.id C, inverse := CategoryTheory.Functor.id C, unit_eq := ⋯, counit_eq := ⋯ }

@[simp]

theorem CategoryTheory.IsoCat.refl_inverse (C : Type u_1) [Category.{v_1, u_1} C] : (refl C).inverse = Functor.id C

@[simp]

theorem CategoryTheory.IsoCat.refl_functor (C : Type u_1) [Category.{v_1, u_1} C] : (refl C).functor = Functor.id C

@[implicit_reducible]

def CategoryTheory.IsoCat.symm {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) : IsoCat D C

The inverse isomorphism of categories, obtained by swapping functor and inverse.

Equations

• e.symm = { functor := e.inverse, inverse := e.functor, unit_eq := ⋯, counit_eq := ⋯ }

@[simp]

theorem CategoryTheory.IsoCat.symm_inverse {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) : e.symm.inverse = e.functor

@[simp]

theorem CategoryTheory.IsoCat.symm_functor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) : e.symm.functor = e.inverse

@[implicit_reducible]

def CategoryTheory.IsoCat.trans {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (e : IsoCat C D) (f : IsoCat D E) : IsoCat C E

Composition of isomorphisms of categories.

Equations

• e.trans f = { functor := e.functor.comp f.functor, inverse := f.inverse.comp e.inverse, unit_eq := ⋯, counit_eq := ⋯ }

@[simp]

theorem CategoryTheory.IsoCat.trans_functor {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (e : IsoCat C D) (f : IsoCat D E) : (e.trans f).functor = e.functor.comp f.functor

@[simp]

theorem CategoryTheory.IsoCat.trans_inverse {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (e : IsoCat C D) (f : IsoCat D E) : (e.trans f).inverse = f.inverse.comp e.inverse

@[implicit_reducible]

def CategoryTheory.IsoCat.objEquiv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) : C ≃ D

The bijection on objects induced by an isomorphism of categories.

Equations

• e.objEquiv = { toFun := e.functor.obj, invFun := e.inverse.obj, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.IsoCat.objEquiv_apply {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) (a✝ : C) : e.objEquiv a✝ = e.functor.obj a✝

@[simp]

theorem CategoryTheory.IsoCat.objEquiv_symm_apply {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) (a✝ : D) : e.objEquiv.symm a✝ = e.inverse.obj a✝

theorem CategoryTheory.IsoCat.functor_comp_injective {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (e : IsoCat C D) {F G : Functor D E} (h : e.functor.comp F = e.functor.comp G) : F = G

theorem CategoryTheory.IsoCat.comp_functor_injective {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (e : IsoCat C D) {F G : Functor E C} (h : F.comp e.functor = G.comp e.functor) : F = G

class CategoryTheory.Functor.IsIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) : Prop

A functor F : C ⥤ D is an isomorphism of categories if it is full, faithful and bijective on objects. Such a functor has a strict inverse Functor.strictInv and assembles into an IsoCat via Functor.asIsomorphism.

• faithful : F.Faithful

  A functor which is an isomorphism of categories is faithful.

• full : F.Full

  A functor which is an isomorphism of categories is full.

• bijective_obj : Function.Bijective F.obj

  A functor which is an isomorphism of categories is bijective on objects.

instance CategoryTheory.Functor.instIsIsoId {C : Type u_1} [Category.{v_1, u_1} C] : (Functor.id C).IsIso

noncomputable def CategoryTheory.Functor.objEquiv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsIso] : C ≃ D

The bijection on objects induced by a functor that is an isomorphism of categories.

Equations

• F.objEquiv = Equiv.ofBijective F.obj ⋯

@[simp]

theorem CategoryTheory.Functor.objEquiv_symm_apply_apply {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsIso] (X : C) : F.objEquiv.symm (F.obj X) = X

@[simp]

theorem CategoryTheory.Functor.objEquiv_apply_symm_apply {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsIso] (Y : D) : F.obj (F.objEquiv.symm Y) = Y

instance CategoryTheory.Functor.instIsEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsIso] : F.IsEquivalence

noncomputable def CategoryTheory.Functor.strictInv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsIso] : Functor D C

The strict inverse of a functor that is an isomorphism of categories, defined using Functor.objEquiv on objects and Functor.preimage on morphisms.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.asIsomorphism {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsIso] : IsoCat C D

A functor that is an isomorphism of categories assembles into an IsoCat, with Functor.strictInv as its inverse.

Equations

• F.asIsomorphism = { functor := F, inverse := F.strictInv, unit_eq := ⋯, counit_eq := ⋯ }

def CategoryTheory.IsoCat.toEquivalence {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) : C ≌ D

The equivalence of categories underlying an IsoCat, with the unit and counit isomorphisms induced by the defining equalities.

Equations

• e.toEquivalence = { functor := e.functor, inverse := e.inverse, unitIso := CategoryTheory.eqToIso ⋯, counitIso := CategoryTheory.eqToIso ⋯, functor_unitIso_comp := ⋯ }

def CategoryTheory.Equivalence.toIsoCat {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : C ≌ D) (h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X) (h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y) (k : ∀ (X : C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (k' : ∀ (Y : D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) : IsoCat C D

Promotes an equivalence of categories e : C ≌ D whose unit and counit isomorphisms are given by equalities of objects into an IsoCat C D.

Equations

• e.toIsoCat h h' k k' = { functor := e.functor, inverse := e.inverse, unit_eq := ⋯, counit_eq := ⋯ }

@[simp]

theorem CategoryTheory.Equivalence.toIsoCat_functor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : C ≌ D) (h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X) (h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y) (k : ∀ (X : C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (k' : ∀ (Y : D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) : (e.toIsoCat h h' k k').functor = e.functor

@[simp]

theorem CategoryTheory.Equivalence.toIsoCat_inverse {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : C ≌ D) (h : ∀ (X : C), e.inverse.obj (e.functor.obj X) = X) (h' : ∀ (Y : D), e.functor.obj (e.inverse.obj Y) = Y) (k : ∀ (X : C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (k' : ∀ (Y : D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) : (e.toIsoCat h h' k k').inverse = e.inverse

instance CategoryTheory.IsoCat.isIso_functor {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) : e.functor.IsIso

instance CategoryTheory.instIsIsoInverse {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (e : IsoCat C D) : e.inverse.IsIso

instance CategoryTheory.instIsIsoStrictInv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.IsIso] : F.strictInv.IsIso

instance CategoryTheory.instIsIsoComp {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) [F.IsIso] [G.IsIso] : (F.comp G).IsIso

@[implicit_reducible]

def CategoryTheory.InducedCategory.isoCat {C : Type u_4} {D : Type u_5} [Category.{v_4, u_4} C] (e : D ≃ C) : IsoCat (InducedCategory C ⇑e) C

The isomorphism of categories between InducedCategory C e and C when e : D ≃ C is a bijection.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InducedCategory.isoCat_inverse_map_hom {C : Type u_4} {D : Type u_5} [Category.{v_4, u_4} C] (e : D ≃ C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((isoCat e).inverse.map f).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp f (eqToHom ⋯))

@[simp]

theorem CategoryTheory.InducedCategory.isoCat_functor {C : Type u_4} {D : Type u_5} [Category.{v_4, u_4} C] (e : D ≃ C) : (isoCat e).functor = inducedFunctor ⇑e

@[simp]

theorem CategoryTheory.InducedCategory.isoCat_inverse_obj {C : Type u_4} {D : Type u_5} [Category.{v_4, u_4} C] (e : D ≃ C) (X : C) : (isoCat e).inverse.obj X = e.symm X

@[reducible, inline]

abbrev CategoryTheory.InducedCategory.equivalence {C : Type u_4} {D : Type u_5} [Category.{v_4, u_4} C] (e : D ≃ C) : InducedCategory C ⇑e ≌ C

The equivalence of categories between InducedCategory C e and C when e : D ≃ C is a bijection.

Equations

• CategoryTheory.InducedCategory.equivalence e = (CategoryTheory.InducedCategory.isoCat e).toEquivalence

theorem CategoryTheory.isIso_inducedFunctor_of_bijective {C : Type u_4} {D : Type u_5} [Category.{v_4, u_4} C] (f : D → C) (hf : Function.Bijective f) : (inducedFunctor f).IsIso