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.

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

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

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

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

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

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

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

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

        Instances For