Theorems · Theorem · category theory

CategoryTheory.Limits.Cone.equivalenceOfReindexing_counitIso

∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cone.equivalenceOfReindexing e α).counitIso =
    (((CategoryTheory.Limits.Cone.postcompose α.inv).comp
              ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
                (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom))).associator
          (CategoryTheory.Limits.Cone.whiskering e.functor) (CategoryTheory.Limits.Cone.postcompose α.hom)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight
          ((CategoryTheory.Limits.Cone.postcompose α.inv).associator
            ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
              (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom))
            (CategoryTheory.Limits.Cone.whiskering e.functor))
          (CategoryTheory.Limits.Cone.postcompose α.hom) ≪≫
        CategoryTheory.Functor.isoWhiskerRight
            ((CategoryTheory.Limits.Cone.postcompose α.inv).isoWhiskerLeft
              (CategoryTheory.NatIso.ofComponents
                (fun s => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯))
            (CategoryTheory.Limits.Cone.postcompose α.hom) ≪≫
          CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Limits.Cone.postcompose α.inv).rightUnitor
              (CategoryTheory.Limits.Cone.postcompose α.hom) ≪≫
            CategoryTheory.NatIso.ofComponents
              (fun s => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl s.pt) ⋯) ⋯

Defined in

Mathlib.CategoryTheory.Limits.Cones

Cited by

0 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category