mathlib documentation

category_theory.functor.inv_isos

Natural isomorphisms with composition with inverses #

Definition of useful natural isomorphisms involving inverses of functors. These definitions cannot go in category_theory/equivalence because they require eq_to_hom.

@[simp]
theorem category_theory.comp_inv_iso_hom_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence H] (i : F G H) (X : A) :
@[simp]
theorem category_theory.comp_inv_iso_inv_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence H] (i : F G H) (X : A) :
def category_theory.comp_inv_iso {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence H] (i : F G H) :
F H.inv G

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

Equations
def category_theory.iso_comp_inv {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence H] (i : G H F) :
G F H.inv

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

Equations
@[simp]
theorem category_theory.iso_comp_inv_hom_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence H] (i : G H F) (X : A) :
@[simp]
theorem category_theory.iso_comp_inv_inv_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence H] (i : G H F) (X : A) :
@[simp]
theorem category_theory.inv_comp_iso_inv_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence G] (i : F G H) (X : B) :
@[simp]
theorem category_theory.inv_comp_iso_hom_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence G] (i : F G H) (X : B) :
def category_theory.inv_comp_iso {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence G] (i : F G H) :
G.inv F H

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

Equations
def category_theory.iso_inv_comp {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence G] (i : G H F) :
H G.inv F

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

Equations
@[simp]
theorem category_theory.iso_inv_comp_inv_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence G] (i : G H F) (X : B) :
@[simp]
theorem category_theory.iso_inv_comp_hom_app {A : Type u₁} [category_theory.category A] {B : Type u₂} [category_theory.category B] {C : Type u₃} [category_theory.category C] {F : A C} {G : A B} {H : B C} [h : category_theory.is_equivalence G] (i : G H F) (X : B) :