# Documentation

Mathlib.CategoryTheory.Functor.InvIsos

# Natural isomorphisms with composition with inverses #

Definition of useful natural isomorphisms involving inverses of functors. These definitions cannot go in CategoryTheory/Equivalence because they require EqToHom.

@[simp]
theorem CategoryTheory.compInvIso_inv_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) (X : A) :
().inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsEquivalence.unitIso.hom.app (G.obj X)) (().map (i.inv.app X))
@[simp]
theorem CategoryTheory.compInvIso_hom_app {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) (X : A) :
().hom.app X = CategoryTheory.CategoryStruct.comp (().map (i.hom.app X)) (CategoryTheory.IsEquivalence.unitIso.inv.app (G.obj X))
def CategoryTheory.compInvIso {A : Type u₁} [] {B : Type u₂} [] {C : Type u₃} [] {F : } {G : } {H : } [h : ] (i : ) :

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

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

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

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

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

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

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

Instances For