Equivalence of categories

An equivalence of categories C and D is a pair of functors F : C ⥤ D and G : D ⥤ C such that η : 𝟭 C ≅ F ⋙ G and ε : G ⋙ F ≅ 𝟭 D. In many situations, equivalences are a better notion of "sameness" of categories than the stricter isomorphism of categories.

Recall that one way to express that two functors F : C ⥤ D and G : D ⥤ C are adjoint is using two natural transformations η : 𝟭 C ⟶ F ⋙ G and ε : G ⋙ F ⟶ 𝟭 D, called the unit and the counit, such that the compositions F ⟶ FGF ⟶ F and G ⟶ GFG ⟶ G are the identity. Unfortunately, it is not the case that the natural isomorphisms η and ε in the definition of an equivalence automatically give an adjunction. However, it is true that

• if one of the two compositions is the identity, then so is the other, and
• given an equivalence of categories, it is always possible to refine η in such a way that the identities are satisfied.

For this reason, in mathlib we define an equivalence to be a "half-adjoint equivalence", which is a tuple (F, G, η, ε) as in the first paragraph such that the composite F ⟶ FGF ⟶ F is the identity. By the remark above, this already implies that the tuple is an "adjoint equivalence", i.e., that the composite G ⟶ GFG ⟶ G is also the identity.

We also define essentially surjective functors and show that a functor is an equivalence if and only if it is full, faithful and essentially surjective.

Main definitions

• Equivalence: bundled (half-)adjoint equivalences of categories
• Functor.EssSurj: type class on a functor F containing the data of the preimages and the isomorphisms F.obj (preimage d) ≅ d.
• Functor.IsEquivalence: type class on a functor F which is full, faithful and essentially surjective.

Main results

• Equivalence.mk: upgrade an equivalence to a (half-)adjoint equivalence
• isEquivalence_iff_of_iso: when F and G are isomorphic functors, F is an equivalence iff G is.
• Functor.asEquivalenceFunctor: construction of an equivalence of categories from a functor F which satisfies the property F.IsEquivalence (i.e. F is full, faithful and essentially surjective).

Notations

We write C ≌ D (\backcong, not to be confused with ≅/\cong) for a bundled equivalence.

structure CategoryTheory.Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] : Type (max (max (max u₁ u₂) v₁) v₂)

We define an equivalence as a (half)-adjoint equivalence, a pair of functors with a unit and counit which are natural isomorphisms and the triangle law Fη ≫ εF = 1, or in other words the composite F ⟶ FGF ⟶ F is the identity.

In unit_inverse_comp, we show that this is actually an adjoint equivalence, i.e., that the composite G ⟶ GFG ⟶ G is also the identity.

The triangle equation is written as a family of equalities between morphisms, it is more complicated if we write it as an equality of natural transformations, because then we would have to insert natural transformations like F ⟶ F1.

Stacks Tag 001J

• mk' :: (
• functor : Functor C D

  A functor in one direction

• inverse : Functor D C

  A functor in the other direction

• unitIso : Functor.id C ≅ self.functor.comp self.inverse

  The composition functor ⋙ inverse is isomorphic to the identity

• counitIso : self.inverse.comp self.functor ≅ Functor.id D

  The composition inverse ⋙ functor is also isomorphic to the identity

• functor_unitIso_comp (X : C) : CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryStruct.id (self.functor.obj X)

  The natural isomorphisms compose to the identity.

• )

theorem CategoryTheory.Equivalence.ext {C : Type u₁} {D : Type u₂} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : Category.{v₂, u₂} D} {x y : C ≌ D} (functor : x.functor = y.functor) (inverse : x.inverse = y.inverse) (unitIso : HEq x.unitIso y.unitIso) (counitIso : HEq x.counitIso y.counitIso) : x = y

def CategoryTheory.«term_≌_» : Lean.TrailingParserDescr

We infix the usual notation for an equivalence

Equations

• CategoryTheory.«term_≌_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_≌_» 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≌ ") (Lean.ParserDescr.cat `term 10))

@[reducible, inline]

abbrev CategoryTheory.Equivalence.unit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Functor.id C ⟶ e.functor.comp e.inverse

The unit of an equivalence of categories.

Equations

• e.unit = e.unitIso.hom

@[reducible, inline]

abbrev CategoryTheory.Equivalence.counit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.inverse.comp e.functor ⟶ Functor.id D

The counit of an equivalence of categories.

Equations

• e.counit = e.counitIso.hom

@[reducible, inline]

abbrev CategoryTheory.Equivalence.unitInv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.functor.comp e.inverse ⟶ Functor.id C

The inverse of the unit of an equivalence of categories.

Equations

• e.unitInv = e.unitIso.inv

@[reducible, inline]

abbrev CategoryTheory.Equivalence.counitInv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : Functor.id D ⟶ e.inverse.comp e.functor

The inverse of the counit of an equivalence of categories.

Equations

• e.counitInv = e.counitIso.inv

@[simp]

theorem CategoryTheory.Equivalence.Equivalence_mk'_unit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unit = unit_iso.hom

@[simp]

theorem CategoryTheory.Equivalence.Equivalence_mk'_counit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counit = counit_iso.hom

@[simp]

theorem CategoryTheory.Equivalence.Equivalence_mk'_unitInv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unitInv = unit_iso.inv

@[simp]

theorem CategoryTheory.Equivalence.Equivalence_mk'_counitInv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (functor : Functor C D) (inverse : Functor D C) (unit_iso : Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ Functor.id D) (f : ∀ (X : C), CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counitInv = counit_iso.inv

@[simp]

theorem CategoryTheory.Equivalence.functor_unit_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryStruct.id (e.functor.obj X)

@[simp]

theorem CategoryTheory.Equivalence.functor_unit_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryStruct.comp (e.functor.map (e.unit.app X)) (CategoryStruct.comp (e.counit.app (e.functor.obj X)) h) = h

@[simp]

theorem CategoryTheory.Equivalence.counitInv_functor_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryStruct.id (e.functor.obj X)

@[simp]

theorem CategoryTheory.Equivalence.counitInv_functor_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (CategoryStruct.comp (e.functor.map (e.unitInv.app X)) h) = h

theorem CategoryTheory.Equivalence.counitInv_app_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)

theorem CategoryTheory.Equivalence.counit_app_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

@[simp]

theorem CategoryTheory.Equivalence.unit_inverse_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) = CategoryStruct.id (e.inverse.obj Y)

The other triangle equality. The proof follows the following proof in Globular: http://globular.science/1905.001

@[simp]

theorem CategoryTheory.Equivalence.unit_inverse_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (CategoryStruct.comp (e.inverse.map (e.counit.app Y)) h) = h

@[simp]

theorem CategoryTheory.Equivalence.inverse_counitInv_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryStruct.id (e.inverse.obj Y)

@[simp]

theorem CategoryTheory.Equivalence.inverse_counitInv_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (CategoryStruct.comp (e.unitInv.app (e.inverse.obj Y)) h) = h

theorem CategoryTheory.Equivalence.unit_app_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)

theorem CategoryTheory.Equivalence.unitInv_app_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)

@[simp]

theorem CategoryTheory.Equivalence.fun_inv_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) : e.functor.map (e.inverse.map f) = CategoryStruct.comp (e.counit.app X) (CategoryStruct.comp f (e.counitInv.app Y))

theorem CategoryTheory.Equivalence.fun_inv_map_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryStruct.comp (e.functor.map (e.inverse.map f)) h = CategoryStruct.comp (e.counit.app X) (CategoryStruct.comp f (CategoryStruct.comp (e.counitInv.app Y) h))

@[simp]

theorem CategoryTheory.Equivalence.inv_fun_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) : e.inverse.map (e.functor.map f) = CategoryStruct.comp (e.unitInv.app X) (CategoryStruct.comp f (e.unit.app Y))

theorem CategoryTheory.Equivalence.inv_fun_map_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryStruct.comp (e.inverse.map (e.functor.map f)) h = CategoryStruct.comp (e.unitInv.app X) (CategoryStruct.comp f (CategoryStruct.comp (e.unit.app Y) h))

def CategoryTheory.Equivalence.adjointifyη {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (η : Functor.id C ≅ F.comp G) (ε : G.comp F ≅ Functor.id D) : Functor.id C ≅ F.comp G

If η : 𝟭 C ≅ F ⋙ G is part of a (not necessarily half-adjoint) equivalence, we can upgrade it to a refined natural isomorphism adjointifyη η : 𝟭 C ≅ F ⋙ G which exhibits the properties required for a half-adjoint equivalence. See Equivalence.mk.

Equations

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

theorem CategoryTheory.Equivalence.adjointify_η_ε {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (η : Functor.id C ≅ F.comp G) (ε : G.comp F ≅ Functor.id D) (X : C) : CategoryStruct.comp (F.map ((adjointifyη η ε).hom.app X)) (ε.hom.app (F.obj X)) = CategoryStruct.id (F.obj X)

theorem CategoryTheory.Equivalence.adjointify_η_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (η : Functor.id C ≅ F.comp G) (ε : G.comp F ≅ Functor.id D) (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (F.map ((adjointifyη η ε).hom.app X)) (CategoryStruct.comp (ε.hom.app (F.obj X)) h) = h

def CategoryTheory.Equivalence.mk {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (G : Functor D C) (η : Functor.id C ≅ F.comp G) (ε : G.comp F ≅ Functor.id D) : C ≌ D

Every equivalence of categories consisting of functors F and G such that F ⋙ G and G ⋙ F are naturally isomorphic to identity functors can be transformed into a half-adjoint equivalence without changing F or G.

Equations

• CategoryTheory.Equivalence.mk F G η ε = { functor := F, inverse := G, unitIso := CategoryTheory.Equivalence.adjointifyη η ε, counitIso := ε, functor_unitIso_comp := ⋯ }

def CategoryTheory.Equivalence.refl {C : Type u₁} [Category.{v₁, u₁} C] : C ≌ C

Equivalence of categories is reflexive.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.refl_inverse {C : Type u₁} [Category.{v₁, u₁} C] : refl.inverse = Functor.id C

@[simp]

theorem CategoryTheory.Equivalence.refl_unitIso {C : Type u₁} [Category.{v₁, u₁} C] : refl.unitIso = Iso.refl (Functor.id C)

@[simp]

theorem CategoryTheory.Equivalence.refl_counitIso {C : Type u₁} [Category.{v₁, u₁} C] : refl.counitIso = Iso.refl ((Functor.id C).comp (Functor.id C))

@[simp]

theorem CategoryTheory.Equivalence.refl_functor {C : Type u₁} [Category.{v₁, u₁} C] : refl.functor = Functor.id C

instance CategoryTheory.Equivalence.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] : Inhabited (C ≌ C)

Equations

• CategoryTheory.Equivalence.instInhabited = { default := CategoryTheory.Equivalence.refl }

def CategoryTheory.Equivalence.symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : D ≌ C

Equivalence of categories is symmetric.

Equations

• e.symm = { functor := e.inverse, inverse := e.functor, unitIso := e.counitIso.symm, counitIso := e.unitIso.symm, functor_unitIso_comp := ⋯ }

@[simp]

theorem CategoryTheory.Equivalence.symm_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.counitIso = e.unitIso.symm

@[simp]

theorem CategoryTheory.Equivalence.symm_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.unitIso = e.counitIso.symm

@[simp]

theorem CategoryTheory.Equivalence.symm_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.inverse = e.functor

@[simp]

theorem CategoryTheory.Equivalence.symm_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.functor = e.inverse

def CategoryTheory.Equivalence.trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : C ≌ E

Equivalence of categories is transitive.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.trans_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).inverse = f.inverse.comp e.inverse

@[simp]

theorem CategoryTheory.Equivalence.trans_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).counitIso = ((f.inverse.comp e.inverse).associator e.functor f.functor).symm ≪≫ isoWhiskerRight (f.inverse.associator e.inverse e.functor ≪≫ isoWhiskerLeft f.inverse e.counitIso ≪≫ f.inverse.rightUnitor) f.functor ≪≫ f.counitIso

@[simp]

theorem CategoryTheory.Equivalence.trans_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).unitIso = e.unitIso ≪≫ isoWhiskerRight (e.functor.rightUnitor.symm ≪≫ isoWhiskerLeft e.functor f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm) e.inverse ≪≫ (e.functor.comp f.functor).associator f.inverse e.inverse

@[simp]

theorem CategoryTheory.Equivalence.trans_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E) : (e.trans f).functor = e.functor.comp f.functor

def CategoryTheory.Equivalence.funInvIdAssoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor C E) : e.functor.comp (e.inverse.comp F) ≅ F

Composing a functor with both functors of an equivalence yields a naturally isomorphic functor.

Equations

• e.funInvIdAssoc F = (e.functor.associator e.inverse F).symm ≪≫ CategoryTheory.isoWhiskerRight e.unitIso.symm F ≪≫ F.leftUnitor

@[simp]

theorem CategoryTheory.Equivalence.funInvIdAssoc_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor C E) (X : C) : (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)

@[simp]

theorem CategoryTheory.Equivalence.funInvIdAssoc_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor C E) (X : C) : (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)

def CategoryTheory.Equivalence.invFunIdAssoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor D E) : e.inverse.comp (e.functor.comp F) ≅ F

Composing a functor with both functors of an equivalence yields a naturally isomorphic functor.

Equations

• e.invFunIdAssoc F = (e.inverse.associator e.functor F).symm ≪≫ CategoryTheory.isoWhiskerRight e.counitIso F ≪≫ F.leftUnitor

@[simp]

theorem CategoryTheory.Equivalence.invFunIdAssoc_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor D E) (X : D) : (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)

@[simp]

theorem CategoryTheory.Equivalence.invFunIdAssoc_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) (F : Functor D E) (X : D) : (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)

def CategoryTheory.Equivalence.congrLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : Functor C E ≌ Functor D E

If C is equivalent to D, then C ⥤ E is equivalent to D ⥤ E.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrLeft.inverse = (whiskeringLeft C D E).obj e.functor

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrLeft.unitIso = NatIso.ofComponents (fun (F : Functor C E) => (e.funInvIdAssoc F).symm) ⋯

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrLeft.functor = (whiskeringLeft D C E).obj e.inverse

@[simp]

theorem CategoryTheory.Equivalence.congrLeft_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrLeft.counitIso = NatIso.ofComponents (fun (F : Functor D E) => e.invFunIdAssoc F) ⋯

def CategoryTheory.Equivalence.congrRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : Functor E C ≌ Functor E D

If C is equivalent to D, then E ⥤ C is equivalent to E ⥤ D.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.congrRight_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.inverse = (whiskeringRight E D C).obj e.inverse

@[simp]

theorem CategoryTheory.Equivalence.congrRight_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.functor = (whiskeringRight E C D).obj e.functor

@[simp]

theorem CategoryTheory.Equivalence.congrRight_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.unitIso = NatIso.ofComponents (fun (F : Functor E C) => F.rightUnitor.symm ≪≫ isoWhiskerLeft F e.unitIso ≪≫ F.associator e.functor e.inverse) ⋯

@[simp]

theorem CategoryTheory.Equivalence.congrRight_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ D) : e.congrRight.counitIso = NatIso.ofComponents (fun (F : Functor E D) => F.associator e.inverse e.functor ≪≫ isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor) ⋯

@[simp]

theorem CategoryTheory.Equivalence.cancel_unit_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ Y) : CategoryStruct.comp f (e.unit.app Y) = CategoryStruct.comp f' (e.unit.app Y) ↔ f = f'

@[simp]

theorem CategoryTheory.Equivalence.cancel_unitInv_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : CategoryStruct.comp f (e.unitInv.app Y) = CategoryStruct.comp f' (e.unitInv.app Y) ↔ f = f'

@[simp]

theorem CategoryTheory.Equivalence.cancel_counit_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) : CategoryStruct.comp f (e.counit.app Y) = CategoryStruct.comp f' (e.counit.app Y) ↔ f = f'

@[simp]

theorem CategoryTheory.Equivalence.cancel_counitInv_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ Y) : CategoryStruct.comp f (e.counitInv.app Y) = CategoryStruct.comp f' (e.counitInv.app Y) ↔ f = f'

@[simp]

theorem CategoryTheory.Equivalence.cancel_unit_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryStruct.comp f (CategoryStruct.comp g (e.unit.app Y)) = CategoryStruct.comp f' (CategoryStruct.comp g' (e.unit.app Y)) ↔ CategoryStruct.comp f g = CategoryStruct.comp f' g'

@[simp]

theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryStruct.comp f (CategoryStruct.comp g (e.counitInv.app Y)) = CategoryStruct.comp f' (CategoryStruct.comp g' (e.counitInv.app Y)) ↔ CategoryStruct.comp f g = CategoryStruct.comp f' g'

@[simp]

theorem CategoryTheory.Equivalence.cancel_unit_right_assoc' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp g (CategoryStruct.comp h (e.unit.app Z))) = CategoryStruct.comp f' (CategoryStruct.comp g' (CategoryStruct.comp h' (e.unit.app Z))) ↔ CategoryStruct.comp f (CategoryStruct.comp g h) = CategoryStruct.comp f' (CategoryStruct.comp g' h')

@[simp]

theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp g (CategoryStruct.comp h (e.counitInv.app Z))) = CategoryStruct.comp f' (CategoryStruct.comp g' (CategoryStruct.comp h' (e.counitInv.app Z))) ↔ CategoryStruct.comp f (CategoryStruct.comp g h) = CategoryStruct.comp f' (CategoryStruct.comp g' h')

def CategoryTheory.Equivalence.powNat {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) : ℕ → (C ≌ C)

Natural number powers of an auto-equivalence. Use (^) instead.

Equations

• e.powNat 0 = CategoryTheory.Equivalence.refl
• e.powNat 1 = e
• e.powNat n.succ.succ = e.trans (e.powNat (n + 1))

def CategoryTheory.Equivalence.pow {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) : ℤ → (C ≌ C)

Powers of an auto-equivalence. Use (^) instead.

Equations

• e.pow (Int.ofNat n) = e.powNat n
• e.pow (Int.negSucc n) = e.symm.powNat (n + 1)

instance CategoryTheory.Equivalence.instPowInt {C : Type u₁} [Category.{v₁, u₁} C] : Pow (C ≌ C) ℤ

Equations

• CategoryTheory.Equivalence.instPowInt = { pow := CategoryTheory.Equivalence.pow }

@[simp]

theorem CategoryTheory.Equivalence.pow_zero {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) : e ^ 0 = refl

@[simp]

theorem CategoryTheory.Equivalence.pow_one {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) : e ^ 1 = e

@[simp]

theorem CategoryTheory.Equivalence.pow_neg_one {C : Type u₁} [Category.{v₁, u₁} C] (e : C ≌ C) : e ^ (-1) = e.symm

instance CategoryTheory.Equivalence.essSurj_functor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.EssSurj

The functor of an equivalence of categories is essentially surjective.

Stacks Tag 02C3

instance CategoryTheory.Equivalence.essSurj_inverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.EssSurj

def CategoryTheory.Equivalence.fullyFaithfulFunctor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.FullyFaithful

The functor of an equivalence of categories is fully faithful.

Equations

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

def CategoryTheory.Equivalence.fullyFaithfulInverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.FullyFaithful

The inverse of an equivalence of categories is fully faithful.

Equations

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

instance CategoryTheory.Equivalence.faithful_functor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.Faithful

The functor of an equivalence of categories is faithful.

Stacks Tag 02C3

instance CategoryTheory.Equivalence.faithful_inverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.Faithful

instance CategoryTheory.Equivalence.full_functor {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.Full

The functor of an equivalence of categories is full.

Stacks Tag 02C3

instance CategoryTheory.Equivalence.full_inverse {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (e : C ≌ E) : e.inverse.Full

def CategoryTheory.Equivalence.changeFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) : C ≌ D

If e : C ≌ D is an equivalence of categories, and iso : e.functor ≅ G is an isomorphism, then there is an equivalence of categories whose functor is G.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.inv.app X = CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.inv.app X = CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) : (e.changeFunctor iso).functor = G

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.hom.app X = CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.hom.app X = CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))

@[simp]

theorem CategoryTheory.Equivalence.changeFunctor_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor C D} (iso : e.functor ≅ G) : (e.changeFunctor iso).inverse = e.inverse

theorem CategoryTheory.Equivalence.changeFunctor_refl {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) : e.changeFunctor (Iso.refl e.functor) = e

Compatibility of changeFunctor with identity isomorphisms of functors

theorem CategoryTheory.Equivalence.changeFunctor_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G G' : Functor C D} (iso₁ : e.functor ≅ G) (iso₂ : G ≅ G') : (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Compatibility of changeFunctor with the composition of isomorphisms of functors

def CategoryTheory.Equivalence.changeInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) : C ≌ D

If e : C ≌ D is an equivalence of categories, and iso : e.functor ≅ G is an isomorphism, then there is an equivalence of categories whose inverse is G.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_counitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.inv.app X = CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_counitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.hom.app X = CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) : (e.changeInverse iso).functor = e.functor

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_unitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.hom.app X = CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) : (e.changeInverse iso).inverse = G

@[simp]

theorem CategoryTheory.Equivalence.changeInverse_unitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {G : Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.inv.app X = CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)

class CategoryTheory.Functor.IsEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

A functor is an equivalence of categories if it is faithful, full and essentially surjective.

• faithful : F.Faithful
• full : F.Full
• essSurj : F.EssSurj

instance CategoryTheory.Equivalence.isEquivalence_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ≌ D) : F.functor.IsEquivalence

instance CategoryTheory.Equivalence.isEquivalence_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ≌ D) : F.inverse.IsEquivalence

theorem CategoryTheory.Functor.IsEquivalence.mk' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (G : Functor D C) (η : Functor.id C ≅ F.comp G) (ε : G.comp F ≅ Functor.id D) : F.IsEquivalence

To see that a functor is an equivalence, it suffices to provide an inverse functor G such that F ⋙ G and G ⋙ F are naturally isomorphic to identity functors.

noncomputable def CategoryTheory.Functor.inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] : Functor D C

A quasi-inverse D ⥤ C to a functor that F : C ⥤ D that is an equivalence, i.e. faithful, full, and essentially surjective.

Equations

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

noncomputable def CategoryTheory.Functor.asEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] : C ≌ D

Interpret a functor that is an equivalence as an equivalence.

Stacks Tag 02C3

Equations

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

@[simp]

theorem CategoryTheory.Functor.asEquivalence_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] : F.asEquivalence.functor = F

instance CategoryTheory.Functor.isEquivalence_refl {C : Type u₁} [Category.{v₁, u₁} C] : (Functor.id C).IsEquivalence

instance CategoryTheory.Functor.isEquivalence_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] : F.inv.IsEquivalence

instance CategoryTheory.Functor.isEquivalence_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.IsEquivalence] [G.IsEquivalence] : (F.comp G).IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) [F.IsEquivalence] : ((whiskeringLeft C D E).obj F).IsEquivalence

instance CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) [F.IsEquivalence] : ((whiskeringRight E C D).obj F).IsEquivalence

@[simp]

theorem CategoryTheory.Functor.fun_inv_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] (X Y : D) (f : X ⟶ Y) : F.map (F.inv.map f) = CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))

@[simp]

theorem CategoryTheory.Functor.inv_fun_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.IsEquivalence] (X Y : C) (f : X ⟶ Y) : F.inv.map (F.map f) = CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryStruct.comp f (F.asEquivalence.unit.app Y))

theorem CategoryTheory.Functor.isEquivalence_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) [F.IsEquivalence] : G.IsEquivalence

theorem CategoryTheory.Functor.isEquivalence_iff_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) : F.IsEquivalence ↔ G.IsEquivalence

theorem CategoryTheory.Functor.isEquivalence_of_comp_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D E) [G.IsEquivalence] [(F.comp G).IsEquivalence] : F.IsEquivalence

If G and F ⋙ G are equivalence of categories, then F is also an equivalence.

theorem CategoryTheory.Functor.isEquivalence_of_comp_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] (F : Functor C D) (G : Functor D E) [F.IsEquivalence] [(F.comp G).IsEquivalence] : G.IsEquivalence

If F and F ⋙ G are equivalence of categories, then G is also an equivalence.

instance CategoryTheory.Equivalence.essSurjInducedFunctor {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D) : (inducedFunctor ⇑e).EssSurj

instance CategoryTheory.Equivalence.inducedFunctorOfEquiv {D : Type u₂} [Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D) : (inducedFunctor ⇑e).IsEquivalence

instance CategoryTheory.Equivalence.fullyFaithfulToEssImage {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] : F.toEssImage.IsEquivalence

def CategoryTheory.Equivalence.ofFullSubcategory {C : Type u₁} [Category.{v₁, u₁} C] {Z Z' : C → Prop} (h : ∀ (X : C), Z X ↔ Z' X) : FullSubcategory Z ≌ FullSubcategory Z'

A biimplication of properties on the objects of a category C induces an equivalence of the respective induced full subcategories of C.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.ofFullSubcategory_functor {C : Type u₁} [Category.{v₁, u₁} C] {Z Z' : C → Prop} (h : ∀ (X : C), Z X ↔ Z' X) : (ofFullSubcategory h).functor = FullSubcategory.map ⋯

@[simp]

theorem CategoryTheory.Equivalence.ofFullSubcategory_inverse {C : Type u₁} [Category.{v₁, u₁} C] {Z Z' : C → Prop} (h : ∀ (X : C), Z X ↔ Z' X) : (ofFullSubcategory h).inverse = FullSubcategory.map ⋯

@[simp]

theorem CategoryTheory.Equivalence.ofFullSubcategory_counitIso {C : Type u₁} [Category.{v₁, u₁} C] {Z Z' : C → Prop} (h : ∀ (X : C), Z X ↔ Z' X) : (ofFullSubcategory h).counitIso = NatIso.ofComponents (fun (X : FullSubcategory Z') => Iso.refl (((FullSubcategory.map ⋯).comp (FullSubcategory.map ⋯)).obj X)) ⋯

@[simp]

theorem CategoryTheory.Equivalence.ofFullSubcategory_unitIso {C : Type u₁} [Category.{v₁, u₁} C] {Z Z' : C → Prop} (h : ∀ (X : C), Z X ↔ Z' X) : (ofFullSubcategory h).unitIso = NatIso.ofComponents (fun (X : FullSubcategory Z) => Iso.refl ((Functor.id (FullSubcategory Z)).obj X)) ⋯

def CategoryTheory.Iso.compInverseIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) : F.comp H.inverse ≅ G

Construct an isomorphism F ⋙ H.inverse ≅ G from an isomorphism F ≅ G ⋙ H.functor.

Equations

• i.compInverseIso = CategoryTheory.isoWhiskerRight i H.inverse ≪≫ G.associator H.functor H.inverse ≪≫ CategoryTheory.isoWhiskerLeft G H.unitIso.symm ≪≫ G.rightUnitor

@[simp]

theorem CategoryTheory.Iso.compInverseIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.hom.app X = CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))

@[simp]

theorem CategoryTheory.Iso.compInverseIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.inv.app X = CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))

def CategoryTheory.Iso.isoCompInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) : G ≅ F.comp H.inverse

Construct an isomorphism G ≅ F ⋙ H.inverse from an isomorphism G ⋙ H.functor ≅ F.

Equations

• i.isoCompInverse = G.rightUnitor.symm ≪≫ CategoryTheory.isoWhiskerLeft G H.unitIso ≪≫ (G.associator H.functor H.inverse).symm ≪≫ CategoryTheory.isoWhiskerRight i H.inverse

@[simp]

theorem CategoryTheory.Iso.isoCompInverse_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.hom.app X = CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))

@[simp]

theorem CategoryTheory.Iso.isoCompInverse_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {G : Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.inv.app X = CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.obj X))

def CategoryTheory.Iso.inverseCompIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) : G.inverse.comp F ≅ H

Construct an isomorphism G.inverse ⋙ F ≅ H from an isomorphism F ≅ G.functor ⋙ H.

Equations

• i.inverseCompIso = CategoryTheory.isoWhiskerLeft G.inverse i ≪≫ (G.inverse.associator G.functor H).symm ≪≫ CategoryTheory.isoWhiskerRight G.counitIso H ≪≫ H.leftUnitor

@[simp]

theorem CategoryTheory.Iso.inverseCompIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.hom.app X = CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))

@[simp]

theorem CategoryTheory.Iso.inverseCompIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.inv.app X = CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))

def CategoryTheory.Iso.isoInverseComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) : H ≅ G.inverse.comp F

Construct an isomorphism H ≅ G.inverse ⋙ F from an isomorphism G.functor ⋙ H ≅ F.

Equations

• i.isoInverseComp = H.leftUnitor.symm ≪≫ CategoryTheory.isoWhiskerRight G.counitIso.symm H ≪≫ G.inverse.associator G.functor H ≪≫ CategoryTheory.isoWhiskerLeft G.inverse i

@[simp]

theorem CategoryTheory.Iso.isoInverseComp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.inv.app X = CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))

@[simp]

theorem CategoryTheory.Iso.isoInverseComp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C E} {H : Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.hom.app X = CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))