Short complexes in functor categories

In this file, it is shown that if J and C are two categories (such that C has zero morphisms), then there is an equivalence of categories ShortComplex.functorEquivalence J C : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

def CategoryTheory.ShortComplex.FunctorEquivalence.functor (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : Functor (ShortComplex (Functor J C)) (Functor J (ShortComplex C))

The obvious functor ShortComplex (J ⥤ C) ⥤ J ⥤ ShortComplex C.

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_obj (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (S : ShortComplex (Functor J C)) (j : J) : ((functor J C).obj S).obj j = S.map ((evaluation J C).obj j)

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_map (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (S : ShortComplex (Functor J C)) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : ((functor J C).obj S).map f = S.mapNatTrans ((evaluation J C).map f)

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.functor_map_app (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : ShortComplex (Functor J C)} (φ : X✝ ⟶ Y✝) (j : J) : ((functor J C).map φ).app j = ((evaluation J C).obj j).mapShortComplex.map φ

def CategoryTheory.ShortComplex.FunctorEquivalence.inverse (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : Functor (Functor J (ShortComplex C)) (ShortComplex (Functor J C))

The obvious functor (J ⥤ ShortComplex C) ⥤ ShortComplex (J ⥤ C).

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₃ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : Functor J (ShortComplex C)} (φ : X✝ ⟶ Y✝) : ((inverse J C).map φ).τ₃ = Functor.whiskerRight φ π₃

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₃ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) : ((inverse J C).obj F).X₃ = F.comp π₃

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₂ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : Functor J (ShortComplex C)} (φ : X✝ ⟶ Y✝) : ((inverse J C).map φ).τ₂ = Functor.whiskerRight φ π₂

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_f (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) : ((inverse J C).obj F).f = F.whiskerLeft π₁Toπ₂

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₂ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) : ((inverse J C).obj F).X₂ = F.comp π₂

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₁ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] {X✝ Y✝ : Functor J (ShortComplex C)} (φ : X✝ ⟶ Y✝) : ((inverse J C).map φ).τ₁ = Functor.whiskerRight φ π₁

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_g (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) : ((inverse J C).obj F).g = F.whiskerLeft π₂Toπ₃

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₁ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) : ((inverse J C).obj F).X₁ = F.comp π₁

def CategoryTheory.ShortComplex.FunctorEquivalence.unitIso (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : Functor.id (ShortComplex (Functor J C)) ≅ (functor J C).comp (inverse J C)

The unit isomorphism of the equivalence ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₂_app (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) : ((unitIso J C).inv.app X).τ₂.app X✝ = CategoryStruct.id (X.X₂.obj X✝)

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₂_app (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) : ((unitIso J C).hom.app X).τ₂.app X✝ = CategoryStruct.id (X.X₂.obj X✝)

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₁_app (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) : ((unitIso J C).inv.app X).τ₁.app X✝ = CategoryStruct.id (X.X₁.obj X✝)

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₃_app (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) : ((unitIso J C).inv.app X).τ₃.app X✝ = CategoryStruct.id (X.X₃.obj X✝)

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₃_app (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) : ((unitIso J C).hom.app X).τ₃.app X✝ = CategoryStruct.id (X.X₃.obj X✝)

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₁_app (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : ShortComplex (Functor J C)) (X✝ : J) : ((unitIso J C).hom.app X).τ₁.app X✝ = CategoryStruct.id (X.X₁.obj X✝)

def CategoryTheory.ShortComplex.FunctorEquivalence.counitIso (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : (inverse J C).comp (functor J C) ≅ Functor.id (Functor J (ShortComplex C))

The counit isomorphism of the equivalence ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₃ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) : (((counitIso J C).hom.app X).app X✝).τ₃ = CategoryStruct.id (X.obj X✝).X₃

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₃ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) : (((counitIso J C).inv.app X).app X✝).τ₃ = CategoryStruct.id (X.obj X✝).X₃

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₂ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) : (((counitIso J C).hom.app X).app X✝).τ₂ = CategoryStruct.id (X.obj X✝).X₂

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₁ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) : (((counitIso J C).inv.app X).app X✝).τ₁ = CategoryStruct.id (X.obj X✝).X₁

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₂ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) : (((counitIso J C).inv.app X).app X✝).τ₂ = CategoryStruct.id (X.obj X✝).X₂

@[simp]

theorem CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₁ (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] (X : Functor J (ShortComplex C)) (X✝ : J) : (((counitIso J C).hom.app X).app X✝).τ₁ = CategoryStruct.id (X.obj X✝).X₁

def CategoryTheory.ShortComplex.functorEquivalence (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : ShortComplex (Functor J C) ≌ Functor J (ShortComplex C)

The obvious equivalence ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C.

@[simp]

theorem CategoryTheory.ShortComplex.functorEquivalence_unitIso (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : (functorEquivalence J C).unitIso = FunctorEquivalence.unitIso J C

@[simp]

theorem CategoryTheory.ShortComplex.functorEquivalence_functor (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : (functorEquivalence J C).functor = FunctorEquivalence.functor J C

@[simp]

theorem CategoryTheory.ShortComplex.functorEquivalence_inverse (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : (functorEquivalence J C).inverse = FunctorEquivalence.inverse J C

@[simp]

theorem CategoryTheory.ShortComplex.functorEquivalence_counitIso (J : Type u_1) (C : Type u_2) [Category.{v_1, u_1} J] [Category.{v_2, u_2} C] [Limits.HasZeroMorphisms C] : (functorEquivalence J C).counitIso = FunctorEquivalence.counitIso J C