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.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The unit 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) [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (X : J) : (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X).app X).τ₁ = CategoryTheory.CategoryStruct.id (X.obj X).X₁

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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