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.
@[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) :
Construct an isomorphism F ⋙ H.inv ≅ G from an isomorphism F ≅ G ⋙ H.
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) :
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) :
Construct an isomorphism G.inv ⋙ F ≅ H from an isomorphism F ≅ G ⋙ H.
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) :
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) :