# 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
• IsEquivalence: type class on a functor F containing the data of the inverse G as well as the natural isomorphisms η and ε.
• EssSurj: type class on a functor F containing the data of the preimages and the isomorphisms F.obj (preimage d) ≅ d.

## Main results #

• Equivalence.mk: upgrade an equivalence to a (half-)adjoint equivalence
• IsEquivalence.equivOfIso: when F and G are isomorphic functors, F is an equivalence iff G is.
• Equivalence.ofFullyFaithfullyEssSurj: a fully faithful essentially surjective functor is an equivalence.

## 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₂) [] [] :
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.

See

• mk' :: (
• functor :

A functor in one direction

• inverse :

A functor in the other direction

• unitIso : CategoryTheory.Functor.comp self.functor self.inverse

The composition functor ⋙ inverse is isomorphic to the identity

• counitIso : CategoryTheory.Functor.comp self.inverse self.functor

The composition inverse ⋙ functor is also isomorphic to the identity

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

The natural isomorphisms compose to the identity.

• )
Instances For

We infix the usual notation for an equivalence

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]
abbrev CategoryTheory.Equivalence.unit {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
CategoryTheory.Functor.comp e.functor e.inverse

The unit of an equivalence of categories.

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

The counit of an equivalence of categories.

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

The inverse of the unit of an equivalence of categories.

Equations
• e.unitInv = e.unitIso.inv
Instances For
@[inline, reducible]
abbrev CategoryTheory.Equivalence.counitInv {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
CategoryTheory.Functor.comp e.inverse 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 : CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
(CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).unit = unit_iso.hom
@[simp]
theorem CategoryTheory.Equivalence.Equivalence_mk'_counit {C : Type u₁} [] {D : Type u₂} [] (functor : ) (inverse : ) (unit_iso : CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
(CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).counit = counit_iso.hom
@[simp]
theorem CategoryTheory.Equivalence.Equivalence_mk'_unitInv {C : Type u₁} [] {D : Type u₂} [] (functor : ) (inverse : ) (unit_iso : CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
(CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).unitInv = unit_iso.inv
@[simp]
theorem CategoryTheory.Equivalence.Equivalence_mk'_counitInv {C : Type u₁} [] {D : Type u₂} [] (functor : ) (inverse : ) (unit_iso : CategoryTheory.Functor.comp functor inverse) (counit_iso : CategoryTheory.Functor.comp inverse functor ) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.toPrefunctor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (functor.toPrefunctor.obj X)) :
(CategoryTheory.Equivalence.mk' functor inverse unit_iso counit_iso).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.toPrefunctor.obj X Z) :
CategoryTheory.CategoryStruct.comp (e.functor.toPrefunctor.map (e.unit.app X)) (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.toPrefunctor.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.toPrefunctor.map (e.unit.app X)) (e.counit.app (e.functor.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.toPrefunctor.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.toPrefunctor.obj X Z) :
CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp (e.functor.toPrefunctor.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.toPrefunctor.obj X)) (e.functor.toPrefunctor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.toPrefunctor.obj X)
theorem CategoryTheory.Equivalence.counitInv_app_functor {C : Type u₁} [] {D : Type u₂} [] (e : C D) (X : C) :
e.counitInv.app (e.functor.toPrefunctor.obj X) = e.functor.toPrefunctor.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.toPrefunctor.obj X) = e.functor.toPrefunctor.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.toPrefunctor.obj Y Z) :
CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.toPrefunctor.obj Y)) (CategoryTheory.CategoryStruct.comp (e.inverse.toPrefunctor.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.toPrefunctor.obj Y)) (e.inverse.toPrefunctor.map (e.counit.app Y)) = CategoryTheory.CategoryStruct.id (e.inverse.toPrefunctor.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.toPrefunctor.obj Y Z) :
CategoryTheory.CategoryStruct.comp (e.inverse.toPrefunctor.map (e.counitInv.app Y)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.toPrefunctor.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.toPrefunctor.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.toPrefunctor.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.toPrefunctor.obj Y)
theorem CategoryTheory.Equivalence.unit_app_inverse {C : Type u₁} [] {D : Type u₂} [] (e : C D) (Y : D) :
e.unit.app (e.inverse.toPrefunctor.obj Y) = e.inverse.toPrefunctor.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.toPrefunctor.obj Y) = e.inverse.toPrefunctor.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.toPrefunctor.obj (e.inverse.toPrefunctor.obj Y) Z) :
CategoryTheory.CategoryStruct.comp (e.functor.toPrefunctor.map (e.inverse.toPrefunctor.map f)) h = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h))
@[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.toPrefunctor.map (e.inverse.toPrefunctor.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.toPrefunctor.obj (e.functor.toPrefunctor.obj Y) Z) :
CategoryTheory.CategoryStruct.comp (e.inverse.toPrefunctor.map (e.functor.toPrefunctor.map f)) h = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h))
@[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.toPrefunctor.map (e.functor.toPrefunctor.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 : } :

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 : } (X : C) {Z : D} (h : F.toPrefunctor.obj X Z) :
CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (.hom.app X)) (CategoryTheory.CategoryStruct.comp (ε.hom.app (F.toPrefunctor.obj X)) h) = h
theorem CategoryTheory.Equivalence.adjointify_η_ε {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (X : C) :
CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (.hom.app X)) (ε.hom.app (F.toPrefunctor.obj X)) = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)
def CategoryTheory.Equivalence.mk {C : Type u₁} [] {D : Type u₂} [] (F : ) (G : ) :
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
Instances For
@[simp]
theorem CategoryTheory.Equivalence.refl_counitIso {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.counitIso =
@[simp]
theorem CategoryTheory.Equivalence.refl_inverse {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.inverse =
@[simp]
theorem CategoryTheory.Equivalence.refl_unitIso {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.unitIso =
@[simp]
theorem CategoryTheory.Equivalence.refl_functor {C : Type u₁} [] :
CategoryTheory.Equivalence.refl.functor =

Equivalence of categories is reflexive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.Equivalence.instInhabitedEquivalence = { default := CategoryTheory.Equivalence.refl }
@[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_unitIso {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.symm.unitIso = e.counitIso.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_functor {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
e.symm.functor = e.inverse
def CategoryTheory.Equivalence.symm {C : Type u₁} [] {D : Type u₂} [] (e : C D) :
D C

Equivalence of categories is symmetric.

Equations
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 = CategoryTheory.Functor.comp e.functor f.functor
@[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
@[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 = CategoryTheory.Functor.comp f.inverse e.inverse
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 : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.funInvIdAssoc_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) (X : C) :
.hom.app X = F.toPrefunctor.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) :
.inv.app X = F.toPrefunctor.map (e.unit.app X)
def CategoryTheory.Equivalence.invFunIdAssoc {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.invFunIdAssoc_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) (F : ) (X : D) :
.hom.app X = F.toPrefunctor.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) :
.inv.app X = F.toPrefunctor.map (e.counitInv.app X)
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_counitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
.counitIso = CategoryTheory.NatIso.ofComponents fun (F : ) =>
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_inverse {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
.inverse = ().toPrefunctor.obj e.functor
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_unitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
@[simp]
theorem CategoryTheory.Equivalence.congrLeft_functor {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
.functor = ().toPrefunctor.obj e.inverse
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) :
.inverse = ().toPrefunctor.obj e.inverse
@[simp]
theorem CategoryTheory.Equivalence.congrRight_functor {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
.functor = ().toPrefunctor.obj e.functor
@[simp]
theorem CategoryTheory.Equivalence.congrRight_counitIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (e : C D) :
.counitIso = CategoryTheory.NatIso.ofComponents fun (F : ) => CategoryTheory.Functor.associator F e.inverse e.functor ≪≫
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.toPrefunctor.obj (e.functor.toPrefunctor.obj Y)) (f' : X e.inverse.toPrefunctor.obj (e.functor.toPrefunctor.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.toPrefunctor.obj (e.inverse.toPrefunctor.obj Y)) (f' : X e.functor.toPrefunctor.obj (e.inverse.toPrefunctor.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
• = CategoryTheory.Equivalence.refl
• = e.trans ()
Instances For
def CategoryTheory.Equivalence.pow {C : Type u₁} [] (e : C C) :
(C C)

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

Equations
Instances For
Equations
• CategoryTheory.Equivalence.instPowEquivalenceInt = { 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
class CategoryTheory.IsEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max (max u₁ u₂) v₁) v₂)

A functor that is part of a (half) adjoint equivalence

• mk' :: (
• inverse :

The inverse functor to F

• Composition F ⋙ inverse is isomorphic to the identity.

• Composition inverse ⋙ F is isomorphic to the identity.

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

The natural isomorphisms are inverse.

• )
Instances
@[simp]
theorem CategoryTheory.IsEquivalence.functor_unitIso_comp_assoc {C : Type u₁} [] {D : Type u₂} [] {F : } [self : ] (X : C) {Z : D} (h : F.toPrefunctor.obj X Z) :
CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map (CategoryTheory.IsEquivalence.unitIso.hom.app X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.counitIso.hom.app (F.toPrefunctor.obj X)) h) = h
instance CategoryTheory.IsEquivalence.ofEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : C D) :
Equations
instance CategoryTheory.IsEquivalence.ofEquivalenceInverse {C : Type u₁} [] {D : Type u₂} [] (F : C D) :
Equations
def CategoryTheory.IsEquivalence.mk {C : Type u₁} [] {D : Type u₂} [] {F : } (G : ) :

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.

Equations
Instances For
def CategoryTheory.Functor.asEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) :
C D

Interpret a functor that is an equivalence as an equivalence.

Equations
Instances For
Equations
def CategoryTheory.Functor.inv {C : Type u₁} [] {D : Type u₂} [] (F : ) :

The inverse functor of a functor that is an equivalence.

Equations
Instances For
instance CategoryTheory.Functor.isEquivalenceInv {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
@[simp]
theorem CategoryTheory.Functor.asEquivalence_functor {C : Type u₁} [] {D : Type u₂} [] (F : ) :
.functor = F
@[simp]
theorem CategoryTheory.Functor.asEquivalence_inverse {C : Type u₁} [] {D : Type u₂} [] (F : ) :
@[simp]
theorem CategoryTheory.Functor.asEquivalence_unit {C : Type u₁} [] {D : Type u₂} [] {F : } :
.unitIso = CategoryTheory.IsEquivalence.unitIso
@[simp]
theorem CategoryTheory.Functor.asEquivalence_counit {C : Type u₁} [] {D : Type u₂} [] {F : } :
.counitIso = CategoryTheory.IsEquivalence.counitIso
@[simp]
theorem CategoryTheory.Functor.inv_inv {C : Type u₁} [] {D : Type u₂} [] (F : ) :
instance CategoryTheory.Functor.isEquivalenceTrans {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.Equivalence.functor_inv {C : Type u₁} [] {D : Type u₂} [] (E : C D) :
CategoryTheory.Functor.inv E.functor = E.inverse
@[simp]
theorem CategoryTheory.Equivalence.inverse_inv {C : Type u₁} [] {D : Type u₂} [] (E : C D) :
CategoryTheory.Functor.inv E.inverse = E.functor
@[simp]
theorem CategoryTheory.Equivalence.isEquivalence_unitIso {C : Type u₁} [] {D : Type u₂} [] (E : C D) :
CategoryTheory.IsEquivalence.unitIso = E.unitIso
@[simp]
theorem CategoryTheory.Equivalence.isEquivalence_counitIso {C : Type u₁} [] {D : Type u₂} [] (E : C D) :
CategoryTheory.IsEquivalence.counitIso = E.counitIso
@[simp]
theorem CategoryTheory.Equivalence.functor_asEquivalence {C : Type u₁} [] {D : Type u₂} [] (E : C D) :
@[simp]
theorem CategoryTheory.Equivalence.inverse_asEquivalence {C : Type u₁} [] {D : Type u₂} [] (E : C D) :
@[simp]
theorem CategoryTheory.IsEquivalence.fun_inv_map {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : D) (Y : D) (f : X Y) :
F.toPrefunctor.map (.toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp (.counit.app X) (CategoryTheory.CategoryStruct.comp f (.counitInv.app Y))
@[simp]
theorem CategoryTheory.IsEquivalence.inv_fun_map {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) (Y : C) (f : X Y) :
.toPrefunctor.map (F.toPrefunctor.map f) = CategoryTheory.CategoryStruct.comp (.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (.unit.app Y))
@[simp]
theorem CategoryTheory.IsEquivalence.ofIso_unitIso_inv_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) (X : C) :
CategoryTheory.IsEquivalence.unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (.toPrefunctor.map (e.inv.app X)) (CategoryTheory.IsEquivalence.unitIso.inv.app X)
@[simp]
theorem CategoryTheory.IsEquivalence.ofIso_unitIso_hom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) (X : C) :
CategoryTheory.IsEquivalence.unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.unitIso.hom.app X) (.toPrefunctor.map (e.hom.app X))
@[simp]
theorem CategoryTheory.IsEquivalence.ofIso_counitIso_inv_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) (X : D) :
CategoryTheory.IsEquivalence.counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.counitIso.inv.app X) (e.hom.app (.toPrefunctor.obj X))
@[simp]
theorem CategoryTheory.IsEquivalence.ofIso_inverse {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) :
@[simp]
theorem CategoryTheory.IsEquivalence.ofIso_counitIso_hom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) (X : D) :
CategoryTheory.IsEquivalence.counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.inv.app (.toPrefunctor.obj X)) (CategoryTheory.IsEquivalence.counitIso.hom.app X)
def CategoryTheory.IsEquivalence.ofIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) :

When a functor F is an equivalence of categories, and G is isomorphic to F, then G is also an equivalence of categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.IsEquivalence.ofIso_trans {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (e : F G) (e' : G H) (hF : ) :

Compatibility of ofIso with the composition of isomorphisms of functors

theorem CategoryTheory.IsEquivalence.ofIso_refl {C : Type u₁} [] {D : Type u₂} [] (F : ) (hF : ) :

Compatibility of ofIso with identity isomorphisms of functors

@[simp]
theorem CategoryTheory.IsEquivalence.equivOfIso_symm_apply {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) :
hF =
@[simp]
theorem CategoryTheory.IsEquivalence.equivOfIso_apply {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) (hF : ) :
def CategoryTheory.IsEquivalence.equivOfIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (e : F G) :

When F and G are two isomorphic functors, then F is an equivalence iff G is.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.IsEquivalence.cancelCompRight {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] (F : ) (G : ) (hG : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.IsEquivalence.cancelCompLeft {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] (F : ) (G : ) (hF : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Equivalence.essSurj_of_equivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) :

An equivalence is essentially surjective.

See .

instance CategoryTheory.Equivalence.faithfulOfEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) :

An equivalence is faithful.

See .

Equations
• (_ : ) = (_ : )
instance CategoryTheory.Equivalence.fullOfEquivalence {C : Type u₁} [] {D : Type u₂} [] (F : ) :

An equivalence is full.

See .

Equations
• One or more equations did not get rendered due to their size.
noncomputable def CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj {C : Type u₁} [] {D : Type u₂} [] (F : ) :

A functor which is full, faithful, and essentially surjective is an equivalence.

See .

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Equivalence.functor_map_inj_iff {C : Type u₁} [] {D : Type u₂} [] (e : C D) {X : C} {Y : C} (f : X Y) (g : X Y) :
e.functor.toPrefunctor.map f = e.functor.toPrefunctor.map g f = g
@[simp]
theorem CategoryTheory.Equivalence.inverse_map_inj_iff {C : Type u₁} [] {D : Type u₂} [] (e : C D) {X : D} {Y : D} (f : X Y) (g : X Y) :
e.inverse.toPrefunctor.map f = e.inverse.toPrefunctor.map g f = g
instance CategoryTheory.Equivalence.essSurjInducedFunctor {D : Type u₂} [] {C' : Type u_1} (e : C' D) :
Equations
noncomputable instance CategoryTheory.Equivalence.inducedFunctorOfEquiv {D : Type u₂} [] {C' : Type u_1} (e : C' D) :
Equations
noncomputable instance CategoryTheory.Equivalence.fullyFaithfulToEssImage {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
@[simp]
theorem CategoryTheory.Iso.compInvIso_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) (X : C) :
.hom.app X = CategoryTheory.CategoryStruct.comp (.toPrefunctor.map (i.hom.app X)) (CategoryTheory.IsEquivalence.unitIso.inv.app (G.toPrefunctor.obj X))
@[simp]
theorem CategoryTheory.Iso.compInvIso_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) (X : C) :
.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.unitIso.hom.app (G.toPrefunctor.obj X)) (.toPrefunctor.map (i.inv.app X))
def CategoryTheory.Iso.compInvIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) :

Construct an isomorphism F ⋙ H.inv ≅ G from an isomorphism F ≅ G ⋙ H.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Iso.compInverseIso_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : F CategoryTheory.Functor.comp G H.functor) (X : C) :
.app X = CategoryTheory.CategoryStruct.comp (H.inverse.toPrefunctor.map (i.hom.app X)) (H.unitIso.inv.app (G.toPrefunctor.obj X))
@[simp]
theorem CategoryTheory.Iso.compInverseIso_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : F CategoryTheory.Functor.comp G H.functor) (X : C) :
.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.toPrefunctor.obj X)) (H.inverse.toPrefunctor.map (i.inv.app X))
def CategoryTheory.Iso.compInverseIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : F CategoryTheory.Functor.comp G H.functor) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Iso.isoCompInv_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) (X : C) :
.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.unitIso.hom.app (G.toPrefunctor.obj X)) (.toPrefunctor.map (i.hom.app X))
@[simp]
theorem CategoryTheory.Iso.isoCompInv_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) (X : C) :
.inv.app X = CategoryTheory.CategoryStruct.comp (.toPrefunctor.map (i.inv.app X)) (CategoryTheory.IsEquivalence.unitIso.inv.app (G.toPrefunctor.obj X))
def CategoryTheory.Iso.isoCompInv {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) :

Construct an isomorphism G ≅ F ⋙ H.inv from an isomorphism G ⋙ H ≅ F.

Equations
• = ().symm
Instances For
@[simp]
theorem CategoryTheory.Iso.isoCompInverse_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : CategoryTheory.Functor.comp G H.functor F) (X : C) :
.app X = CategoryTheory.CategoryStruct.comp (H.inverse.toPrefunctor.map (i.inv.app X)) (H.unitIso.inv.app (G.toPrefunctor.obj X))
@[simp]
theorem CategoryTheory.Iso.isoCompInverse_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : CategoryTheory.Functor.comp G H.functor F) (X : C) :
.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.toPrefunctor.obj X)) (H.inverse.toPrefunctor.map (i.hom.app X))
def CategoryTheory.Iso.isoCompInverse {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : D E} (i : CategoryTheory.Functor.comp G H.functor F) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Iso.invCompIso_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) (X : D) :
.hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (.toPrefunctor.obj X)) (H.toPrefunctor.map (CategoryTheory.IsEquivalence.counitIso.hom.app X))
@[simp]
theorem CategoryTheory.Iso.invCompIso_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) (X : D) :
.inv.app X = CategoryTheory.CategoryStruct.comp (H.toPrefunctor.map (CategoryTheory.IsEquivalence.counitIso.inv.app X)) (i.inv.app (.toPrefunctor.obj X))
def CategoryTheory.Iso.invCompIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) :

Construct an isomorphism G.inv ⋙ F ≅ H from an isomorphism F ≅ G ⋙ H.

Equations
• One or more equations did not get rendered due to their size.
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 CategoryTheory.Functor.comp G.functor H) (X : D) :
.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.toPrefunctor.obj X)) (H.toPrefunctor.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 CategoryTheory.Functor.comp G.functor H) (X : D) :
.app X = CategoryTheory.CategoryStruct.comp (H.toPrefunctor.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.toPrefunctor.obj X))
def CategoryTheory.Iso.inverseCompIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : F CategoryTheory.Functor.comp G.functor H) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Iso.isoInvComp_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) (X : D) :
.hom.app X = CategoryTheory.CategoryStruct.comp (H.toPrefunctor.map (CategoryTheory.IsEquivalence.counitIso.inv.app X)) (i.hom.app (.toPrefunctor.obj X))
@[simp]
theorem CategoryTheory.Iso.isoInvComp_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) (X : D) :
.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (.toPrefunctor.obj X)) (H.toPrefunctor.map (CategoryTheory.IsEquivalence.counitIso.hom.app X))
def CategoryTheory.Iso.isoInvComp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) :

Construct an isomorphism H ≅ G.inv ⋙ F from an isomorphism G ⋙ H ≅ F.

Equations
• = ().symm
Instances For
@[simp]
theorem CategoryTheory.Iso.isoInverseComp_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : CategoryTheory.Functor.comp G.functor H F) (X : D) :
.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.toPrefunctor.obj X)) (H.toPrefunctor.map (G.counitIso.hom.app X))
@[simp]
theorem CategoryTheory.Iso.isoInverseComp_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : CategoryTheory.Functor.comp G.functor H F) (X : D) :
.app X = CategoryTheory.CategoryStruct.comp (H.toPrefunctor.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.toPrefunctor.obj X))
def CategoryTheory.Iso.isoInverseComp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {H : } {G : C D} (i : CategoryTheory.Functor.comp G.functor H F) :

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

Equations
Instances For
@[deprecated CategoryTheory.Iso.compInvIso]
def CategoryTheory.compInvIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) :

Alias of CategoryTheory.Iso.compInvIso.

Construct an isomorphism F ⋙ H.inv ≅ G from an isomorphism F ≅ G ⋙ H.

Equations
Instances For
@[deprecated CategoryTheory.Iso.isoCompInv]
def CategoryTheory.isoCompInv {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) :

Alias of CategoryTheory.Iso.isoCompInv.

Construct an isomorphism G ≅ F ⋙ H.inv from an isomorphism G ⋙ H ≅ F.

Equations
Instances For
@[deprecated CategoryTheory.Iso.invCompIso]
def CategoryTheory.invCompIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) :

Alias of CategoryTheory.Iso.invCompIso.

Construct an isomorphism G.inv ⋙ F ≅ H from an isomorphism F ≅ G ⋙ H.

Equations
Instances For
@[deprecated CategoryTheory.Iso.isoInvComp]
def CategoryTheory.isoInvComp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (i : ) :

Alias of CategoryTheory.Iso.isoInvComp.

Construct an isomorphism H ≅ G.inv ⋙ F from an isomorphism G ⋙ H ≅ F.

Equations
Instances For