# 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.

theorem CategoryTheory.Equivalence.ext {C : Type u₁} {D : Type u₂} :
∀ {inst : } {inst_1 : } {x y : C D}, x.functor = y.functorx.inverse = y.inverseHEq x.unitIso y.unitIsoHEq x.counitIso y.counitIsox = y
theorem CategoryTheory.Equivalence.ext_iff {C : Type u₁} {D : Type u₂} :
∀ {inst : } {inst_1 : } {x y : C D}, x = y x.functor = y.functor x.inverse = y.inverse HEq x.unitIso y.unitIso HEq x.counitIso y.counitIso
structure CategoryTheory.Equivalence (C : Type u₁) (D : Type u₂) [] [] :
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.

• mk' :: (
• functor :

A functor in one direction

• inverse :

A functor in the other direction

• unitIso : self.functor.comp self.inverse

The composition functor ⋙ inverse is isomorphic to the identity

• counitIso : self.inverse.comp self.functor

The composition inverse ⋙ functor is also isomorphic to the identity

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

The natural isomorphisms compose to the identity.

• )
Instances For
theorem CategoryTheory.Equivalence.functor_unitIso_comp {C : Type u₁} {D : Type u₂} [] [] (self : C D) (X : C) :
CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryTheory.CategoryStruct.id (self.functor.obj X)

The natural isomorphisms compose to the identity.

We infix the usual notation for an equivalence

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Equivalence.unit {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.functor.comp e.inverse

The unit of an equivalence of categories.

Equations
• e.unit = e.unitIso.hom
Instances For
@[reducible, inline]
abbrev CategoryTheory.Equivalence.counit {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.inverse.comp e.functor

The counit of an equivalence of categories.

Equations
• e.counit = e.counitIso.hom
Instances For
@[reducible, inline]
abbrev CategoryTheory.Equivalence.unitInv {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.functor.comp e.inverse

The inverse of the unit of an equivalence of categories.

Equations
• e.unitInv = e.unitIso.inv
Instances For
@[reducible, inline]
abbrev CategoryTheory.Equivalence.counitInv {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.inverse.comp e.functor

The inverse of the counit of an equivalence of categories.

Equations
• e.counitInv = e.counitIso.inv
Instances For
@[simp]
theorem CategoryTheory.Equivalence.Equivalence_mk'_unit {C : Type u₁} [] {D : Type u₂} [] (functor : ) (inverse : ) (unit_iso : functor.comp inverse) (counit_iso : inverse.comp functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.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₁} [] {D : Type u₂} [] (functor : ) (inverse : ) (unit_iso : functor.comp inverse) (counit_iso : inverse.comp functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.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₁} [] {D : Type u₂} [] (functor : ) (inverse : ) (unit_iso : functor.comp inverse) (counit_iso : inverse.comp functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.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₁} [] {D : Type u₂} [] (functor : ) (inverse : ) (unit_iso : functor.comp inverse) (counit_iso : inverse.comp functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.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_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) {Z : D} (h : e.functor.obj X Z) :
CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.obj X)) h) = h
@[simp]
theorem CategoryTheory.Equivalence.functor_unit_comp {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) :
CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
@[simp]
theorem CategoryTheory.Equivalence.counitInv_functor_comp_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) {Z : D} (h : e.functor.obj X Z) :
CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (CategoryTheory.CategoryStruct.comp (e.functor.map (e.unitInv.app X)) h) = h
@[simp]
theorem CategoryTheory.Equivalence.counitInv_functor_comp {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) :
CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
theorem CategoryTheory.Equivalence.counitInv_app_functor {C : Type u₁} [] {D : Type u₂} [] (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₁} [] {D : Type u₂} [] (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_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) (Y : D) {Z : C} (h : e.inverse.obj Y Z) :
CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counit.app Y)) h) = h
@[simp]
theorem CategoryTheory.Equivalence.unit_inverse_comp {C : Type u₁} [] {D : Type u₂} [] (e : C D) (Y : D) :
CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) = CategoryTheory.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.inverse_counitInv_comp_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) (Y : D) {Z : C} (h : e.inverse.obj Y Z) :
CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.obj Y)) h) = h
@[simp]
theorem CategoryTheory.Equivalence.inverse_counitInv_comp {C : Type u₁} [] {D : Type u₂} [] (e : C D) (Y : D) :
CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
theorem CategoryTheory.Equivalence.unit_app_inverse {C : Type u₁} [] {D : Type u₂} [] (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₁} [] {D : Type u₂} [] (e : C D) (Y : D) :
e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)
theorem CategoryTheory.Equivalence.fun_inv_map_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : D) (Y : D) (f : X Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) Z) :
@[simp]
theorem CategoryTheory.Equivalence.fun_inv_map {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : D) (Y : D) (f : X Y) :
e.functor.map (e.inverse.map f) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y))
theorem CategoryTheory.Equivalence.inv_fun_map_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) (Y : C) (f : X Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) Z) :
@[simp]
theorem CategoryTheory.Equivalence.inv_fun_map {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) (Y : C) (f : X Y) :
e.inverse.map (e.functor.map f) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y))
def CategoryTheory.Equivalence.adjointifyη {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (η : F.comp G) (ε : G.comp F ) :
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.
Instances For
theorem CategoryTheory.Equivalence.adjointify_η_ε_assoc {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (η : F.comp G) (ε : G.comp F ) (X : C) {Z : D} (h : F.obj X Z) :
CategoryTheory.CategoryStruct.comp (F.map (.hom.app X)) (CategoryTheory.CategoryStruct.comp (ε.hom.app (F.obj X)) h) = h
theorem CategoryTheory.Equivalence.adjointify_η_ε {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (η : F.comp G) (ε : G.comp F ) (X : C) :
CategoryTheory.CategoryStruct.comp (F.map (.hom.app X)) (ε.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Equivalence.mk {C : Type u₁} [] {D : Type u₂} [] (F : ) (G : ) (η : F.comp G) (ε : G.comp F ) :
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
• = { functor := F, inverse := G, unitIso := , counitIso := ε, functor_unitIso_comp := }
Instances For
@[simp]
theorem CategoryTheory.Equivalence.refl_functor {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.functor =
@[simp]
theorem CategoryTheory.Equivalence.refl_unitIso {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.unitIso =
@[simp]
theorem CategoryTheory.Equivalence.refl_inverse {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.inverse =
@[simp]
theorem CategoryTheory.Equivalence.refl_counitIso {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.counitIso =

Equivalence of categories is reflexive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.Equivalence.instInhabited = { default := CategoryTheory.Equivalence.refl }
@[simp]
theorem CategoryTheory.Equivalence.symm_functor {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.symm.functor = e.inverse
@[simp]
theorem CategoryTheory.Equivalence.symm_counitIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.symm.counitIso = e.unitIso.symm
@[simp]
theorem CategoryTheory.Equivalence.symm_inverse {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.symm.inverse = e.functor
@[simp]
theorem CategoryTheory.Equivalence.symm_unitIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.symm.unitIso = e.counitIso.symm
def CategoryTheory.Equivalence.symm {C : Type u₁} [] {D : Type u₂} [] (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 := }
Instances For
@[simp]
theorem CategoryTheory.Equivalence.trans_functor {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (f : D E) :
(e.trans f).functor = e.functor.comp f.functor
@[simp]
theorem CategoryTheory.Equivalence.trans_inverse {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (f : D E) :
(e.trans f).inverse = f.inverse.comp e.inverse
@[simp]
theorem CategoryTheory.Equivalence.trans_unitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (f : D E) :
(e.trans f).unitIso = e.unitIso ≪≫ CategoryTheory.isoWhiskerLeft e.functor (CategoryTheory.isoWhiskerRight f.unitIso e.inverse)
@[simp]
theorem CategoryTheory.Equivalence.trans_counitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (f : D E) :
(e.trans f).counitIso = CategoryTheory.isoWhiskerLeft f.inverse (CategoryTheory.isoWhiskerRight e.counitIso f.functor) ≪≫ f.counitIso
def CategoryTheory.Equivalence.trans {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (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.
Instances For
def CategoryTheory.Equivalence.funInvIdAssoc {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) :
e.functor.comp (e.inverse.comp F) F

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Equivalence.funInvIdAssoc_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) (X : C) :
(e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
@[simp]
theorem CategoryTheory.Equivalence.funInvIdAssoc_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) (X : C) :
(e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)
def CategoryTheory.Equivalence.invFunIdAssoc {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) :
e.inverse.comp (e.functor.comp F) F

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Equivalence.invFunIdAssoc_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) (X : D) :
(e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
@[simp]
theorem CategoryTheory.Equivalence.invFunIdAssoc_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) (X : D) :
(e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app X)
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_inverse {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrLeft.inverse = .obj e.functor
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_unitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrLeft.unitIso = CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun (F : ) => (e.funInvIdAssoc F).symm) ) (CategoryTheory.NatIso.ofComponents (fun (F : ) => e.invFunIdAssoc F) )
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_functor {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrLeft.functor = .obj e.inverse
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_counitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrLeft.counitIso = CategoryTheory.NatIso.ofComponents (fun (F : ) => e.invFunIdAssoc F)
def CategoryTheory.Equivalence.congrLeft {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :

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.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.congrRight_inverse {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrRight.inverse = .obj e.inverse
@[simp]
theorem CategoryTheory.Equivalence.congrRight_functor {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrRight.functor = .obj e.functor
@[simp]
theorem CategoryTheory.Equivalence.congrRight_counitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrRight.counitIso = CategoryTheory.NatIso.ofComponents (fun (F : ) => F.associator e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor)
@[simp]
theorem CategoryTheory.Equivalence.congrRight_unitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
e.congrRight.unitIso = CategoryTheory.Equivalence.adjointifyη (CategoryTheory.NatIso.ofComponents (fun (F : ) => F.rightUnitor.symm ≪≫ CategoryTheory.isoWhiskerLeft F e.unitIso ≪≫ F.associator e.functor e.inverse) ) (CategoryTheory.NatIso.ofComponents (fun (F : ) => F.associator e.inverse e.functor ≪≫ CategoryTheory.isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor) )
def CategoryTheory.Equivalence.congrRight {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C 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.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.cancel_unit_right {C : Type u₁} [] {D : Type u₂} [] (e : C D) {X : C} {Y : C} (f : X Y) (f' : X Y) :
@[simp]
theorem CategoryTheory.Equivalence.cancel_unitInv_right {C : Type u₁} [] {D : Type u₂} [] (e : C D) {X : C} {Y : C} (f : X e.inverse.obj (e.functor.obj Y)) (f' : X e.inverse.obj (e.functor.obj Y)) :
CategoryTheory.CategoryStruct.comp f (e.unitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unitInv.app Y) f = f'
@[simp]
theorem CategoryTheory.Equivalence.cancel_counit_right {C : Type u₁} [] {D : Type u₂} [] (e : C D) {X : D} {Y : D} (f : X e.functor.obj (e.inverse.obj Y)) (f' : X e.functor.obj (e.inverse.obj Y)) :
@[simp]
theorem CategoryTheory.Equivalence.cancel_counitInv_right {C : Type u₁} [] {D : Type u₂} [] (e : C D) {X : D} {Y : D} (f : X Y) (f' : X Y) :
CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counitInv.app Y) f = f'
@[simp]
theorem CategoryTheory.Equivalence.cancel_unit_right_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) {W : C} {X : C} {X' : C} {Y : C} (f : W X) (g : X Y) (f' : W X') (g' : X' Y) :
@[simp]
theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc {C : Type u₁} [] {D : Type u₂} [] (e : C D) {W : D} {X : D} {X' : D} {Y : D} (f : W X) (g : X Y) (f' : W X') (g' : X' Y) :
@[simp]
theorem CategoryTheory.Equivalence.cancel_unit_right_assoc' {C : Type u₁} [] {D : Type u₂} [] (e : C D) {W : C} {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} (f : W X) (g : X Y) (h : Y Z) (f' : W X') (g' : X' Y') (h' : Y' Z) :
@[simp]
theorem CategoryTheory.Equivalence.cancel_counitInv_right_assoc' {C : Type u₁} [] {D : Type u₂} [] (e : C D) {W : D} {X : D} {X' : D} {Y : D} {Y' : D} {Z : D} (f : W X) (g : X Y) (h : Y Z) (f' : W X') (g' : X' Y') (h' : Y' Z) :
def CategoryTheory.Equivalence.powNat {C : Type u₁} [] (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))
Instances For
def CategoryTheory.Equivalence.pow {C : Type u₁} [] (e : C C) :
(C C)

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

Equations
Instances For
instance CategoryTheory.Equivalence.instPowInt {C : Type u₁} [] :
Pow (C C)
Equations
• CategoryTheory.Equivalence.instPowInt = { pow := CategoryTheory.Equivalence.pow }
@[simp]
theorem CategoryTheory.Equivalence.pow_zero {C : Type u₁} [] (e : C C) :
e ^ 0 = CategoryTheory.Equivalence.refl
@[simp]
theorem CategoryTheory.Equivalence.pow_one {C : Type u₁} [] (e : C C) :
e ^ 1 = e
@[simp]
theorem CategoryTheory.Equivalence.pow_neg_one {C : Type u₁} [] (e : C C) :
e ^ (-1) = e.symm
instance CategoryTheory.Equivalence.essSurj_functor {C : Type u₁} [] {E : Type u₃} [] (e : C E) :
e.functor.EssSurj

The functor of an equivalence of categories is essentially surjective.

Equations
• =
instance CategoryTheory.Equivalence.essSurj_inverse {C : Type u₁} [] {E : Type u₃} [] (e : C E) :
e.inverse.EssSurj
Equations
• =
def CategoryTheory.Equivalence.fullyFaithfulFunctor {C : Type u₁} [] {E : Type u₃} [] (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.
Instances For
def CategoryTheory.Equivalence.fullyFaithfulInverse {C : Type u₁} [] {E : Type u₃} [] (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.
Instances For
instance CategoryTheory.Equivalence.faithful_functor {C : Type u₁} [] {E : Type u₃} [] (e : C E) :
e.functor.Faithful

The functor of an equivalence of categories is faithful.

Equations
• =
instance CategoryTheory.Equivalence.faithful_inverse {C : Type u₁} [] {E : Type u₃} [] (e : C E) :
e.inverse.Faithful
Equations
• =
instance CategoryTheory.Equivalence.full_functor {C : Type u₁} [] {E : Type u₃} [] (e : C E) :
e.functor.Full

The functor of an equivalence of categories is full.

Equations
• =
instance CategoryTheory.Equivalence.full_inverse {C : Type u₁} [] {E : Type u₃} [] (e : C E) :
e.inverse.Full
Equations
• =
@[simp]
theorem CategoryTheory.Equivalence.changeFunctor_inverse {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.functor G) :
(e.changeFunctor iso).inverse = e.inverse
@[simp]
theorem CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.functor G) (X : D) :
(e.changeFunctor iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))
@[simp]
theorem CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.functor G) (X : C) :
(e.changeFunctor iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)
@[simp]
theorem CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.functor G) (X : C) :
(e.changeFunctor iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))
@[simp]
theorem CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.functor G) (X : D) :
(e.changeFunctor iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)
@[simp]
theorem CategoryTheory.Equivalence.changeFunctor_functor {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.functor G) :
(e.changeFunctor iso).functor = G
def CategoryTheory.Equivalence.changeFunctor {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (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.
Instances For
theorem CategoryTheory.Equivalence.changeFunctor_refl {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.changeFunctor (CategoryTheory.Iso.refl e.functor) = e

Compatibility of changeFunctor with identity isomorphisms of functors

theorem CategoryTheory.Equivalence.changeFunctor_trans {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } {G' : } (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

@[simp]
theorem CategoryTheory.Equivalence.changeInverse_counitIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.inverse G) (X : D) :
(e.changeInverse iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))
@[simp]
theorem CategoryTheory.Equivalence.changeInverse_unitIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.inverse G) (X : C) :
(e.changeInverse iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))
@[simp]
theorem CategoryTheory.Equivalence.changeInverse_unitIso_inv_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.inverse G) (X : C) :
(e.changeInverse iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)
@[simp]
theorem CategoryTheory.Equivalence.changeInverse_inverse {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.inverse G) :
(e.changeInverse iso).inverse = G
@[simp]
theorem CategoryTheory.Equivalence.changeInverse_functor {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.inverse G) :
(e.changeInverse iso).functor = e.functor
@[simp]
theorem CategoryTheory.Equivalence.changeInverse_counitIso_hom_app {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.inverse G) (X : D) :
(e.changeInverse iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)
def CategoryTheory.Equivalence.changeInverse {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (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.
Instances For
class CategoryTheory.Functor.IsEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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

• faithful : F.Faithful
• full : F.Full
• essSurj : F.EssSurj
Instances
theorem CategoryTheory.Functor.IsEquivalence.faithful {C : Type u₁} [] {D : Type u₂} [] {F : } [self : F.IsEquivalence] :
F.Faithful
theorem CategoryTheory.Functor.IsEquivalence.full {C : Type u₁} [] {D : Type u₂} [] {F : } [self : F.IsEquivalence] :
F.Full
theorem CategoryTheory.Functor.IsEquivalence.essSurj {C : Type u₁} [] {D : Type u₂} [] {F : } [self : F.IsEquivalence] :
F.EssSurj
instance CategoryTheory.Equivalence.isEquivalence_functor {C : Type u₁} [] {D : Type u₂} [] (F : C D) :
F.functor.IsEquivalence
Equations
• =
instance CategoryTheory.Equivalence.isEquivalence_inverse {C : Type u₁} [] {D : Type u₂} [] (F : C D) :
F.inverse.IsEquivalence
Equations
• =
theorem CategoryTheory.Functor.IsEquivalence.mk' {C : Type u₁} [] {D : Type u₂} [] {F : } (G : ) (η : F.comp G) (ε : G.comp F ) :
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₁} [] {D : Type u₂} [] (F : ) [F.IsEquivalence] :

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.
Instances For
@[simp]
theorem CategoryTheory.Functor.asEquivalence_functor {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.IsEquivalence] :
F.asEquivalence.functor = F
noncomputable def CategoryTheory.Functor.asEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.IsEquivalence] :
C D

Interpret a functor that is an equivalence as an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Functor.isEquivalence_refl {C : Type u₁} [] :
.IsEquivalence
Equations
• =
instance CategoryTheory.Functor.isEquivalence_inv {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.IsEquivalence] :
F.inv.IsEquivalence
Equations
• =
instance CategoryTheory.Functor.isEquivalence_trans {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) [F.IsEquivalence] [G.IsEquivalence] :
(F.comp G).IsEquivalence
Equations
• =
instance CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) [F.IsEquivalence] :
(.obj F).IsEquivalence
Equations
• =
instance CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) [F.IsEquivalence] :
(.obj F).IsEquivalence
Equations
• =
@[simp]
theorem CategoryTheory.Functor.fun_inv_map {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.IsEquivalence] (X : D) (Y : D) (f : X Y) :
F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))
@[simp]
theorem CategoryTheory.Functor.inv_fun_map {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.IsEquivalence] (X : C) (Y : C) (f : X Y) :
F.inv.map (F.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y))
theorem CategoryTheory.Functor.isEquivalence_of_iso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) [F.IsEquivalence] :
G.IsEquivalence
theorem CategoryTheory.Functor.isEquivalence_iff_of_iso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) :
F.IsEquivalence G.IsEquivalence
theorem CategoryTheory.Functor.isEquivalence_of_comp_right {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] (F : ) (G : ) [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₁} [] {D : Type u₂} [] {E : Type u_1} [] (F : ) (G : ) [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₂} [] {C' : Type u_1} (e : C' D) :
.EssSurj
Equations
• =
noncomputable instance CategoryTheory.Equivalence.inducedFunctorOfEquiv {D : Type u₂} [] {C' : Type u_1} (e : C' D) :
.IsEquivalence
Equations
• =
noncomputable instance CategoryTheory.Equivalence.fullyFaithfulToEssImage {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.Full] [F.Faithful] :
F.toEssImage.IsEquivalence
Equations
• =
@[simp]
theorem CategoryTheory.Iso.compInverseIso_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : F G.comp H.functor) (X : C) :
i.compInverseIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))
@[simp]
theorem CategoryTheory.Iso.compInverseIso_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : F G.comp H.functor) (X : C) :
i.compInverseIso.hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))
def CategoryTheory.Iso.compInverseIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {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
Instances For
@[simp]
theorem CategoryTheory.Iso.isoCompInverse_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : G.comp H.functor F) (X : C) :
i.isoCompInverse.inv.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.obj X))
@[simp]
theorem CategoryTheory.Iso.isoCompInverse_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : G.comp H.functor F) (X : C) :
i.isoCompInverse.hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))
def CategoryTheory.Iso.isoCompInverse {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {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
Instances For
@[simp]
theorem CategoryTheory.Iso.inverseCompIso_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : F G.functor.comp H) (X : D) :
i.inverseCompIso.hom.app X = CategoryTheory.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₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : F G.functor.comp H) (X : D) :
i.inverseCompIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))
def CategoryTheory.Iso.inverseCompIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {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
Instances For
@[simp]
theorem CategoryTheory.Iso.isoInverseComp_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : G.functor.comp H F) (X : D) :
i.isoInverseComp.hom.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))
@[simp]
theorem CategoryTheory.Iso.isoInverseComp_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : G.functor.comp H F) (X : D) :
i.isoInverseComp.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
def CategoryTheory.Iso.isoInverseComp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {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
Instances For
@[deprecated CategoryTheory.Functor.IsEquivalence]
def CategoryTheory.IsEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) :

Alias of CategoryTheory.Functor.IsEquivalence.

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

Equations
Instances For
@[deprecated CategoryTheory.Functor.fun_inv_map]
theorem CategoryTheory.IsEquivalence.fun_inv_map {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.IsEquivalence] (X : D) (Y : D) (f : X Y) :
F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))

Alias of CategoryTheory.Functor.fun_inv_map.

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

Alias of CategoryTheory.Functor.inv_fun_map.

@[deprecated CategoryTheory.Equivalence.changeFunctor]
def CategoryTheory.IsEquivalence.ofIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } (iso : e.functor G) :
C D

Alias of CategoryTheory.Equivalence.changeFunctor.

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
Instances For
@[deprecated CategoryTheory.Equivalence.changeFunctor_trans]
theorem CategoryTheory.IsEquivalence.ofIso_trans {C : Type u₁} [] {D : Type u₂} [] (e : C D) {G : } {G' : } (iso₁ : e.functor G) (iso₂ : G G') :
(e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Alias of CategoryTheory.Equivalence.changeFunctor_trans.

Compatibility of changeFunctor with the composition of isomorphisms of functors

@[deprecated CategoryTheory.Equivalence.changeFunctor_refl]
theorem CategoryTheory.IsEquivalence.ofIso_refl {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.changeFunctor (CategoryTheory.Iso.refl e.functor) = e

Alias of CategoryTheory.Equivalence.changeFunctor_refl.

Compatibility of changeFunctor with identity isomorphisms of functors

@[deprecated CategoryTheory.Functor.isEquivalence_iff_of_iso]
theorem CategoryTheory.IsEquivalence.equivOfIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) :
F.IsEquivalence G.IsEquivalence

Alias of CategoryTheory.Functor.isEquivalence_iff_of_iso.

@[deprecated CategoryTheory.Functor.isEquivalence_of_comp_right]
theorem CategoryTheory.IsEquivalence.cancelCompRight {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] (F : ) (G : ) [G.IsEquivalence] [(F.comp G).IsEquivalence] :
F.IsEquivalence

Alias of CategoryTheory.Functor.isEquivalence_of_comp_right.

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

@[deprecated CategoryTheory.Functor.isEquivalence_of_comp_left]
theorem CategoryTheory.IsEquivalence.cancelCompLeft {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] (F : ) (G : ) [F.IsEquivalence] [(F.comp G).IsEquivalence] :
G.IsEquivalence

Alias of CategoryTheory.Functor.isEquivalence_of_comp_left.

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