mathlib3 documentation

category_theory.functor.inv_isos

Natural isomorphisms with composition with inverses #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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